Optimize QuantumParallelRepetition proof elaboration

[Vilin97]

QuantumParallelRepetition repeatedly expands scalar, matrix and history arguments inside large proof contexts. This replaces those steps with direct identities, shared existing theorems and explicit tactic inputs, while preserving every original declaration and import path.

• Use Parseval for purification Gram entries, a Gram-matrix proof of local-unitary norm preservation, and direct diagonal-positivity/Hermitian-integral arguments.
• Keep EPR and embezzlement scalars abstract in the spectral-gauge sum. Reuse groupedMass_expectation and the existing masked-history results; a new private finitePrefixMask_attach_flag lemma simplifies both marked-context proofs.
• Use direct square, norm, square-root and order lemmas. Replace associativity/commutativity normalization with ac_rfl, and restrict profiled arithmetic/simplifier calls to their dependencies. Retain the mathematical intermediate steps and all original private/generated declarations.

The target is the existing roughly 72,000-line project, with twelve sequential Part modules and measured hotspots in purification Gram, spectral-gauge and history/operator proofs.

Base: 929e41de6782f0a9d418d2b5cd60fe89a5539120. Head: a5f259bf1170d7a7e1f11811d3b322493f1403b8. A pre-edit Lean environment manifest was recorded at this base before applying any proof changes. The live pins are Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; configuration is unchanged.

The invariant audit reads the compiled Lean environment with extensions disabled and serializes exact expression DAGs. It compares qualified names, elaborated types (including binder names/annotations and metadata), universe parameter lists, safety/partial flags, reducibility/mutual metadata, every non-theorem value, and inductive/constructor/recursor data. Only theorem proof bodies are excluded. All 4,766 original declarations match exactly: zero missing or changed entries, with no exceptions or normalization allowances. The 20 additions are one private supporting lemma and 19 generated private simplifier lemmas. All 2,861 original exported entries match exactly, with no public additions. Separate exported-environment audits importing each original Part01–Part12 and the original project entry individually also have zero differences. An independent source-range audit preserves 2,642 original explicit theorem headers or complete non-theorem declarations byte-for-byte (1,818 theorem headers, 743 definitions, 17 structures, 57 abbreviations, 7 instances); generated declarations are covered by the compiled audit.

Two-CPU affinity (3 runs/revision)

Revision	Run	Wall s	User s	System s	Max process RSS KiB	Aggregate RSS KiB	Aggregate PSS KiB
base	1	416.99	411.89	10.01	1,928,920	2,824,220	1,367,817
base	2	350.9	373.1	9.44	1,936,372	2,836,300	2,400,614
base	3	379.52	381.89	9.67	1,926,564	2,833,180	2,338,384
optimized	1	360.17	355.83	9.49	1,910,872	2,810,028	2,357,450
optimized	2	331.22	344.59	9.7	1,913,576	2,814,632	2,390,005
optimized	3	354.14	342.25	9.62	1,912,348	2,818,304	1,698,627

Median wall time: 379.52 → 354.14 (6.69% lower).
Median user CPU: 381.89 → 344.59 (9.77% lower).
Median peak compiler RSS: 1,928,920 → 1,912,348 (0.86% lower).
Paired wall reductions: 13.63%, 5.61%, 6.69%.

Ordinary Lake scheduling (2 runs/revision)

Revision	Run	Wall s	User s	System s	Max process RSS KiB	Aggregate RSS KiB	Aggregate PSS KiB
base	1	245.21	376.02	9.87	1,934,528	2,835,820	1,292,056
base	2	219.26	361.93	10.14	1,925,392	2,828,964	2,420,926
optimized	1	197.6	331.79	9.78	1,913,972	2,814,364	2,414,078
optimized	2	193.14	331.44	9.94	1,901,432	2,810,772	2,410,493

Median wall time: 232.235 → 195.37 (15.87% lower).
Median user CPU: 368.975 → 331.615 (10.13% lower).
Median peak compiler RSS: 1,929,960 → 1,907,702 (1.15% lower).
Paired wall reductions: 19.42%, 11.91%.

