[SamuelSchlesinger]

Change

#2191 removed a fixed cost of about 0.4 s from every polytime/ppt call. The cost came from rebuilding the table of imported modules whose import closure declares a raw-family (Turing.MultiTapeTM.ComputableTidily…/ComputesTidily…) constant. #2191 kept the table in a process-global IO.Ref keyed by the import list. This PR keeps the speed-up and changes how the table is stored. Search is unchanged.

• The table is now the state of an environment extension. rawImportClosureExt is a persistent extension that stores no entries. Its addImportedFn creates a Thunk over the import header. The table belongs to the environment it was computed from, so there is no global state and no key comparison. The scan runs once per file, on the first call that needs it, and never in files that do not call the tactics. Forcing a Thunk is thread-safe, so proofs elaborated in parallel share one scan. With perf(polytime): compute the raw-import classification once per file #2191's IO.Ref, every theorem body that started before the first scan finished ran its own scan. In a file of five theorem … := by polytime, each call took about 0.38 s.
• One structural raw-family test. isRawFamilyName matches the name component after Turing.MultiTapeTM. It replaces two copies of a Name.toString prefix test, one in the import scan and one in rawTransitionPremise. It allocates nothing and makes the one-time scan about 40% cheaper.

When #862 deletes the tidy calculus, isRawFamilyName, rawImportClosure and rawImportClosureExt go with the rest of the classification memo.

Options tried

1. (a) A cheaper scan with no cache. Not enough. The structural test cuts a full scan of Complexity.Tactic.PolyTime's imports (343k constants) from about 400 ms to about 230 ms, or about 160 ms with an extra Name.isPrefixOf guard. The tactic's meta code is interpreted, though, so the per-name loop still dominates. Every call then costs about 240 ms, against 28 ms with a cached table. PolyTimeTactic was 56% slower.
2. (b) An environment extension. Chosen. It matches or beats perf(polytime): compute the raw-import classification once per file #2191 on every measurement below.
3. (c) The IO.Ref. Not needed.

Timings

lake env lean on the same base (#2191's head fc5455819, prebuilt imports), so the only difference is PolyTime.lean. Each figure is the median of 3 runs with LEAN_NUM_THREADS=4. Per-call figures come from set_option profiler true on the trivial goal ComputableInPolyTime (fun n : ℕ => n + 1) encUnary encUnary. The machine was shared (load 4–8), so differences under about 1 s are noise.

	#2191 (IO.Ref)	(a) structural scan, no cache	(b) extension (this PR)
trivial polytime, first call in a file	375 ms	240 ms	233 ms
trivial polytime, later calls	28 ms	240 ms	28 ms
file with five such theorems, wall / CPU	2.02 s / 2.75 s	1.96 s / 2.01 s	1.91 s / 1.51 s
Crypto.Protocols.MAC.CarterWegman, wall / CPU	27.2 s / 43.4 s	31.6 s / 49.5 s	25.5 s / 40.9 s
ComplexityTests.PolyTimeTactic, wall / CPU	21.5 s / 20.8 s	33.4 s / 32.6 s	21.2 s / 20.6 s

The five-theorem row shows the parallel case. Under (b), the calls wait for one scan instead of each running their own.

Search behaviour

The table only decides which rules skip the exact premise check (hasRawPremise). A module with no raw-family constant in its import closure cannot state a raw premise. I checked the new test against the old one over every constant imported by Complexity together with ComplexityTests.PolyTimeTactic: 677,252 names in 9,548 modules. The two tests agree on every name, 545 of which are raw-family, and the resulting per-module tables are identical (1,374 modules can see the raw family). Rule classifications, certificate filtering and search are therefore unchanged.

Validation

• Built the tactic tests with --wfail --iofail: ComplexityTests.PolyTime*, PPT*, ProgramCertificateDiagnostics and Machines.Turing.MultiTape.Internal.PolyTimeBoundary. PPTMemoScope covers the memo's scoping and PolyTimeBoundary covers the raw/plain boundary that this table serves.
• scripts/check.sh --quick against origin/main fe49fb4eb rebuilt and checked all 397 affected targets (PolyTime.lean's clients across Complexity, ComplexityTests and ComplexityAbstracts), followed by lake build Complexity ComplexityTests ComplexityAbstracts --wfail --iofail. Both pass.
• check_hygiene.py --check-simp, check_tidy_surface.py and check_changed_files.py --base origin/main pass.

Contributes to #622; follows up #2191.

AI assistance

Written and measured by worker-claude-015dlg8k-tacticcache (Claude Code, Opus) for coordinator-claude-015dlg8k. Needs independent review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): this is a Claude-fleet PR from worker-claude-015dlg8k-tacticcache, the taste follow-up to #2191 that Samuel requested. The global IO.Ref is replaced by an environment extension holding a lazily built Thunk, and a structural Name test replaces the two toString prefix copies. It is one file, about +24/−23. Search behaviour is unchanged, checked on all 677k imported names. It also stops #2191's duplicate scans when theorem bodies elaborate in parallel. Please review at dc648c3ba0a10fd80653039398dd944ddeac34bf: reviewer-codex-edemaine (@edemaine) or codex-pcp-review-20261101.

[edemaine]

APPROVE — reviewer-codex-edemaine, independent non-author review of dc648c3ba0a10fd80653039398dd944ddeac34bf.

Read the complete one-file diff, classification callers, existing memo-scope/raw-boundary tests and pinned Lean extension/Thunk implementation. The empty-entry extension captures only the fixed import header; each imported environment initializes its own lazy table, and forcing the shared thunk memoizes the scan. Current-module declarations and unknown metadata retain conservative exact checks. No local proofs, evidence or changing rule classifications leak into this import cache. The structural name test correctly recognizes the raw namespace component and descendants; filtering/search logic is unchanged.

Hygiene/simp and whitespace checks pass. The author reports the focused/397-client builds and a full imported-name equivalence comparison; I did not repeat those builds, that exhaustive comparison or the timing experiment. At one CI inspection, Guide/title passed and library CI was running. No mathematical, resource or abstract change. Agent review, not human approval; required final validation remains before integration.