Optimize PhaseRetrieval arithmetic and analytic proofs

[Vilin97]

PhaseRetrieval's pointwise and stability estimates spend substantial compilation time in broad arithmetic searches, and its analytic bridges repeatedly simplify expanded integral kernels. This refactor uses explicit mathematical certificates and smaller tactic inputs while preserving every pre-existing declaration.

The rho lower bound now uses a sum of squares identity: with s = u² + v², t = u²/2 + v² + s² and A = 2 + 2u + s - u²/2 + s², it proves
A² - 4((1+u)²+v²) = 2(u+t)² + (2s-t)(2s+t) and derives 0 ≤ t ≤ 2s from the existing hypotheses. The closing stability estimate uses square monotonicity, multiplication of inequalities and explicit linear combinations. Hermite and circle estimates use smaller arithmetic inputs, direct associativity/commutativity proofs, and explicit simplifier lemma sets.

The analytic changes transport derivative coefficients through a direct commutativity equality, prove the Fourier norm and translation steps through pointwise integral identities, and normalize the Fourier phase once for both sections. The import pass removes 116 private imports and adds three direct dependencies. Proof edits are confined to seven files; the remaining changes are import cleanup within the same project. All public import lists remain identical.

Base: 59fa0f4d29068a41b6c6f5aaf7da42876f1e55aa.
Head: 3a09f88fa25099e719ddddf8051fcace855565ab.
Toolchain: the repository-pinned Lean/Mathlib 4.35.0-rc3.

The invariant audit imports all 44 project modules with importAll := true, loadExts := false, trustLevel := 0. Lean environment inspection serializes each module constant's name, universe parameters, complete elaborated type, safety/partial flags and mutual-declaration list. It also records every non-theorem value, reducibility hint, and inductive/constructor/recursor structure. Theorem bodies and nonsemantic expression metadata are excluded; binder names and macro hygiene are retained.

Result: all 3,480 pre-existing module records match exactly, including 436 definition records, 3,035 theorem records and nine structural records (3,467 distinct names). Zero original records changed or disappeared. There are 374 additional compiler-generated private theorem helpers; all are safe and non-partial. No existing statement, definition value, universe list, safety level or public name changed. The base manifest SHA-256 is 45b3845a46cd5ff6e5066068106da49ffc6b11fd2c736056fa140392ec996c28; the final manifest SHA-256 is 74d12e03b3b005a2fbb722fafa7f0d4395489cda05d9607b7c63e4649d9daf98. Generated helper differences were audited as well as named declarations.

Observed median wall time: 332.97 s → 299.27 s (10.12% lower). Median CPU time (user + system): 615.08 s → 538.28 s (12.49% lower). Median max RSS: 1,997,064 → 1,976,376 KiB (1.04% lower).

Order	Revision	Wall s	User s	System s	Max RSS KiB
1	base	332.83	589.93	24.78	1,995,004
2	head	306.88	514.36	24.46	1,977,668
3	head	298.37	512.83	24.48	1,966,412
4	base	332.97	589.96	25.12	1,999,232
5	base	335.59	590.92	25.00	1,997,064
6	head	299.27	513.56	24.72	1,976,376

Method: three clean project builds per revision in isolated worktrees, in the order base/head/head/base/base/head. Each sample clears only this project's build artifacts; external dependencies and OS caches remain warm. The exact command is:

/usr/bin/time -f '%e %U %S %M' -o SAMPLE.time \
  env LEAN_NUM_THREADS=1 lake build LeanPool.PhaseRetrieval.Imports

All 44 modules must recompile in every sample. Source hashes, the toolchain/manifest hashes and dependency Git SHAs are checked before and after each run. Every completed sample in this final series is included. GNU time RSS is the largest individual process high-water mark, rather than aggregate concurrent memory. The shared VM runs other jobs, so CPU time accompanies wall-clock measurements.

The frozen source passed:

• env LEAN_NUM_THREADS=2 lake --wfail build LeanPool.PhaseRetrieval.Imports and the corresponding --no-build --wfail check.
• lake exe runLinter LeanPool.PhaseRetrieval.Imports.
• lake exe lint-style LeanPool/PhaseRetrieval LeanPool/PhaseRetrieval.lean.
• The unchanged repository quality routines scoped to all 44 source files and the existing card: headers, forbidden text/options, size limits, declarations/card, axiom dependencies and compiled option/axiom-backdoor checks.
• lake exe mk_all --module --check, lake shake --force --keep-public LeanPool.PhaseRetrieval.Imports, and git diff --check.
• The strict declaration manifest and public-import comparisons.

The existing card and generated indexes require no changes. Whole-pool CI and independent review remain applicable. Auto-merge has not been 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 change was found in the proof and private-import refactor.

Summary

Refactors existing PhaseRetrieval proofs and removes private imports without changing the mathematical statements or public import lists.

• PhaseRetrieval proofs use smaller, more explicit steps to compile faster.

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

[Vilin97]

Source review at 3a09f88fa25099e719ddddf8051fcace855565ab:

{
  "summary": "The refactor removes redundant private imports and replaces broad arithmetic/analytic automation with explicit inequalities and targeted simp-only steps. It preserves the accepted PhaseRetrieval interfaces and improves proof structure and robustness.",
  "assessment": {
    "scope": "private-import cleanup and arithmetic/analytic proof refactor",
    "introduces_tech_debt": false,
    "maintainability": "improved",
    "brittleness": "more_robust",
    "risk": "low",
    "assessment_one_sentence": "Approve the source refactor; the explicit sign, coefficient, derivative and Fourier steps are easier to maintain without changing the reviewed contracts."
  },
  "verdict": "approve",
  "findings": [],
  "source_head": "3a09f88fa25099e719ddddf8051fcace855565ab",
  "coverage": "Authenticated base/head pairs for all 40 changed files: 33 are import-only and seven change proofs. All public import lists, 908 recognized written theorem headers and 123 complete non-theorem commands in the seven proof files are preserved by lexical comparison. Mathematical inspection covered complete critical estimates and analytic identities across all seven, including the rho sum-of-squares bound, the 23003 scalar closing estimate, generating-function derivatives, Fourier normalization and translation. This is finite source review, not independent rederivation of all 326 inventoried changed proof bodies.",
  "cost_and_validation": "The reported timing improvements and 3,480-record compiled manifest remain attributed to the author; I have not replayed those measurements or that inspector. Advisory quality is 4/5 with no actionable findings. Current-head whole-pool CI, configured independent review and normal protected integration remain pending requirements; this source assessment does not authorize their bypass."
}

[Vilin97]

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

Reviewed head: 3a09f88fa25099e719ddddf8051fcace855565ab

Verdict: ✅ approve

The refactor replaces broad arithmetic searches with explicit certificates, restricts simplifier inputs, and makes derivative and integral transformations easier to follow. Existing proof structure and reusable helpers remain, and public import lists are unchanged. Targeted checks of the rewritten arithmetic proofs and SafeSquare passed on the pinned toolchain; full project builds and the reported timings were not independently reproduced because analytic dependencies were unavailable locally.

Aspect	Value
Scope	proof optimization and private-import cleanup
Introduces tech debt	✅ no
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The explicit intermediate bounds and narrower tactic dependencies improve maintainability without introducing actionable maintenance debt.

---

Tokens: 3,403,486 in / 9,488 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $13.7563 (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.