Optimize FriezePatterns continuant proof elaboration

[Vilin97]

FriezePatterns' two continuant proofs expand large field expressions before cancelling a nonzero interior entry. This change cancels first and uses explicit algebraic rewrites, reducing elaboration work while preserving every existing declaration.

The exact base is 766a994003f161b1013109977cd615b06d0dd5a9; the head is 238cb39646cba35c3058a27d2259a1d63a405955. Its actual pins are Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; the task's older 4.34 reference was superseded by the current repository pin. No pins were changed. PR610 and PR611 are merged, and the current base has a successful Build pool check. This PR remains open for normal review and protections, with no auto-merge enabled.

Changes are confined to LeanPool/FriezePatterns/Chapter1.lean:

• pattern_nContinuant1 applies nonzero multiplication cancellation directly, then uses the induction hypothesis and two diamond relations. Explicit associativity, distributivity and subtraction lemmas replace ring_nf and the final convert.
• pattern_nContinuant2 retains the reverse induction and all its index bounds. Its step uses nonzero cancellation and explicit algebra instead of repeatedly expanding products with field inverses and calling ring or simp_all.
• Remove the private RingNF import now that neither proof calls ring normalization. The Chapter1 build graph drops from 929 to 926 jobs. The full project graph remains at 996 jobs. Public imports are preserved.

Before editing, an independent Lean environment inspector imported the compiled base project aggregate and enumerated env.header.moduleData.constNames. It recorded all 555 owned constants, including compiler auxiliaries, by full name, kind, exact universe parameters, full elaborated type, safety, reducibility and inductive/constructor/recursor metadata. Expression DAG serialization includes constants, universe levels, binder information and de Bruijn indices. It additionally records the values of all 70 non-theorem declarations, including generated matchers and recursor rules. Only theorem proof bodies are excluded.

The rebuilt-head comparison has zero missing declarations, zero additions and zero semantic changes. All 70 non-theorem records are exactly equal. All public declaration types are exactly equal. The sole raw difference is an autogenerated hygienic bound-variable number in pattern_nContinuant2._proof_1_13; its type is alpha-equivalent. Comparison normalizes only hygienic bound-variable names in theorem types; constant names, universe names, ordinary binder names, expression structure and non-theorem values are kept exact. A separate source-signature comparison reports zero changed statements, binder renames, additions or removals across the eight source declarations.

Measurements use the same isolated VM worktree and pinned dependencies. Each clean trial removes only this project's compiled artifacts from the worktree's build directory, retaining dependency oleans. Times include Lake startup. Three alternating paired project trials use baseline→head, head→baseline, baseline→head order.

Clean target	Baseline trials (seconds)	Optimized trials (seconds)	Median before → after
LeanPool.FriezePatterns.Chapter1	4.456588, 4.792858, 4.333063	3.993759, 3.949204, 4.155182	4.456588 → 3.993759 (10.4% lower)
LeanPool.FriezePatterns.Imports, paired	16.432733, 17.143325, 16.645540	16.477274, 16.882852, 18.830375	16.645540 → 16.882852 (1.4% higher)

Initial unpaired project medians were 16.826793 → 18.491182 seconds; the discrepancy prompted the paired runs above. There is no claim of an overall build speedup. The unchanged Chapter2 remains the longest module, and shared-VM timing varies.

Synchronous command profiling uses the first successful theorem trace, excluding the linter's repeated elaboration. Counts are raw heartbeat allocations, not the divided heartbeat-budget units.

Declaration	Baseline	Optimized	Reduction
pattern_nContinuant1	7,248,301	2,834,314	60.9%
pattern_nContinuant2	26,682,158	13,020,882	51.2%

Validation:

lake build LeanPool.FriezePatterns.Imports
lake env lean --profile LeanPool/FriezePatterns/Chapter1.lean
lake env lean -DElab.async=false -Dtrace.Elab.command=true -Dtrace.profiler=true \
  -Dtrace.profiler.useHeartbeats=true -Dtrace.profiler.threshold=1000000000000000000 \
  LeanPool/FriezePatterns/Chapter1.lean
