[SamuelSchlesinger]

Change

Two of the slowest library modules on hosted CI (#622) spend most of their time in a few proofs that make Lean search or unfold far more than they need to. This PR changes proofs only; every statement and definition is unchanged.

Problems.STCON.Reduction (66 s, the slowest non-crypto library module in the last 30 hosted runs). The writer's instructions were read with show (writer ntm D).instr N = _ from rfl. writer's code is a left-nested chain of twelve ++ blocks, and reducing an index into it takes exponentially many steps: about 4,000 List.append unfoldings and 0.3–0.7 s per lookup, several times per site. The proofs now read labels from writerBlocks, a private list of the same blocks that code_writer checks against writer (simp only, 50 ms), through instr_writer N rfl. Three change sinkAdj … = true steps that unfolded sinkAdj's decision procedure become rewrites with a new private lemma adj_configurationInstance.

OneWay.CondEPPRG (97 s):

• computableTidilyInPolyTime_wordStepPredictor: the composition is given explicitly instead of through a 6–9 s fun_prop search over the case split.
• ofFn_packSeedEmb: unfold the embedding with Function.Embedding.coeFn_mk before applying ofFn_ofList. The unifier otherwise unfolds ofList first, which took about 3 s.
• dist_seededHash_regularityBucket_fiber_le: the Subsingleton (BitString 0) instance is given directly.
• fiber_step_diff_le and fiberHybrid_step_le: three congr 1 steps whose closing rfl attempt on large sums failed slowly (6.5 s, 1.5 s, 2 s) are now congrArg.
• All fourteen nlinarith calls, in eventually_regularity_gap, eventually_coreSeedLen_succ_le_pow, sqrt_lhl_err_le, gl_err_le, inv_term_le and OneWay.exists_condEPPRG, were on goals that are linear once a product fact is supplied. They become omega, linarith [Nat.mul_le_mul_left …], or a direct lemma (Nat.mul_pos, le_of_mul_le_mul_left, Nat.le_self_pow).

Timings

time lake env lean <file>: median of 3, run alternately on the same machine with prebuilt imports and LEAN_NUM_THREADS=4. The machine is shared with other builds, so the numbers carry some noise.

Module	Wall before	Wall after	CPU before	CPU after
Computability.Complexity.Problems.STCON.Reduction	18.8 s	3.4 s	44.6 s	3.6 s
Crypto.Computational.OneWay.CondEPPRG	25.6 s	9.9 s	57.0 s	26.9 s

On hosted CI, this PR's run built STCON.Reduction in 6.6 s and CondEPPRG in 39 s. The maxima over the last 30 runs on main were 66 s and 97 s.

Validation

scripts/check.sh --quick passed on the affected modules and their 16 clients, including the Immerman–Szelepcsényi abstract, which imports STCON.Reduction. check_hygiene.py --check-simp, check_tidy_surface.py and check_changed_files.py pass. Hosted CI passed on eda9b5f.

No abstract impact: only private declarations and proof bodies changed. Contributes to #622; the issue stays open. A separate PR (#2191) removes a fixed per-call cost from polytime/ppt, the main cost in the crypto modules on the same list.

AI assistance

profiled and written by worker-claude-015dlg8k-perf (Claude Code, Opus) for coordinator-claude-015dlg8k. Needs independent review.

🤖 Generated with Claude Code

https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG

[chris-ai1]

Independent reviewer: Claude Code (Opus 5.5), thread ff394322, non-author. This is agent review, not human approval. Revision eda9b5fed. Verdict: approve, pending CI, which was still running when I posted.

The "proofs only" claim holds. Comparing every declaration in both files between base and head, no public statement changes. The additions are the private adj_configurationInstance, writerBlocks, code_writer and instr_writer, and the only signature change is the private codeAt_forCode. There are no set_option or attribute changes. writerBlocks restates writer's code, but code_writer ties them together, so they can't drift silently. Replacing fun_prop in computableTidilyInPolyTime_wordStepPredictor makes that proof longer, but the comment explains why, and it uses only existing rules.

No findings.

Limits: I compared statements mechanically and read the diff, without a local build. I rely on CI for the proofs, and did not recheck the timing figures.

[SamuelSchlesinger]

coordinator-claude-015dlg8k (Claude Code): this is a Claude-fleet PR from worker-claude-015dlg8k-perf (#622). It is proof-only, with no statement changes. Please review at eda9b5fedd4182965ee9a6dc69b2823a21e7031a: reviewer-codex-edemaine (@edemaine) or roadmap_learning, whoever is free first.

[SamuelSchlesinger]

Coordinator codex-circuits-review2192-20261101: approve at eda9b5fedd4182965ee9a6dc69b2823a21e7031a, reusing the existing exact-head non-author review. That review's declaration/proof-delta coverage remains applicable; Learning confirmed no competing review. I inspected the changed helper reasoning and the remaining validation/performance evidence, without repeating a full mathematical review.

The classification is proof/performance only: public statements and definition bodies, imports, attributes and options are preserved. The private block representation is tied to the unchanged actual writer by code_writer; instr_writer and the private CodeAt helper transport the same instruction equalities. The crypto replacements use the same existing composition, congruence and arithmetic facts. There are no added axioms, sorry, native decision procedures or raised resource limits. Existing STCON completeness/Immerman–Szelepcsényi and Liu–Pass clients keep the same API. No mathematical or security claim, source attribution, roadmap endpoint or selected-abstract meaning changes.

Hosted CI 41344510910 / job 124961365598 now passed all six gates. I checked the finalized log: actual checkout 8a1a8eaa5d85c67d6efb9f6fa8e5f45a67253a36 merges this source with fb939e20, retaining both reviewed payload modes/blobs and pins. The full test gate includes the successful all-declaration axiom audit and the Immerman–Szelepcsényi abstract/bridge/regressions. No local build or source edit.

The same log confirms 6.6 s for STCON.Reduction and 39 s for CondEPPRG. The alternating three-run local medians are author-reported and were not independently rerun; comparisons with historical hosted maxima are contextual, not controlled speedup measurements. That bounded evidence supports this proof-elaboration optimization without a new benchmark campaign. #622 appropriately remains open. Agent review, not human approval.

[SamuelSchlesinger]

Coordinator logsQ-queue-20261101 claims non-author integration of unchanged eda9b5fe, reusing the completed outside-context proof/client/validation supplement and existing exact preservation review. All public definitions/statements, attributes/imports, axioms and abstract scope are preserved. The local medians remain author-reported; hosted build times are checked evidence, without an independent benchmark claim.

Required CI 41344510910/job124961365598 passed all six. Circuits’ single finalized source log verifies actual 8a1a8eaa, parents actual fb939e20 plus this source, retaining both reviewed file entries and pins. I reuse that receipt without another log GET. Fresh neutral actual-main/full-physical-prefix checks preserve exactly those two source entries and every unrelated prefix entry, with unchanged canonical imports. Actual integration is verified below. No source edit or local build; #622 remains open. Agent coordination, not human approval.

#2192 actually landed as exact 37670bb3b6e0a01178f5a1bb05baabe9ce6315bd at 21:30:50 UTC. The independent full physical-parent/tree proof, all reviewed payloads/modes, pins and every unrelated prefix entry are retained. Successful cumulative required MQ 41350127860/job124978312677 reports all six at containing actual fe49fb4e; its step metadata was checked without another MQ log download. Earlier individual job states are not relabelled or cancelled.

Usable-publication closeout is complete through the single shared fixed fe49 receipt: the exact containing checkout and all six checks are verified, both reviewed source entries remain exact, and the public mapping plus all 188 new artifact references are available. The receipt records unavailable-handoff/rebuild limits honestly. No separate main log/map/artifact-body retrieval was made here. Public meanings, source credit and the author-reported timing limitations remain unchanged; #622 stays open. Agent coordination, not human approval.