Optimize PhaseRetrieval analytic and Hermite proofs

[Vilin97]

PhaseRetrieval repeats expensive Gaussian integrability and norm estimates and uses broad automation for several elementary algebraic steps. This refactor reuses weighted L2, bilinear, Hölder, and Cauchy–Schwarz arguments while preserving every original declaration.

The selected project has 44 original modules, roughly 2.3 MB of source, and 3,841 unique original environment declarations. Baseline profiling identified the analytic wrappers and Hermite basis proofs as worthwhile targets. This is an optimization of the existing completed project; no project is imported or vendored.

Changes:

• Share bilinear difference/norm bounds and an L1 bound for differences of squared norms; reuse Mathlib's integral and Hölder estimates in the STFT/ambiguity arguments.
• Reuse L2 closure for Gaussian weighted-square integrability, and reuse the existing weighted Cauchy–Schwarz lemma for the Hermite truncation bound. Move its existing prerequisites earlier without changing their definitions.
• Use descending-factorial vanishing for the Hermite support argument, finite polynomial roots for the dense nonzero set, and a measurable representative for the almost-everywhere product argument.
• Replace broad rank-one recovery simplification with zero-product and cancellation lemmas, remove unnecessary field normalization, and narrow arithmetic/simplification hypotheses throughout this project.

Base: cef43c9dad38860a5c57245205f2299f92d76184.
Head: 0bf6857e9b69ff3ee214315f3280532984ada7e5.
The live base pins Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e; these pins are unchanged.

Invariant audit

Before editing, a Lean environment inspection recorded all original modules with importAll := true, trustLevel := 0, and extensions disabled. The manifest serializes full elaborated Expr types, ordered universe parameters, declaration kinds, safety, reducibility hints, and all non-theorem values. Only theorem proof bodies are omitted. The rebuilt candidate is compared against that original manifest.

All 3,841 original unique declarations remain. Every original non-theorem value is identical, with no changed type, universe list, kind, safety, or reducibility hint. Only alpha-renamed generated bound-variable labels in 45 types are normalized; no definitional-equivalence normalization is used. A separate source comparison finds no original signature/binder change or removed declaration in the 36 modified files. There are five new private mathematical helpers and twelve generated auxiliaries/equation theorems.

The explicitly retained _simp/proof helpers already existed in the base environment. The small zero-application proof in the STFT difference argument generates its original reserved pairing congruence theorem. These preserve the strict environment contract while allowing the expensive parent proofs to change.

Measurements

Metric	Baseline samples	Head samples	Median baseline → head	Reduction
Wall (s)	[281.44, 279.6, 272.84]	[229.28, 257.77, 226.08]	279.6 → 229.28	18.00%
CPU, user + system (s)	[643.54, 639.39, 663.44]	[574.46, 582.29, 586.46]	643.54 → 582.29	9.52%
Maximum compiler-child RSS (KiB)	[1965348, 1968860, 1966072]	[1968932, 1973464, 1977084]	1966072 → 1973464	-0.38%

Each sample clears only PhaseRetrieval's own library/IR build outputs and runs /usr/bin/time lake build LeanPool.PhaseRetrieval.Imports with ordinary Lake defaults. Dependencies remain cached. The final source sets are frozen and hashed; the three pairs run in baseline/head, head/baseline, baseline/head order. No other Lean jobs from this optimization worker run during measurement. The VM is shared, so elapsed times contain scheduling noise. RSS is GNU time's maximum single compiler-child resident set, not total simultaneous build memory.

The Hermite truncation proof's allocation profile falls from 22,301,993 to 4,452,611 raw profiler heartbeats using identical command-profiler options. This is a declaration-level metric, separate from the full-build measurements above.

Validation

• Warning-free lake build LeanPool.PhaseRetrieval.Imports.
• Complete declaration-manifest comparison and independent source-signature comparison.
• lake shake --force --keep-public LeanPool.PhaseRetrieval.Imports after the project build.
• lake exe runLinter --no-build LeanPool.PhaseRetrieval.Imports.
• lake exe lint-style LeanPool.PhaseRetrieval.Imports.
• The unmodified repository quality/trust checker on an isolated view containing the project's actual sources/card, unchanged configuration, and actual compiled outputs.
• lake exe mk_all --module --check and git diff --check.

