[Vilin97]

PhaseRetrieval repeatedly elaborated the same analytic arguments and normalized large expressions during rewriting. This change shares those arguments and uses typed lemma applications while preserving every existing declaration. Four balanced pairs of project-clean builds measured a median wall-time reduction of 20.78%, from 242.9725 s to 192.474 s.

Selected project: LeanPool/PhaseRetrieval (44 modules, about 49,000 lines). It offered several expensive modules on the compilation path and duplicated Bessel, continuity, integrability, arc-measure and Gaussian-norm proofs. No project is imported or vendored.

Base: df9538f1976de4ab3b22dcaf457f30b28191a7d5. Head: 4c7374da8a11f84e5222c5f1eab33e92a8e32006. Validation uses the repository's actual pinned Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. Those were current-main pins when work began; no version changes are included.

Concrete changes:

• Factor rank-one recovery into a generic almost-everywhere kernel argument and retain the original L2 theorem as a bridge.
• Share the ambiguity-integral representative transport, normalized Gaussian integral, Bessel summability and coefficient-norm lemmas.
• Prove finite Parseval directly with the orthogonal Fourier family. Replace the repeated dominated-convergence construction for circle Parseval with convergence through continuous functions and ContinuousMap.toLp.
• Reuse existing arc-measure, continuity, integrability and rotation lemmas. Replace broad normalization of large STFT/ambiguity expressions with typed congruence and explicit rewrite lists; simplify the high-frequency scalar inequalities.
• Remove the single redundant LpNorm import identified by lake shake. Preserve all existing module headers, theorem signatures and data definitions. Net change: 733 fewer lines across 14 selected-project files.

Invariant audit: before editing, an independent Lean environment inspection recorded every project constant, including private/compiler-generated declarations, at the exact base. The final audit imports LeanPool.PhaseRetrieval.Imports with private data, extensions disabled and trust level zero. It compares names, full elaborated expression DAGs, universe parameters, safety, declaration kind, mutual/constructor/recursor information, and all non-theorem values and reducibility information. Expression metadata is erased; no definitional unfolding or proof-irrelevance normalization is used for data values. All 3,858 original distinct constants are retained, with 15 supporting additions, no missing constants and no semantic differences. Every old source-level statement and definition remains unchanged.

The raw audit has exactly one type-field difference: the retained private circleSeries_l2_identity._proof_1_3 uses the unused hypothesis binder label h instead of the previous compiler-hygienic label. A separate comparison of the de Bruijn expression structure confirms alpha equivalence, retaining every constant, universe and binder-info field. All other original fields, including non-theorem values, compare structurally exactly after metadata removal. Original generated equation/simplifier helpers are deliberately preserved; two local hsum_apply proofs regenerate the old finiteHermiteSum.eq_1 constants.

Measurement: remove only this project's build artifacts from each isolated worktree's .lake/build/lib/lean/LeanPool and .lake/build/ir/LeanPool, including its entry module; keep the same pinned external dependencies prebuilt. Run /usr/bin/time -v lake build LeanPool.PhaseRetrieval.Imports with native/default Lake parallelism. Alternate order as below, with no profiling or validation jobs running concurrently. Source was frozen throughout all eight builds, and all ten dependency checkouts were verified pinned and tracked-clean before and after. All eight runs rebuilt all 44 project modules without warnings.

Pair / order	Base wall (s)	Optimized wall (s)	Base / optimized user CPU (s)	Base / optimized peak RSS (KiB)
1: base → optimized	210.888	183.131	519.09 / 490.10	1970504 / 1944656
2: optimized → base	232.812	197.935	545.22 / 493.85	1962912 / 1953996
3: base → optimized	253.133	243.417	562.13 / 518.62	1973028 / 1949804
4: optimized → base	254.058	187.013	549.74 / 490.05	1967140 / 1946136

The primary comparison is the ratio of four-run medians, declared before completing the series. Median user CPU: 547.480 → 491.975 s (10.14% lower). Median maximum process RSS: 1,968,822 → 1,947,970 KiB (1.06% lower). GNU time's RSS is the maximum process/child RSS, not aggregate memory. Rounded per-module median log times include ImportedAnalyticInputs 62 → 54 s, ExactModulusRecovery 45.5 → 37.5 s, FiniteBaseCircleEstimate 37.5 → 29.5 s, and CoefficientLimitRigidity 15 → 11.5 s; these overlap and are not additive.

Passed checks on the frozen source:

