Repository navigation
perf: speed up Burkholder majorant proofs - #454
Conversation
Optimize the two 10k-line majorant files of the Burkholder project (`MajorantPG2`, `MajorantPL2`) without changing any declaration. - Replace 42 `continuity` calls (aesop, 1.5-3.5 s each inside these crowded contexts) by explicit continuity terms. - Factor 38 private helper lemmas for facts that were re-proved inline dozens of times (`0 < a p`, `y < y / a p`, `a p * y < y`, sector membership of boundary points, denominator clearing, consequences of `2 ≤ p` / `1 < p < 2`, interior of `Icc`, quarter-plane exclusions, sector derivatives) and use them at ~600 sites. - Rewrite the `HasDerivAt` bookkeeping in the derivative lemmas with `hasDerivAt_id'`/`div_const`/`rpow_const` plus `congr_deriv (by ring)` instead of AC-normalising `simpa` calls. - Downgrade 84 `nlinarith` calls to `linarith` where that suffices, and drop `simpa` in favour of direct lemmas (`mul_lt_of_lt_one_left`, ...). Clean `lake build LeanPool.Burkholder`: 243 -> 188 user CPU seconds (-23%), 23.8 s -> 19.4 s wall. Declaration manifest (types, universes, safety, names of all 997 pre-existing declarations) unchanged. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
|
Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.  The PR appears safe to merge because the proof-only refactors preserve the public contracts and no actionable regression remains. SummaryThe PR refactors the two Burkholder majorant developments to reduce elaboration cost without changing their mathematical interfaces.
Reviews (5) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." |
Proof profile (new / modified Lean files)Statement changes✅ No statements changed — all 702 tracked declarations across 2 modified files kept their type; only proofs / definition bodies changed. Also: 39 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 (39)
Statements are compared textually against the merge base (comments and whitespace ignored; Compile cost of modified files — base → headHeartbeats: 2,652 → 2,808 (+156, +5.9%). Declarations: 663 → 702. Per-file wall sum: 141.0 s → 132.4 s (-6.1%). Wall clock is measured under parallel load and is noisy; heartbeats are deterministic and are the regression signal. Files: 2 compared — 0 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 Mathlib's
Advisory only — never blocks merge. Full log uploaded as the |
|
Exact-head review at What changes. Proof bodies only: 42 new Maintainability. Improved: explicit continuity terms and named elementary lemmas are more robust to Mathlib drift than Disposition. Nothing is requested of the author. Merge waits only for the required checks on this head: the Lean CI run is a cold ten-shard build because #450's new cache namespaces are still being seeded by |
|
Head moved to |
|
Auto-rebase stopped: this PR conflicts with |
1 similar comment
|
Auto-rebase stopped: this PR conflicts with |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
Independent refactor review at af9b64a739944724ab6d842149924eb73f5ea5bb: approve the content, quality 4/5. Shared parameter and region lemmas, explicit continuity terms and focused arithmetic replace repeated heavy solver setup while preserving proof structure. The prior profile reports all 702 tracked types preserved; its +5.9% heartbeat change is below the profiler's material threshold, and noisy per-file wall time fell 141.0 → 132.4 s. No material regression established.
This cycle repaired the main/module migration conflict in an isolated worktree, preserving the public-import layout and the explicit arithmetic proofs already on main. The final 3,036-job project build, semantic lint, full-root style, index, repository static scans and axiom/environment audit pass. The remote head was checked before the fast-forward push. Fresh whole-pool CI is now running its quality checks. The configured LLM workflow dispatch returned HTTP 422 (disabled); this is the independent exact-head refactor review, not a claim that workflow ran. Equivalent approval comment because GitHub forbids self-approval. Normal protected merge remains conditional on final exact-head CI/mergeability checks; no override.
Vilin97
added
the
needs-maintainer
|
Disposition: merged at reviewed head |
Vilin97
removed
the
needs-maintainer
1 participant
Summary
Daily optimization cycle, target project:
LeanPool/Burkholder(Burkholder's sharp martingale-transform inequality, provenanceAI). Base:b2041a8152d6667dc61e9119b8654d36d77aa391(origin/mainat the start of the cycle;LeanPool/Burkholder, the toolchain and the manifest are unchanged onmainsince then).Why this project: among nine candidates built and timed from cold (
CompactnessAndDegeneracy,Burkholder,NonSoficGroup,Vlasov,EhrhartVolumeInequality,SpherePacking,PhaseRetrieval,HadwigerNelsonBounds,QuantumParallelRepetition), Burkholder had the densest cost: 95 % of its 242 CPU-seconds sit in two twin 10k-line files (MajorantPG2,MajorantPL2, thep > 2and1 < p < 2regimes) made of ~330 private lemmas each that re-prove the same elementary facts inline hundreds of times. PhaseRetrieval has a larger total (694 CPU-s) but spread over 43 measure-theoretic files with many public declarations.Only
MajorantPG2.leanandMajorantPL2.leanchange. No definition, statement, name, universe list, safety level, instance/simp/reducibility attribute or import changes; no gate, waiver,set_option,sorry,native_decideor new axiom.Invariant audit
Method: a Lean script (
importModules LeanPool.Burkholder, run against a copied olean directory so rebuilds cannot race it) prints, for every constant whose module starts withLeanPool.Burkholder: kind, safety, reducibility hints, universe params, reducibility status, instance flag/priority, simp flag, protected/private flags, inductive/ctor/recursor metadata, the type hash and the fully explicit pretty-printed type (pp.explicit,pp.universes,pp.privateNames,pp.instances, ...), plus value hashes for defs; theorem proof hashes go to a side file. Run at the base commit and at the head, then diffed.Result: base 997 declarations, head 1015.
Majorants.exists_majorant_geTwo,Majorants.exists_majorant_leTwo,Majorants.exists_majorant_p_eq_2,Majorants.exists_majorant_p_g_1,MeasureTheory.Lp_Burkholder_inequality_martingaleTransform, alldefs and notations).simpauxiliaries (<lemma>._simp_1_N): 22 removed and 1 with a different type, all children of private lemmas whosesimpcalls were replaced. Alldefvalue hashes are unchanged.private lemmas below and 1_simp_auxiliary.exists_majorant_geTwo, whosehave-levellinarithone-liners now use the helpers); its statement is byte-identical.What changed (both files, same patterns)
continuity→ explicit terms (42 sites). In a scratch filecontinuitytakes 0.1 s, inside these proofs 1.5–3.5 s (aesop normalising a context with ~30 hypotheses andlet-bound sets).Continuous (fun z => (-z.1, -z.2))is nowcontinuous_fst.neg.prodMk continuous_snd.neg,fun t => (t, y)iscontinuous_id.prodMk continuous_const, etc.MajorantPL2re-proved0 < a p57 times (rw [a_eq_leTwo]; exact div_pos (by linarith) (by linarith)),y < y / a p33 times (withnlinarith),a p * y < y40 times (simpa using mul_lt_mul_of_pos_right), boundary-point sector membership 50+ times;MajorantPG2re-derivedy < xfromA2,¬ QuarterPlane/¬ QuarterPlane2facts (54 sites),t ∈ Set.Ioofrominterior (Icc)(90 sites in both files), and the derivative ofvGeTwoonclosureA2(11 sites). These are now single private lemmas (a_pos_of_one_lt_of_lt_two,lt_self_div_a_leTwo,mul_a_lt_of_lt_div_a,closureA2_diag_leTwo,quarterPlane3_mul_a_leTwo,lt_of_lt_mul_a,not_quarterPlane_of_neg,mem_Ioo_of_mem_interior_Icc,hasDerivAt_vGeTwo_x_DxauxFunction1, ...). Elementary consequences of2 ≤ p/1 < p < 2(0 < p,0 < p - 1,p ≠ 1, ...) are stated once and used as terms at 177 sites instead ofby linarithin contexts whose division-heavy hypotheses make eachlinarithcall cost 50–300 ms ofcancelDenomspreprocessing. InMajorantPG2the threea plemmas moved above their first use so the earlier lemmas could use them.HasDerivAt (fun s => (s + y) / 2) (1 / 2) tis((hasDerivAt_id' (x := t)).add_const y).div_const 2instead ofsimpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using ...;rpowderivatives useReal.hasDerivAt_rpow_const/HasDerivAt.rpow_constwithcongr_deriv (by ring)(or arw [show p - 1 - 1 = p - 2 by ring]) instead of AC-normalisingsimpaandconvert ... using 2(95 blocks).nlinarith→linarithwhere linear reasoning suffices (each kept only when it compiles);simpa using mul_lt_mul_of_pos_right h hx→mul_lt_of_lt_one_left hx h;dsimp [c]; field_simp→mul_div_cancel₀; two hand-rewritten steps invLeTwo_A2_second_bracket_nonpos_leTwo(mul_div_cancel₀,mul_le_mul_of_nonneg_rightinstead offield_simp/linarith [...]).Net: −1069 lines (PG2 10682 → 10213, PL2 10023 → 9423);
continuity42 → 0,nlinarith105 → 21,linarith1369 → 1114,simpa838 → 553,field_simp141 → 111.Measurements
Machine: 32-core WSL2 host, otherwise idle; Lean v4.34.0 / Mathlib
5ed29652as pinned by the repository. Clean builds delete.lake/build/{lib/lean,ir}/LeanPool/Burkholder*first; base and head were built back to back on the same oleans.lake build LeanPool.Burkholder(clean)b2041a81Per file, sequential
lake env lean -DmaxSynthPendingDepth=3 -Dweak.linter.mathlibStandardSet=true <file>(user CPU s, base → head):MajorantPG2121.5 → 93.8 (−22.8 %),MajorantPL2131.1 → 80.3 (−38.8 %);Definitions,MajorantPEq2,Majorants,MartingaleTransforms,Burkholderunchanged (1.2–6.5 s each). Profiling used-Dtrace.profiler=true -Dtrace.profiler.threshold=20; the biggest single items werecontinuity(aesop) and the repeated inline blocks listed above.Checks run (all green)
lake build LeanPool.Burkholder— 0 warnings, 0 errors (the threeinfo: Try this: ring_nfnotes are pre-existing onmain).lake exe runLinter LeanPool.Burkholder— "Linting passed".lake exe lint-style LeanPool— no output.lake exe mk_all --check— "No update necessary".python -m lean_pool.qualitypieces scoped to the project: textual gates (headers, forbidden text, sizes, proof sizes, cards) — 0 errors for Burkholder;#print axiomsaudit of the project declarations — 0 errors (onlypropext/Classical.choice/Quot.sound); environment option-backdoor audit overLeanPool.Burkholder— 0 errors.Limitations
linarithcalls at 20–200 ms each (dominated bycancelDenomspreprocessing of/ 2hypotheses) and ~550simpacalls; the next step would be per-sitelinarith only [...], which is not safely automatable.LeanPool/Burkholderis touched; generated indexes needed no change.🤖 Generated with Claude Code