Measurements wrap lake --wfail build LeanPool.QuantumParallelRepetition.Imports in GNU time. Before every run, only the selected project's .lake/build/lib/lean and .lake/build/ir artifacts are deleted; pinned dependencies and filesystem caches stay warm. Both revisions use identical Lean/Lake options. The three-pair series uses taskset -c 6,8 and the order base/head/head/base/base/head. The separate ordinary-scheduling two-pair series uses the order base/head/head/base and no affinity restriction. Frozen source fingerprints are checked throughout both series; the modes are not pooled. GNU time records wall, user/system CPU and maximum single-process RSS. A separate process-group monitor samples aggregate RSS/PSS every 0.5 seconds. Aggregate RSS double-counts shared mapped pages; PSS apportions them. This is a shared Azure VM with other independent jobs, so wall times reflect scheduling variation. No other Lean compiler, profiler or validation process from this task runs during this series.

The ordinary-scheduling sample exceeds the 10% wall-time target; the two-CPU series shows a smaller 6.69% median reduction. Both series and every run are retained above. The ordinary sample has two pairs, and wall-time variation on the shared VM limits generalization. The resumed cycle also completed six hours of effort. No 10% RAM reduction was observed.

Validation on the measured source:

lake --wfail build LeanPool.QuantumParallelRepetition.Imports
lake env lean --run scripts/ci/lint-project.lean \
  LeanPool.QuantumParallelRepetition LeanPool.QuantumParallelRepetition.Imports \
  LeanPool.QuantumParallelRepetition.Part{01..12}
lake exe lint-style LeanPool.QuantumParallelRepetition.Imports
lake shake --force --keep-public LeanPool.QuantumParallelRepetition.Imports
git diff --check

Mathlib/Batteries linters pass for all 14 project modules and 4,786 declarations. Style and warning checks pass. Read-only shake reports no remaining public-preserving import changes. The unmodified production quality checker and index checker pass in a selected-project filesystem view, including headers, forbidden-code/options, sizes, registry/card/reachability, axiom and compiled backdoor audits:

uv run python -m lean_pool.quality --repo <selected-project-view>
uv run python -m lean_pool.indexes --repo <selected-project-view> --check

Full/public/per-import/source manifest comparisons also pass. Full/public manifests were repeated after the final builds. Repository-wide lake exe mk_all --module --check passes as well. Full-pool and protected PR validation, and independent refactor review, remain separate requirements. The change edits 340 explicit theorem proof bodies across ten source files; the public API, original definitions and statements, imports, generated indexes, card, root index, pins and gates are fixed. This PR is left open with auto-merge disabled.

[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 actionable defect was found in the proof-only changes; independent build, environment-audit, and upstream-source verification remain outside this review.

Summary

Refactors proofs across Part01.lean–Part10.lean without changing original statements, definitions, or import paths.

• Quantum repetition proofs elaborate with less work.

No actionable defect was found. The reported timing improvements were not independently reproduced. Builds and compiled-environment audits were not rerun. The unchanged card and headline statements were inspected; the pinned upstream source and license were not independently verified.

Vilin97 explicitly acknowledged the smaller two-CPU improvement and the absence of a 10% RAM reduction. These are disclosed limits, not hidden regressions.

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

[Vilin97]

{
"summary": "This refactor makes the QuantumParallelRepetition proofs use named Parseval, Gram, norm and order identities, shares the prefix-mask flag identity, and replaces broad local normalization with explicit tactic inputs. The complete ten-file delta preserves the original source contracts, definitions, scopes and imports. Mathematical intermediates remain visible, and the measured performance claims disclose their small samples and shared-host variability; benchmark and compiled-environment results remain contributor-reported.",
"assessment": {
"scope": "Proof elaboration refactor across Parts01–10",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "low",
"assessment_one_sentence": "Named mathematical producers and the reused private flag lemma reduce duplicated expansions and search dependencies while preserving all original source contracts; protected exact-head validation and configured review remain separate."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: a5f259bf1170d7a7e1f11811d3b322493f1403b8

Verdict: ✅ approve

The refactor replaces broad tactic inputs with explicit dependencies and direct identities across ten QuantumParallelRepetition modules. The larger Gram, spectral-gauge, and history rewrites preserve the mathematical checkpoints while reusing existing results and sharing a small mask lemma. I found no actionable maintenance regression. Compilation and performance claims remain independently unverified: local elaboration stopped because Mathlib dependencies are absent.

Aspect	Value
Scope	proof elaboration optimization
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

Explicit proof dependencies and shared identities make these proofs easier to maintain without sacrificing their mathematical structure.

---

Tokens: 968,822 in / 6,659 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $3.9752 (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.