• Eight project-clean lake build LeanPool.PhaseRetrieval.Imports runs and warning scans.
• lake env lean --run scripts/ci/lint-project.lean <all 44 owned modules>: 3,873 declarations; all slow CI declaration linters pass.
• lake exe runLinter --no-build LeanPool.PhaseRetrieval.Imports and lake exe lint-style LeanPool.PhaseRetrieval.Imports.
• Unmodified uv run python -m lean_pool.quality --repo <selected-project-view> with byte-identical ordinary copies of the project, entry file and existing card, unchanged repository configuration, and the real compiled artifacts.
• lake exe mk_all --module --check --repo <selected-project-view> and recursive lake shake --force --explain LeanPool.PhaseRetrieval.Imports.
• Final after-clean environment manifest comparison, alpha-label investigation, full transitive trust walk, and git diff --check. The trust walk visits 3,886 project inventory roots and 67,091 constants; only Quot.sound, Classical.choice and propext occur as axioms.

Limitations: this is a shared VM, and the absolute wall samples vary substantially; the reported reduction is an observation from the complete balanced series, not a guaranteed deployment speedup. Local quality/index checks are scoped to this project; full repository protected CI and independent review remain required. Current main b634835ce57618a1331f62c3dae458c88df868d8 has no intervening change to this project, its pins or the relevant policies. The branch retains the measured base. Root/generated indexes, project cards, CI and gates are unchanged. This PR stays open for normal review; no merge, auto-merge or queue entry 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.

[Medium impact] No change-caused defect was found; the refactor remains subject to the repository’s normal CI checks.

Summary

The PR shares analytic proofs across PhaseRetrieval while retaining existing theorem statements and data definitions.

• Ambiguity recovery reuses shared proofs for representatives and kernels.
• Hermite and Gaussian estimates are shared across polynomial proofs.
• Circle Parseval reaches infinite sums through continuous-function convergence.
• Circle-arc estimates reuse shared endpoint and measure facts.
• Several analytic proof steps now spell out the rewrites they need.

Review limits: builds, timing measurements, and the compiled declaration audit were not rerun. External source fidelity and upstream license evidence were not independently verified; this PR changes neither the project card nor its source attribution. The compatibility-only helpers are intentional, as stated by Vilin97.

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

[github-actions]

Proof profile (new / modified Lean files)

Statement changes

✅ No statements changed — all 1,409 tracked declarations across 14 modified files kept their type; only proofs / definition bodies changed.

Also: 12 declarations added, 0 removed. A reorganization moves declarations between files, which shows up here as an add in one file and a remove in another.

➕ Declarations added (12)

• DimdPolyLEAN.evalPkappa_lpNorm_eq_coefficient_norm — LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean
• DimdPolyLEAN.gaussianL2Norm_eq_lpNorm_from_measurability — LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean
• DimdPolyLEAN.norm_le_defect_add_two_of_norm_one — LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean
• DimdPolyLEAN.normalized_integral_cexp_quadratic — LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean
• DimdPolyLEAN.rankOneKernel_phase_of_ae — LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean
• HermitekLEAN.circleL2Sq_tendsto_partial_fourier_sums — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
• HermitekLEAN.circleSeries_l2_identity._proof_1_3 — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
• HermitekLEAN.norm_toLp_sq — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
• HermitekLEAN.summable_circle_continuous — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
• HermitekLEAN.summable_norm_sq_Phi_eval — LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean
• DimdPolyLEAN.ambiguityRep_eq_integral_of_ae_eq — LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean
• DimdPolyLEAN.ambiguityRep_schwartz_eq_integral — LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean

Statements are compared textually against the merge base (comments and whitespace ignored; by proof terms embedded in a type are treated as proof-irrelevant), the same method as physlib's /check-golf. Anonymous instances and examples are not tracked.

Compile cost of modified files — base → head

Heartbeats: 4,211,504 → 3,726,590 (-484,914, -11.5%). Commands: 1,141 → 1,152.