Full-pool validation remains for PR CI. The project card, generated indexes, other projects, dependency pins, CI, configuration, and gates are unchanged. No merge or auto-merge is requested.

[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 the proof refactor; external source and license checks remain unverified.

Summary

Refactors existing PhaseRetrieval proofs without changing their mathematical statements.

• PhaseRetrieval proofs reuse shared estimates to finish with less repeated work.

No actionable issue was found in the reviewed changes. The project card and headline declarations were checked for changes to their claims and assumptions. External source fidelity and upstream license evidence were not independently verified. The supplied timing results and full declaration-manifest comparison were not independently reproduced.

Vilin97 explicitly identifies the retained generated helpers and hpairing_zero as intentional compatibility measures in the supplied PR description.

_{Reviews (1) · Last reviewed commit: "Optimize PhaseRetrieval analytic and Her..." · Reviewed by Greptile}

[Vilin97]

{
"summary": "This refactor narrows arithmetic hypotheses, removes unnecessary simplification and normalization, and reuses analytic estimates in the existing PhaseRetrieval proofs. The named intermediate arguments remain available rather than being replaced by broad proof search. The published timing and compiled declaration-manifest results are the author's measurements; I did not rerun them.",
"assessment": {
"scope": "analytic helper reuse and targeted proof simplification",
"introduces_tech_debt": false,
"maintainability": "improved",
"brittleness": "more_robust",
"risk": "medium",
"assessment_one_sentence": "The changes make the analytic and Hermite arguments more explicit and reusable without an actionable maintenance regression."
},
"verdict": "approve",
"findings": []
}

[Vilin97]

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

Reviewed head: 0bf6857e9b69ff3ee214315f3280532984ada7e5

Verdict: 🤔 needs_discussion

The refactor shares analytic estimates, reuses weighted L2 and Cauchy–Schwarz arguments, and narrows automation while retaining the main proof structure. These changes improve readability and reuse, but manually preserving generated private proof artifacts adds avoidable maintenance debt. Builds and reported timings were not independently reproduced because dependency artifacts are absent locally.

Aspect	Value
Scope	proof reuse and tactic rewrites
Introduces tech debt	🛑 yes
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	🟡 medium

The substantive proof changes improve maintainability, but the compatibility obligation for generated private artifacts needs a maintainer decision.

Findings (1)

• dead-leftover — LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean:5906
  The seven hand-written _simp theorems here have no callers or attributes. The same preservation strategy adds an unused bessel_truncate_le._simp_1_2 and an unused hpairing_zero elsewhere, while norm_sq_phi_integral._proof_1_10 copies an explicit order-instance projection chain. This turns transient tactic output into hand-maintained source. Establish whether these generated private constants have a concrete downstream compatibility requirement; otherwise remove the preservation scaffolding and allow generated private auxiliaries to change with their proofs.

---

Tokens: 3,346,635 in / 10,873 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $13.5496 (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]

Maintainer adjudication for 0bf6857e9b69ff3ee214315f3280532984ada7e5 and review job 2213:

My earlier introduces_tech_debt: false was too broad. The eight unused private _simp facts and the hpairing_zero generator deliberately preserve the PR's stated environment-compatibility target. norm_sq_phi_integral._proof_1_10 has a real caller; its expanded order-instance expression still carries maintenance cost.

I accept this bounded cost for this refactor. Its explicit scope preserves the original declaration names and types, including generated private auxiliaries; deleting the shims would change that scope. This establishes neither a concrete downstream consumer nor a repository-wide obligation to freeze private names. The compiled 3,841-declaration comparison and timings remain the author's reported results. The independently reviewed proof reuse and completed authored CI support retaining the source approval.

The configured verdict remains needs_discussion; this reply records the maintainer's decision on that trade-off. Current-main qualification and every normal protected queue gate still apply.