Repository navigation
Import analytic Hamiltonian KAM on compact action domains - #632
Conversation
|
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 remaining code finding blocks the latest cleanup; this is not a full merge approval because external source checks and dependency-wide novelty remain unverified. SummaryImports the analytic Hamiltonian KAM development, including the global theorem, infinite iteration, and noninjective-frequency examples.
Reviews (2) · Last reviewed commit: "Reuse shared frequency derivatives and p..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
Proof profile (new / modified Lean files)
This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget. Total heartbeats: 2,664,472 maxHeartbeats units across 148 valid files (17,238 added LOC). Sum of Count-heartbeats wall-clock total: 686.75 s. Repeated import cost inside Heartbeat values sum disjoint root command traces with LOC counts added lines in the profiled Lean files from this PR diff.
Aggregate phase totals
Slowest changed modules (from
|
| Changed module | Lake time |
|---|---|
LeanPool.ArnoldKAM.Arnold1963.Analysis.ParameterIntegral |
5.50 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.FourierKernel |
5.30 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.FourierParameter |
4.40 s |
LeanPool.ArnoldKAM.Arnold1963.Basic.Spaces |
3.60 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.AnalyticLift |
3.50 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.SecondCauchy |
3.50 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.Taylor |
3.40 s |
LeanPool.ArnoldKAM.Arnold1963.Audit.FundamentalExample |
3.40 s |
LeanPool.ArnoldKAM.Arnold1963.Analysis.Cauchy |
3.30 s |
LeanPool.ArnoldKAM.Arnold1963.Geometry.GradientBounds |
3.30 s |
LeanPool.ArnoldKAM.Arnold1963.Basic.SymplecticMatrix |
3.20 s |
LeanPool.ArnoldKAM.Arnold1963.Geometry.SlabMeasure |
3.20 s |
Comment truncated to fit GitHub's 64 KB limit. This PR profiles 148 files; the per-file table shows only the 148 hottest by heartbeats. The full table and raw
lean --profileoutput for every file are in the run's step summary andproof-profileartifact.
Advisory only — never blocks merge.
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review_kind": "Separate thorough agentic review under .github/REVIEW_RULES.md and the acquisition selection/engineering requirements",
"reviewed_commit": "7ddd4edd90f5197964623fe39ffea9045c6e037f",
"conclusion": "approve",
"coverage": {
"upstream_commit": "69c10c07bcd0a65f8965bc58c37eea2700bafafb",
"source_files": 148,
"method": "Bounded packets covered every retained file, its imports, declarations, data fields and representative implementation slices; the principal interfaces and construction chain were also read in full. The entire semantic port diff and subsequent four-file cleanup diff were inspected. No elided file was accepted as reviewed.",
"closure": "All 148 Lean modules are reachable from the generated public wrapper; retained upstream proof modules number 146. The two-branch examples and reusable Fourier, resonance, analytic transformation and iteration infrastructure remain."
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "The card accurately describes the restricted compact-domain KAM theorem proved by the Lean endpoint.",
"proves_the_claim": "proves_it",
"claim_note": "theorem1 chooses a positive threshold before quantifying over analytic perturbations and constructs a compact positive-volume good set, strict relative exceptional-measure bound, pairwise disjoint analytic nonresonant invariant tori, and all-real-time trajectories of the original perturbed Hamiltonian.",
"assumed_inputs": "Positive dimension, compact conjugation-stable complex action domain, analytic real-compatible unperturbed Hamiltonian, a nonempty real open interior whose closure is the real slice and whose boundary is null, interior complexification, nonzero Hessian determinant, and positive width/tolerance. The card discloses the domain and nondegeneracy restrictions. Quantitative Diophantine and Lagrangian conclusions are explicitly excluded from its claims.",
"findings": []
},
"novelty": {
"verdict": "pass",
"bottom_line": "No duplicate headline was found in Mathlib, TauCeti or the pool.",
"already_formalized": "",
"novelty_note": "Searches of pinned Mathlib, live Mathlib code-search hits, pinned/current public TauCeti sources, pool project cards, 1,000 PR records, targeted issues and source history found no corresponding KAM endpoint; the SU(2) torus and three-body perturbation hits were inspected and concern different statements. This is a preservation/duplicate assessment, not a worldwide priority claim.",
"findings": []
},
"significance": {
"verdict": "pass",
"bottom_line": "This is a substantial completed dynamical-systems formalization with reusable analytic infrastructure.",
"fit": "good_fit",
"level": "research",
"branch": "Hamiltonian dynamics",
"mode": "mixed",
"significance_one_sentence": "The coherent proof development constructs invariant tori and global measure estimates for small perturbations of nondegenerate analytic Hamiltonians, including localization without global frequency injectivity.",
"findings": []
},
"sources": {
"verdict": "pass",
"bottom_line": "The pinned source and archived software support the explicitly restricted theorem and its attribution.",
"source_match": "matches",
"findings": []
},
"quality": {
"verdict": "pass",
"bottom_line": "The modular dependency closure passes the required local gates and the measured optimizations improve its elaboration cost without weakening results.",
"code_quality": 4,
"findings": []
},
"source_and_license_evidence": {
"repository": "https://github.com/ybq1415926-droid/arnold1963-kam",
"public_release": "v0.1.0, 2026-10-07T02:48:05Z",
"archive": "https://doi.org/10.5281/zenodo.23232025",
"archive_check": "The Lean source at the pinned commit is identical to the v1.0.0 tag; the retrieved Zenodo API record identifies the software, author and Apache-2.0 license. The actual repository LICENSE was inspected.",
"historical_source": "Arnold 1963, DOI 10.1070/RM1963v018n05ABEH004130; the original theorem section was read through MathNet. The card does not claim every conclusion or scope of the historical theorem.",
"attribution": "Bingqi Yu; upstream AI proof-production disclosure is recorded as provenance AI, with human mathematical direction distinguished from generated/revised Lean."
},
"semantic_checks": {
"inputs": "GlobalHamiltonianData contains genuine analytic/domain/nondegeneracy hypotheses, with no field postulating the KAM conclusion or a global inverse frequency map.",
"objects": "KAMTorus stores actual analytic maps and closed embeddings into the real phase space, tied to the original vector field; no surrogate invariant relation replaces the Hamiltonian equation.",
"nonvacuity": "The cubic unperturbed Hamiltonian on the two disjoint real neighborhoods has nonzero Hessian and equal frequencies at distinct centers; a nonconstant cosine perturbation is instantiated, and the examples produce tori in both branches.",
"construction": "Inspected the Fourier/homological estimates, generating transformations, local step and infinite iteration, finite localization and global measure assembly. Cross-chart disjointness uses original-ODE uniqueness and dense orbit closures."
},
"engineering_and_validation": {
"trust": "The unmodified axiom audit found no prohibited dependencies among 1,365 parsed public declarations; the imported-environment/backdoor audit found none. No sorry, admit, native_decide, unsafe, partial, diagnostic command, option override, waiver or changed gate is present.",
"local_gates": "Clean build at this exact commit: exit 0, no warnings. Generated-index check, style, whole-repository static quality, declaration/card audits, and all 15 slow Mathlib linters on 148 modules / 2,736 declarations passed. Content-only and whitespace checks passed; Python source was unaffected.",
"controlled_performance": "With pinned cached dependencies and only this project compiled/IR artifacts removed, lake build LeanPool.ArnoldKAM.Imports measured 183.153 s at the compatibility baseline and 153.204 s at this head (16.35% observed improvement on the shared VM). Source hashes before/after the final build were identical.",
"profile": "remainder_budget synchronous declaration time fell from 12.316 s to 1.461 s; the derivative proof that previously timed out under synchronous profiling now passes in 0.931 s at default heartbeats. No material safe additional optimization was identified in the inspected remaining modules.",
"repairs": "Mathlib API/public-module port; removed diagnostic/training wrappers; narrowed tactic imports; restricted arithmetic tactics; explicit derivative types; documentation and naming repairs; removed redundant simp attributes/unused class assumptions; consolidated action-frequency derivative and phase-direction infrastructure in response to Greptile. Important APIs and theorem strength are preserved.",
"ci": "Lean Action CI run 38045618762 completed successfully for this exact head: https://github.com/LeanPool/lean-pool/actions/runs/38045618762. Build, warning, index, Mathlib linter, style, repository quality/trust and required compatibility gate passed. Documentation preflight, scope/content separation and workflow checks also passed; unrelated Python/minimal-verifier paths were skipped by their normal path filters."
},
"review_separation": "This source/diff review is separate from the configured GPT five-rubric worker and Greptile. It does not stand in for either automated review. The normal merge queue remains conditional on current-head CI and all reviews completing without unresolved material findings."
}
|
/review |
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All three card headlines match the Lean statements and construction. |
| Novelty | ✅ pass |
No inspected Mathlib, Tau Ceti, or pooled declaration subsumes the three headlines; broader Tau Ceti semantic coverage remains unverifiable. |
| Significance | ✅ pass |
The analytic Hamiltonian KAM theorem and its supporting analytic and dynamical theory are a good fit for the pool. |
| Sources | ✅ pass |
The cited archive supports the stated KAM variant, and the upstream Lean formalization is explicitly credited. |
| Code quality (advisory) | ✅ pass |
The code is competently modularized, with shared derivative helpers and no material maintenance issue identified. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | GlobalHamiltonianData supplies positive dimension, compact conjugation-invariant geometry, a nonempty open real action set with null boundary whose closure is the real slice and whose complexification lies in the domain interior, analyticity, reality and Hessian nondegeneracy. Perturbations are bounded, periodic, real-compatible analytic functions. These specify the card’s domain and Hamiltonian scope; charts, iteration and tori are constructed. canonical_pullback assumes differentiable symplecticity and mapping into the phase domain. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | Hamiltonian dynamics |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: The global theorems choose a positive threshold before the perturbation and construct the claimed disjoint torus partition, strict relative measure bound and all-time trajectories of the original Hamiltonian; canonical_pullback proves the derivative pushforward identity.
The project proves persistence of a large-measure family of analytic invariant tori under small Hamiltonian perturbations, developing Fourier estimates, canonical transformations, infinite iteration, measure control, and all-time trajectories.
Tokens: 16,622,064 in / 47,317 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $67.1980 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.
1 participant
This imports a completed nondegenerate analytic Hamiltonian KAM theorem: a uniform positive perturbation threshold produces a compact positive-measure set partitioned into disjoint analytic invariant tori, with a strict relative measure-loss bound and trajectories of the original perturbed Hamiltonian for every real time.
Source, eligibility and scope
69c10c07bcd0a65f8965bc58c37eea2700bafafb.[2026-10-03 09:15:19, 2026-10-10 09:15:19)UTC window. Eligibility uses the public release, not repository refresh metadata.docs/PROVENANCE.md.Imports.leanwrapper. This is the dependency closure of the global theorem, its iteration interface and the substantive cubic/noninjective-frequency examples. Training modules, audit print commands and progress wrappers are excluded.The global theorem's explicit hypotheses include a positive dimension, a compact conjugation-invariant complex action domain, and a nonempty open real action set whose closure is the real slice, whose boundary is null, and which complexifies into the domain's interior. The unperturbed Hamiltonian is analytic and real-compatible with nonzero Hessian determinant on that real open set. The threshold is chosen before the perturbation. Global frequency injectivity is not assumed. The final torus interface states nonresonance, an analytic lift, closed embedding, injective derivative, small displacement, angle invertibility and all-time Hamiltonian trajectories; it does not additionally claim a quantitative Diophantine bound or the Lagrangian property.
This is a substantial result in Hamiltonian dynamics suited to preservation as a coherent project. Its reusable infrastructure includes normalized torus Fourier analysis, contour shifts, Cauchy bounds, analytic generating transformations, frequency-chart inversion, resonance measure estimates, infinite iteration and cross-chart orbit-closure arguments. Public-source and repository-history searches found no corresponding KAM development already in Mathlib, TauCeti, Lean Pool, its PRs or issues; unrelated torus and Hamiltonian-perturbation hits were inspected.
Port and engineering changes
Ported Lean 4.33.1/mathlib 4.33.1 to the pool's Lean 4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e. The port updates deprecated imports/lemmas, adopts public module imports, wraps private proof helpers appropriately, and repairs tactic focus and simp normal forms. Copyright and authorship are retained. English module documentation and 366 API/data-field docstrings describe the construction and its conventions.
Removed upstream option overrides and diagnostic commands. Removed two unnecessary typeclass assumptions, making the affected lemmas more general; retained every important theorem and the strength of the three advertised results. Added explicit derivative types, replaced broad nonlinear arithmetic with restricted linear/nonlinear calls, narrowed broad tactic imports and eliminated avoidable dependency fan-out. Greptile’s duplication finding is repaired by sharing
actionFrequencyCLMand its derivative theorem from the definition module and makingphaseBasisan alias ofphaseDirection. The fixedLeanPool.lean, infrastructure, checks and configurations are unchanged.Validation and measured performance
Controlled clean project build: remove only the imported project's
.lake/build/lib/leanand IR artifacts, retain the exact pinned Mathlib/dependency artifacts, then runlake build LeanPool.ArnoldKAM.Importswith default Lake scheduling on this 16-logical-CPU Azure VM. The VM is shared, so timings include ordinary load variation.The controlled baseline was recorded after compatibility porting and before substantial optimization, with its source snapshot retained for reproduction. Optimizations reduced
FundamentalParameters.remainder_budgetsynchronous profiler time from 12.316 s to 1.461 s. Explicit derivative types madeiteratedDeriv_two_line_eqpass synchronous profiling in 0.931 s; its former inferred term timed out at the default 200,000-heartbeat limit. No heartbeat override is present.Local checks passed:
lake exe mk_all --check.lake exe lint-style LeanPool.ArnoldKAM.Imports.All retained upstream files were reviewed in bounded source packets covering imports, declarations, structure interfaces and implementation slices, with deeper inspection of the endpoint definitions and the construction/dependency chain. The port's code-body diff was separately inspected in full. CI and the configured Greptile/GPT reviews remain the final external checks; a separate thorough review will record its exact reviewed head on this PR. Enqueueing will use the validated native queue only after the required checks and reviews pass.
Exact locally validated head:
7ddd4edd90f5197964623fe39ffea9045c6e037f. The earlier head02229606abfc2fc873681c56279d75cb07bed3b0passed Lean Action CI before this cleanup; CI and configured reviews must validate the current head.