Per-file wall sum: 695.9 s → 602.5 s (-13.4%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal.

Files: 9 compared — 7 cheaper, 0 costlier, 2 within noise (threshold: |Δ heartbeats| ≥ 1,000 and ≥ 1%).

Both sides are elaborated against the merge-base build of the pool — sound when only proofs and definition bodies change; a file whose statements changed may fail there and is flagged ⚠. Heartbeats come from disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted to maxHeartbeats units. Failed measurements are not classified as cheaper or costlier. Δ lines counts added/deleted lines from this PR diff.

File	Δ lines	HB base	HB head	Δ HB	Δ HB %	Wall base (s)	Wall head (s)
LeanPool/PhaseRetrieval/DimdPoly/Internal/ImportedAnalyticInputs.lean	+91/-163	923,159	793,947	-129,212	-14.0%	143.80	137.54
LeanPool/PhaseRetrieval/Constant/Internal/HighFreqBandEstimate.lean	+22/-9	373,605	273,991	-99,614	-26.7%	47.31	27.79
LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseAnnulusEstimate.lean	+6/-86	366,850	280,655	-86,195	-23.5%	61.27	41.24
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/TrueLevelBasis.lean	+69/-100	945,215	869,993	-75,222	-8.0%	150.37	122.26
LeanPool/PhaseRetrieval/DimdPoly/Internal/ProductAnnulusLocalization.lean	+3/-21	151,291	83,022	-68,269	-45.1%	21.16	21.90
LeanPool/PhaseRetrieval/DimdPoly/Internal/FiniteBaseCircleEstimate.lean	+31/-247	514,853	498,815	-16,039	-3.1%	128.87	110.00
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/BasisLocalization.lean	+1/-1	610,572	603,028	-7,544	-1.2%	96.84	107.41
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermite1Dimd/ImportedAnalyticInputs.lean	+2/-2	323,816	320,997	-2,819	-0.9%	43.40	31.43
LeanPool/PhaseRetrieval/DimdPoly/Internal/Hermitek/ImportedAnalyticInputs.lean	+2/-3	2,142	2,142	-0	-0.0%	2.90	2.88
Total	+227/-632	4,211,504	3,726,590	-484,914	-11.5%	695.9	602.5

New files — absolute profile

Total heartbeats: — maxHeartbeats units across 0 valid files (163 added LOC).

Sum of lean --profile: — across 0 valid files. Import-excluded time: —.

Count-heartbeats wall-clock total: 0.00 s. Repeated import cost inside lean --profile: —.

Heartbeat values sum disjoint root command traces with trace.profiler.useHeartbeats and synchronous elaboration, converted from raw allocations to maxHeartbeats units by dividing by 1000. They include command elaboration and kernel checking, exclude imports, and include profiler overhead; they are not comparable to the deprecated linter's totals. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Commands	Errors
LeanPool/PhaseRetrieval/DimdPoly/Internal/CoefficientLimitRigidity.lean	36	—	—	—	—	—	116	1
LeanPool/PhaseRetrieval/DimdPoly/Internal/ExactModulusRecovery.lean	113	—	—	—	—	—	388	1
LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean	6	—	—	—	—	—	55	1
LeanPool/PhaseRetrieval/DimdPoly/Internal/PhaseStability.lean	2	—	—	—	—	—	31	1
LeanPool/PhaseRetrieval/DimdPoly/Internal/TensorBasis.lean	6	—	—	—	—	—	96	1
Total	163	—	0.00	—	—	—	686	5

Aggregate phase totals

Phase	Time
Unavailable	—

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[Vilin97]

Source review at 4c7374d.

{
  "summary": "The refactor shares ambiguity representative transport, rank-one recovery, Gaussian normalization and norm estimates, and reuses existing summability, continuity and arc-measure lemmas. Finite Parseval now uses the orthogonal Fourier family directly, while circle Parseval passes through continuous functions and their L2 map. The written contracts and existing data definitions are preserved, and typed congruence and explicit rewrite lists replace repeated broad normalization. The source changes improve reuse and make the analytic dependencies easier to follow.",
  "assessment": {
    "scope": "shared analytic lemmas and typed proof rewrites",
    "introduces_tech_debt": false,
    "maintainability": "improved",
    "brittleness": "more_robust",
    "risk": "low",
    "assessment_one_sentence": "The full14-file source delta preserves the existing written API/data and replaces duplicated analytic arguments with reusable proofs; no actionable maintenance regression was found."
  },
  "verdict": "approve",
  "findings": []
}

Coverage: the complete 14-file source delta and 70 hunks, including the generic almost-everywhere rank-one argument, Gaussian representative transport, finite/circle Parseval, and shared norm/summability suppliers. Existing written headers and non-theorem commands are preserved. The public profile has nine valid base-to-head comparisons (11.5% fewer heartbeats); five other file timings are unavailable. Profiling remains advisory.

Exact-head protected CI and the configured review remain separate requirements. The author's review-only instruction remains in force: no queue admission, merge or auto-merge.

[Vilin97]

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

Reviewed head: 4c7374da8a11f84e5222c5f1eab33e92a8e32006

Verdict: 🤔 needs_discussion

This extracts shared analytic lemmas and replaces broad normalization with typed applications while retaining the kernel and Parseval arguments' structure. The active proofs become more robust, and the recorded /profile comparisons are cheaper, but several replacements strand substantial private proof chains. Local compilation was blocked because fetching the pinned Mathlib revision returned HTTP 403.

Aspect	Value
Scope	analytic helper extraction and proof rewrites
Introduces tech debt	🛑 yes
Maintainability	✅ improved
Brittleness	✅ more_robust
Risk	✅ low

The active proofs improve, but preserving the private declaration inventory leaves substantial dead analytic code whose retention needs a maintainer decision.

Findings (1)

• dead-leftover — LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean:424
  Delegating here removes the last consumers of defect_lpNorm_eq_wip and evalPkappa_pointwise_bound_wip, leaving roughly 270 lines of private helpers without a consumer among the module's exported declarations, including the three cross-integrability proofs. Those independent analytic derivations still elaborate and require maintenance on dependency bumps. The same pattern strands oneDimPhi_phaseLaw_annulus in FiniteBaseAnnulusEstimate.lean. Remove the obsolete private chains, or retain required compatibility names as thin forwards to shared results instead of maintaining their old derivations.

---

Tokens: 1,656,406 in / 11,629 out · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $6.8001 (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]

Follow-up to configured review 2244 at 4c7374da8a11f84e5222c5f1eab33e92a8e32006 (comment 6316420685).

The dead-leftover finding is valid. My earlier source review checked the preserved contracts but missed the change in consumers. In the written consumer graph, OrthogonalCoercivity.lean:149–418 retains 15 private commands after the shared norm bridge disconnects their final exported consumers. The annulus phase-law derivation at FiniteBaseAnnulusEstimate.lean:1306–1352 likewise loses its last caller and duplicates the existing TensorBasis proof.

{
  "summary": "The active analytic proofs use shared results more robustly, but that rewiring strands a substantial private analytic closure. The concern is valid; preserving a stronger private-inventory target creates a real maintenance trade-off, and a domain-preserving cleanup is not entirely a mechanical one-line substitution.",
  "assessment": {
    "scope": "shared analytic helpers and private compatibility chains",
    "introduces_tech_debt": true,
    "maintainability": "improved",
    "brittleness": "more_robust",
    "risk": "low",
    "assessment_one_sentence": "The active proofs improve, while a newly orphaned private closure should be acknowledged or reduced without breaking its broader contracts."
  },
  "verdict": "needs_discussion",
  "findings": [
    {
      "file": "LeanPool/PhaseRetrieval/DimdPoly/Internal/OrthogonalCoercivity.lean",
      "line": 424,
      "rule": "dead-leftover",
      "comment": "The shared norm bridge removes the last consumers of defect_lpNorm_eq_wip and evalPkappa_pointwise_bound_wip, disconnecting15 private commands at149–418, including3 cross-integrability proofs. FiniteBaseAnnulusEstimate:1306–1352 similarly retains an identical private phase-law derivation after its sole caller switches to TensorBasis. Preserve old names/types/data if that is the chosen compatibility target, but expose and forward to matching already-proved suppliers where available; do not replace all-dimensional cross-integrability contracts by a positive-dimensional MemLp bridge. Otherwise document why this retained inventory cost is accepted."
    }
  ]
}

As maintainer, I accept this documented residual maintenance cost at the current revision. The active proofs now share established results, the refactor removes 733 lines overall, and the public mathematical contracts remain intact. Retaining the broader private inventory is the author's stated audit target; it is stronger than the repository's refactor requirements. It explains the choice but does not make the leftover proofs cost-free or turn the configured needs_discussion result into an approval.

A later cleanup should preserve the promised names/types and non-theorem data while sharing matching proof suppliers through explicit bridges. This is not uniformly a one-line substitution: the disconnected cross-integrability helpers quantify over all dimensions, whereas the available public MemLp bridge assumes 0 < d; some exact suppliers are private. Do not add that hypothesis or delete declarations merely to silence the finding. Any cleanup needs its own declaration audit and normal project validation.

The complete own-head CI run 39587734269, its canonical check 119223566291, and applicable required contexts are now verified. This does not relax the author's explicit instruction to keep this PR open for review, with no merge, auto-merge or queue entry.