lake env lean --run <scratch>/Manifest.lean
python3 <scratch>/compare-manifests.py
lake env lean --run scripts/ci/lint-project.lean LeanPool.FriezePatterns \
  LeanPool.FriezePatterns.Chapter1 LeanPool.FriezePatterns.Chapter2 \
  LeanPool.FriezePatterns.Chapter3 LeanPool.FriezePatterns.Imports
lake exe lint-style LeanPool.FriezePatterns.Imports
lake exe mk_all --module --check
lake shake --force --keep-public LeanPool.FriezePatterns.Imports
python -m lean_pool.quality --repo . --static-only
lake env lean --run <scratch>/AuditAxioms.lean
PYTHONPATH=python python <scratch>/quality-project.py
git diff --check

The selected project builds warning-free and all 555 constants pass the repository's slow declaration linters. Text style, generated indexes, static repository/card checks, declaration resolution, allowed-axiom dependency collection and the repository's full compiled-environment option/backdoor audit pass. Shake reports no additional changes; --force skips its unrelated whole-pool freshness check after the entire selected project closure has been built. No gates or waivers were changed. Whole-pool CI and remote refactor review remain for GitHub.

Reproduction scripts, manifests, raw logs and full-precision timings are preserved under /data/codex/scratch/vilin/optimization-20261010-resume/. The interrupted attempt's worktree and logs remain intact; it had no source edits or PR to duplicate.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low impact] No blocking defect was found in these proof-only changes.

Summary

Rewrites pattern_nContinuant1 and pattern_nContinuant2 to cancel a nonzero factor before working through the diamond relations.

• The first continuant proof cancels before expanding products.
• The reverse continuant proof cancels without field inverses.

_{Reviews (1) · Last reviewed commit: "Optimize FriezePatterns continuant proof..." · Reviewed by Greptile}

[Vilin97]

🤖 LLM review — refactor (gpt-6.1-sol)

Reviewed head: 238cb39646cba35c3058a27d2259a1d63a405955

Verdict: ✅ approve

Both continuant proofs now cancel the nonzero interior factor first and follow explicit algebraic calc chains. The induction structure and index bounds remain available for debugging, while inverse expansion and broad simplification are reduced. Independent profiling confirms heartbeat reductions of 60.9% and 51.2%. The selected project compiled without diagnostics using matching cached dependencies; Lake dependency fetching was blocked by HTTP 403.

Aspect	Value
Scope	continuant proof tactic rewrite
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The refactor makes the algebraic argument easier to debug and cheaper to elaborate without losing reusable lemmas or induction structure.

---

Tokens: 1,077,439 in / 8,483 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $4.4370 (Standard API equivalent; uncached input) (long-context rate)
Automated review against .github/REFACTOR_REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Reviewed LeanPool/FriezePatterns/Chapter1.lean at 238cb39646cba35c3058a27d2259a1d63a405955 against sole parent 766a994003f161b1013109977cd615b06d0dd5a9, reading both complete files. This is a proof refactor within the existing FriezePatterns project.

• Faithfulness: PASS. All eight declaration statements and six complete declarations are unchanged. Both continuant proofs retain the same nonzero hypotheses, interior/index bounds, induction contracts and conclusions.
• Novelty: PASS for this refactor. The contribution is a simpler proof implementation; no new headline mathematical result or claim of global novelty is needed.
• Significance: PASS. Cancelling the established nonzero interior factor first shortens both arguments. The second proof avoids introducing field inverses, and explicit algebraic rewrites replace the former ring automation. This improves maintainability within an existing project.
• Sources: PASS within the diff. No citation, license or provenance change is introduced. Existing project provenance was not independently reverified in this review.
• Quality: PASS on source review. The edits are confined to pattern_nContinuant1, pattern_nContinuant2 and removal of the private Mathlib.Tactic.Ring.RingNF import. The cancellation steps use the existing nonzero evidence; I found no concrete statement or proof-structure blocker in the complete comparison.

The author reports Chapter1 medians of 4.4566 → 3.9938 seconds, while whole-project medians are 16.6455 → 16.8829 seconds. These are author measurements and do not establish an overall project speedup. I did not independently run Lean, a kernel check, exports, downstream builds or a benchmark; removing the private import does not by itself establish export/API invariance.