Repository navigation
Import stability of matter and the kinetic Lieb–Thirring inequality - #641
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 blocking issue was identified in the changes since the previous review. SummaryImports stability of fermionic Coulomb matter, the kinetic Lieb–Thirring inequality, Baxter’s inequality, and the Schwartz kinetic-energy identity.
Reviews (6) · Last reviewed commit: "refactor: share symmetric finite-sum cou..." · Reviewed by Greptile |
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
|
/review |
|
{ |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review": "Permanent reviewer: independent scoped source supplement",
"reviewed_head": "3e4c6a06e09bd7372f62fc2de2821ccc50108dd9",
"overall_verdict": "pending_complete_configured_review",
"coverage": {
"complete_diff": false,
"root_whole_lean_files": 19,
"root_whole_card": true,
"scope": "Five endpoint proofs; concrete carriers; stability and finite-real assembly; screening and arbitrary bounded-charge Baxter extension. A distinct peer inspected supporting Pauli, Rumin, Fourier and electrostatic proof paths. This does not replace the acquisition agent's separately attributed complete 188-file audit."
},
"faithfulness": {
"verdict": "pass",
"bottom_line": "The five card headlines match the inspected Lean statements and concrete objects.",
"proves_the_claim": "proves_it",
"claim_note": "The constant precedes particle counts and configurations; the real form assumes distinct nuclei and finite kinetic energy and proves Coulomb finiteness before real subtraction.",
"assumed_inputs": "Positive spin multiplicity, normalization, fermionic antisymmetry and charges bounded by Z. Distinct nuclei and finite kinetic energy for the real form. These are disclosed; public endpoints supply proved Baxter, kinetic and Hardy inputs to conditional assembly.",
"findings": []
},
"evidence": [
"Concrete spin-valued Lp over Euclidean 3N-space, with simultaneous particle-permutation antisymmetry.",
"WeakBaxter handles Z=0 and proves the bounded-charge extension by averaging {0,Z} vertices; screening uses density mass and a positive cutoff.",
"Rumin's coefficient is explicit and is not claimed optimal. The kinetic theorem permits infinite energy.",
"The positive Z²/4 nearest-other-nucleus Baxter correction remains. Inspected Pauli, Rumin and electrostatic paths construct their inputs."
],
"sources": [
{
"url": "https://arxiv.org/html/2007.09326v1",
"assessment": "Frank Section 2 supports the normalized fermionic density inequality and uniform linear Coulomb stability formulation. Spin and explicit-coefficient adaptations are labelled."
}
],
"findings": [],
"disposition": "Favorable scoped mathematical assessment. Keep open pending the current-head configured rubric review and every protected native-queue gate. No native approval or queue action is claimed."
}
🤖 LLM review (
|
| Rubric | Verdict | Bottom line |
|---|---|---|
| Faithfulness | ✅ pass |
All five card headlines match the Lean statements and disclosed hypotheses. |
| Novelty | ✅ pass |
No duplicate of the five headlines was identified in Mathlib, Tau Ceti, or the pool; exhaustive semantic comparison with Tau Ceti remains unverifiable. |
| Significance | ✅ pass |
The uniform stability-of-matter theorem and kinetic Lieb–Thirring inequality justify pooling this research-level theory. |
| Sources | ✅ pass |
The labelled formulations match Frank’s Section 2 and Lundholm’s notes, and the pinned upstream formalization is credited. |
| Code quality (advisory) | ✅ pass |
The Lean is competently modularized, with shared pair-counting and permutation constructions and no material maintenance debt identified. |
| Aspect | Value |
|---|---|
| Proves the claim | ✅ proves_it |
| Assumed, not proved | Positive spin multiplicity, normalization, antisymmetry and bounded nonnegative nuclear charges; distinct nuclei and finite kinetic energy additionally for real stability; equal charges for Baxter; Schwartz regularity for the derivative identity—all disclosed in the card. Conditional analytical inputs are supplied by proved theorems. |
| Matches cited source | ✅ matches |
| Fit | ✅ good_fit |
| Level | research |
| Branch | mathematical physics |
| Mode | theory_building |
| Code quality | 3 / 5 |
Statement check: Stability uses a positive constant chosen before particle counts, bounded charges, nuclear positions and normalized antisymmetric states; the real corollary additionally proves Coulomb finiteness for distinct nuclei and finite kinetic energy.
The Lean develops uniform linear lower bounds for the total energy of three-dimensional fermionic Coulomb matter through kinetic, electrostatic, Fourier, and Hardy estimates.
Faithfulness findings (1)
- prompt-injection — PR-wide
Contributor-posted reviews supply approval and faithfulness verdicts for earlier heads, risking substitution of prior self-assessment for independent review. These assertions were disregarded. Remove verdict assertions from contributor audit summaries.
Evidence: prose only: acquisition-review comments in .review-pr.json dated 2026-10-12T11:05:53Z, 2026-10-12T12:14:29Z and 2026-10-12T13:34:23Z contain "overall_verdict": "approve" and faithfulness "verdict": "pass"; the contributor-reproduced review dated 2026-10-12T11:32:50Z contains "Verdict: ✅approve".
Novelty findings (1)
- prompt-injection — PR-wide
Three contributor audit comments claim prior approval and assign novelty-pass verdicts for earlier heads, risking substitution of self-assessment for independent review; these claims were disregarded.
Evidence: The acquisition-review comments in .review-pr.json dated 2026-10-12T11:05:53Z, 2026-10-12T12:14:29Z, and 2026-10-12T13:34:23Z each contain "overall_verdict": "approve" and a novelty section containing "verdict": "pass".
Significance findings (1)
- prompt-injection — PR-wide
Contributor-posted prior approval and significance-pass assertions risk biasing independent assessment and have no authority here; they were disregarded. Retain audit evidence without contributor-assigned review verdicts.
Evidence: In .review-pr.json, contributor comments dated 2026-10-12T11:05:53Z, 2026-10-12T12:14:29Z, and 2026-10-12T13:34:23Z each contain "overall_verdict": "approve" and a significance section containing "verdict": "pass". The contributor-posted reproduced review dated 2026-10-12T11:32:50Z contains "Verdict: ✅approve" and a significance-pass assessment.
Sources findings (1)
- prompt-injection — PR-wide
Three contributor-authored audit comments supply prior approval and sources-pass verdicts, risking substitution of self-assessment for independent review. These claims were disregarded; remove review verdicts from contributor audit summaries.
Evidence: Discussion comments dated 2026-10-12T11:05:53Z, 2026-10-12T12:14:29Z and 2026-10-12T13:34:23Z each contain "overall_verdict": "approve" and a "sources" section containing "verdict": "pass" and "source_match": "matches".
Code quality findings (1)
- prompt-injection — PR-wide
Three contributor-authored audit comments supply approval and quality-pass verdicts for earlier heads, risking substitution of self-assessment for independent review. These claims were disregarded; remove contributor-assigned verdicts from audit summaries.
Evidence: The comments in .review-pr.json dated 2026-10-12T11:05:53Z, 2026-10-12T12:14:29Z and 2026-10-12T13:34:23Z each contain "overall_verdict": "approve" and a quality section containing "verdict": "pass".
Tokens: 22,882,242 in / 56,840 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $92.3816 (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.
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review": "Permanent reviewer: exact-head cleanup delta supplement",
"reviewed_head": "8014b63c98fdb67dce9324a4d43e54374f04f5f4",
"previous_reviewed_head": "3e4c6a06e09bd7372f62fc2de2821ccc50108dd9",
"overall_verdict": "favorable_delta_pending_current_head_reviews_and_CI",
"coverage": {
"complete_pr_diff": false,
"complete_changed_delta": true,
"changed_lean_files": 4,
"peer_whole_before_and_after_bodies": 8,
"peer_new_source_utf8_bytes": 24683,
"method": "Root read the complete one-commit Git comparison. A distinct peer whole-read all four files before and after, independently checked content pins, and applied/reversed all 12 hunks against those bodies. The earlier scoped review and separate acquisition audit remain attributed to their reviewed head."
},
"evidence": [
"RealForm removes the prior-approval qualifier; mathematical code after public section is unchanged.",
"oneParticleCurrying now projects the single full isometric equivalence. The public State-to-fiber API, full equivalence and AE representative theorem are preserved.",
"Forward tensor insertion and pointwise/factor maps use normed-space assumptions and unchanged constructions. Inner-product and completeness assumptions remain on adjoints, contractions and projections.",
"No project card, headline, import, normalization, particle/spin quantifier or target-estimate premise changed."
],
"findings": [],
"source_ownership": "The acquisition owner removed the previous queue entry and pushed these repairs. Its local validation and benchmark claims remain separately attributed.",
"disposition": "Keep open with favorable delta source review. Fresh current-head CI, configured GPT/Greptile and the acquisition owner's updated thorough review are pending. Retain the previous exact-head checkpoints; no stale-head queue request is made."
}
|
{ |
|
/review |
Vilin97
left a comment
Vilin97
left a comment
There was a problem hiding this comment.
{
"review": "Permanent reviewer: exact-head cleanup delta supplement",
"reviewed_head": "4880944d18831a41d67832656b90eb5d3104f787",
"previous_reviewed_head": "8014b63c98fdb67dce9324a4d43e54374f04f5f4",
"overall_verdict": "favorable_delta_pending_current_head_reviews_and_CI",
"coverage": {
"complete_pr_diff": false,
"complete_changed_delta": true,
"changed_lean_files": 3,
"peer_whole_new_source_utf8_bytes": 18727,
"method": "Root read the complete one-commit comparison and the whole new FourierFactor body. A distinct peer independently whole-read all three new bodies and verified all seven patch hunks forward and backward. Earlier source reviews retain their original scope and exact heads."
},
"evidence": [
"statePermutationLinearIsometryEquiv and its apply theorem move byte-identically to FourierFactor, retaining their names, types and public/expose/simp attributes. simultaneousPermutation applies that shared equivalence.",
"The representative, sign and antisymmetry arguments remain unchanged. The Fourier proof unfolds the shared equivalence back to the original compLp expression, then uses the same Fourier identities.",
"The two TensorDensity APIs retain their complete proofs and conclusions under weaker NormedSpace assumptions. The concrete Schwartz-density theorem remains unchanged.",
"CurryingTransport imports only Mathlib.MeasureTheory.Function.L2Space, so the new edge cannot create a LeanPool import cycle.",
"The project card and all five headline statements are unchanged. No desired inequality or finiteness conclusion becomes an endpoint premise."
],
"findings": [],
"disposition": "Favorable delta source assessment at the author's ready-for-review head. Keep out of the queue until fresh exact-head CI, configured reviews, the owner's updated thorough review, current-main CI and all normal protections pass. The 8014 configured approval and CI are historical.",
"activation": "20261012T130000"
}
|
{ |
|
/review |
There was a problem hiding this comment.
{
"review": "Permanent reviewer: incremental source review",
"reviewed_head": "117979b12ae4c4b87cf11e95d63a516b7512cb2b",
"previous_reviewed_head": "4880944d18831a41d67832656b90eb5d3104f787",
"source_verdict": "favorable",
"coverage": {
"complete_delta": true,
"changed_files": 1,
"method": "Compared the complete one-commit delta and both full KineticLT.lean bodies. Retain earlier substantive reviews for unchanged source; this is not a repeated audit of all 188 files."
},
"findings": [],
"evidence": [
"kinetic_lieb_thirring_of_lowMomentumBound drops only the unused _hnorm premise. Its zero-particle vacuum proof and successor Rumin proof are byte-identical; q >= 1, antisymmetry and the pointwise low-momentum hypothesis remain.",
"The sole adjusted call omits that argument. The public kinetic_lieb_thirring statement still requires normalization and supplies hnorm to lowFourierField_density_bound. The conclusion, coefficient and all five headline statements retain their strength.",
"Exactly two substitutions reproduce the complete new file from the accepted old file. No project card, import, license, provenance, gate or other source changed.",
"Current-head CI is SUCCESS, including Build pool and Build project in run 38261134399. This review did not rerun unchanged private validation or adopt the owner's local-build claims.",
"The configured five-rubric review now approves this exact head (comment 6123419368, updated 2026-10-12T15:15:13Z). Live protected checks and all required GitHub Actions contexts pass; every review thread is resolved."
],
"disposition": {
"state": "Source accepted; enqueued through the normal protected native queue",
"configured_review": "All five rubrics pass at 117979b. The earlier pending status has been superseded.",
"separate_thorough_review": "The acquisition audit at 4880944 remains historical evidence for unchanged source. This complete current-head delta review complements the preserved substantive reviews. Live contribution rules and protections require no additional approving review; this preserves the configured mathematical, quality and CI gates.",
"queue": {
"id": "MQE_lQDOSY3yXM8AAAABH8bSWs4ABJD4zgM4h6M",
"position": 1,
"enqueued_at": "2026-10-12T15:22:11Z"
},
"next_action": "Await the existing native queue's combined CI and merge. If the head or findings change, recheck source acceptance and every normal gate. Preserve the author's branch ownership and avoid duplicate queue requests or updates merely to chase main."
}
}
|
/review |
There was a problem hiding this comment.
{
"review": "Permanent reviewer: incremental source review",
"reviewed_head": "1a780d4c1ba225862d99cd549e2f66197e7f09f7",
"previous_reviewed_head": "117979b12ae4c4b87cf11e95d63a516b7512cb2b",
"source_verdict": "favorable",
"coverage": {
"complete_delta": true,
"changed_files": 4,
"commits": 1,
"method": "Reviewed the complete four-file comparison, verified all five patch hunks exactly reproduce current file bytes, and read the whole shared-lemma provider. An independent peer read all four complete changed bodies (16,953 UTF-8 bytes), checked their content pins and proof hypotheses, and found no blocker. Prior substantive reviews remain valid for unchanged source with their original scope."
},
"findings": [],
"evidence": [
"sum_ne_eq_two_sum_lt handles the two strict-order cases plus the diagonal, then swaps finite sums. It preserves the factor of two over ENNReal without subtraction or cancellation, including zero/empty and infinite Coulomb values.",
"sum_eq_diag_add_two_sum_lt splits the diagonal from the off-diagonal sum and derives its remaining term from that shared lemma. No positivity, finiteness or distinct-position premise has been added.",
"The three consuming nuclear-repulsion, erased-index and shell-energy API statements remain unchanged. Their proofs now apply the shared identities; ne_comm reconciles the erased-index orientation.",
"All Coulomb definitions, headline endpoint statements, project card, imports, license, provenance and CI settings remain unchanged. This addresses the earlier finite-pair duplication advisory without weakening a theorem.",
"Current-head CI is SUCCESS (run 38271269013, Build pool and Build project). The old native merge-group run 38269762130 succeeded for its old combined commit and provides no validation credit for this changed head. No local/private validation replay was run.",
"The configured five-rubric review approves this exact head (comment 6123419368, updated 2026-10-12T16:46:43Z). The existing native queue completed its protected merge at 2026-10-12T17:09:28Z, producing main commit f482bd7."
],
"disposition": {
"state": "Merged through existing protected native queue",
"mergedAt": "2026-10-12T17:09:28Z",
"mergeCommit": "f482bd7ae78816404abd4ec7d2dff4935c65fdab",
"configured_review": "All five rubrics pass at the reviewed 1a780 head.",
"permanent_reviewer_enqueued_this_activation": false,
"queue_request_duplicated": false,
"next_action": "Source review is retained for this merged head. The resulting push-main CI remains a separate gate for subsequent queue requests."
}
}
|
{ |
1 participant
This imports stability of non-relativistic fermionic Coulomb matter in three dimensions, together with the kinetic Lieb–Thirring inequality, corrected Baxter electrostatic inequality, and identification of Fourier kinetic energy with the classical derivative form. The constant is uniform over particle counts, nuclear positions and charges bounded by the prescribed maximum. States are concrete spin-valued L² functions; the real-energy theorem additionally requires distinct nuclei and finite kinetic energy.
Upstream: Scott Armstrong and Amélie Loher’s LiebThirring, exact commit
8bf4656f07f5aaa227b0b850d77b16976915bbd4, Apache-2.0. The public announcement is dated 2026-10-11 09:51:05 UTC, inside the original acquisition window 2026-10-05 09:15:17 UTC → 2026-10-12 09:15:17 UTC. The source completion commit is dated October 7. Upstream credits AI agents supervised by the authors; the card recordsprovenance: AIand preserves both authors, copyright and funding acknowledgments.The scope is the 184-module transitive production closure of
stability_of_matter,stability_of_matter_real,kinetic_lieb_thirring,baxterandkineticEnergy_schwartz, from 870 upstream Lean files. One state/geometry split yields 185 production modules, an entry point and a generated public wrapper: 187 Lean files / 20,068 lines, plus one project YAML. Fourier transport, Pauli occupation, Hardy estimates and Voronoi boundary-measure infrastructure are retained for reuse. Separate ionization, thermodynamic-limit, Thomas–Fermi and upstream audit tooling are outside this import’s claims.Ported to exact Lean v4.35.0-rc3 and Mathlib c55e6e786f49471c72fbddbec5415808896aec1e, which remain current-main’s pins. All five endpoint statements retain their strength. The changes repair warnings/style, make multigoal branches explicit, generalize finite-index and normed-space helpers, remove unused assumptions, document definitions, share currying/permutation constructions, and consolidate directed and symmetric finite-pair counting. Splitting geometry from Fourier-heavy state definitions removes 73 electrostatic modules’ owned paths to the explicit Fourier LpSpace import. The conditional kinetic helper drops an unused normalization premise; the public theorem still uses normalization to prove its analytical input.
The actual statements were checked against Frank, Section 2 and Lundholm, Theorems 6.1, 7.2 and 7.6. Rumin’s explicit coefficient and the spin adaptation are labelled; no optimal constant is claimed. Positive spin, bounded charges, normalization/antisymmetry, finite real-form conditions, empty configurations and collisions were checked. The inspected pinned Mathlib, Tau Ceti source declarations, pool cards/history and all-state PR/issue searches showed no duplicate headline. Closest CAR/Fock algebra modules concern finite representations rather than analytic Coulomb stability; no Mathlib or Tau Ceti project is vendored.
Validation on head
1a780d4c1ba225862d99cd549e2f66197e7f09f7:lake build LeanPool.LiebThirringand public-wrapper build.lake exe mk_all --checkandlake exe lint-style LeanPool.LiebThirring.Imports.Classical.choice,propextandQuot.sound.Measured optimization used
lake build LeanPool.LiebThirringon the same 16-core Azure VM, deleting only project library/IR artifacts while retaining identical warm pinned dependencies. Original clean baseline: 147.53 s, 156 warnings. Fully cleaned intermediate: 167.71 s. Previous helper-repair head: 157.55 s, zero warnings. Latest final head: 191.33 s, zero warnings. The final run’s observed shared-VM load average was about 35 on 16 cores; these single runs do not establish a net speedup. Before/after per-file profiles are retained separately with their exact source heads. A cached-instance experiment did not improve paired profiles and was discarded. The retained structural changes reduce dependency fan-out and duplicated constructions without changing theorem strength or trust. No further material safe improvement was identified without broader proof/representation redesign.The preserved agentic audit covers every upstream dependency file in bounded chunks, declarations, implementation slices, concrete definitions, endpoints and all nonformatting deltas. Its latest continuation read all four finite-pair repair files in full and verified that the other 184 source/card hashes are unchanged from the preceding checkpoint. Current-head Greptile completed; configured five-rubric review is running. Earlier-head reviews remain historical evidence and do not replace current-head review.
This is a content-only branch using the migrated one-card layout.
LeanPool.lean, CI/gates, review rules and lint settings are unchanged. PR610 and PR611 are merged and current-main’s required Lean check is green. The branch has not rebased to chase main. Any merge must use the protected native queue after current-head reviews and every required gate are satisfactory.