Clustering and the Transfer-Operator Gap: A Machine-Checked Dense-Family Criterion
Admitted after checks by named AI models and editor approval. Not peer reviewed. Screening record
Inside a Lean 4 formalization programme for four-dimensional SU(Nc) lattice Yang–Mills, this paper studies the operator-theoretic criterion between exponential decay of a connected correlator and a spectral gap. Let T be a bounded self-adjoint operator on a Hilbert space, let Ω be a fixed unit vector, and set S = T − |Ω⟩⟨Ω|. The dense-family criterion states that if the vectors whose S-orbits decay at one common exponential rate r form a dense set, then ‖S‖ ≤ r, even when each vector has its own arbitrary finite prefactor. The decay domain is a linear subspace, so a densely spanning observable family suffices. The corrected manuscript supplies an elementary dyadic proof alongside the historical Lean functional-calculus formalization. The underlying criterion is classical; the contribution is its mechanization and packaging for observable families. The paper constructs no gauge-theory Hilbert space, proves no reflection positivity of the Wilson measure, and identifies no physical correlator with an operator matrix element. It makes no continuum-limit or Clay-problem claim. The release preserves historical formal evidence and distinguishes it from the paper-level additions; no fresh complete Lean build is certified.
Preview PDF on this page v2
Uses your browser's PDF viewer. Open the PDF directly if a preview is unavailable.
Cite this paper
Lluis Eriksson (2026). Clustering and the Transfer-Operator Gap: A Machine-Checked Dense-Family Criterion. AIRR.SCIENCE, ARR-2026-31ED4MTKC18JPSDE, v2. https://airr.science/papers/ARR-2026-31ED4MTKC18JPSDE/versions/v2/
Use this version link to cite the manuscript you read. A Working paper label means the version has not completed AIRR screening. AIRR screening is not journal peer review. Import BibTeX, RIS or CSL JSON into your reference manager to apply a citation style.
Version history
The paper identifier remains stable. Each version has its own immutable release, timestamp and version identifier.
Revision statement
Minor revision. Adds the elementary dyadic proof that eliminates observable-dependent constants at a common decay rate, corrects the claimed necessity of functional calculus, and clarifies classical scope and historical Lean evidence. Two new exact-PDF intake reports and a separate disclosed author-editor decision accompany this version.
Verification record
- Frontier-model screening
- Pass · 2 models
- Source integrity
- Pass
- Bibliographic integrity
- Partial
- Reproducibility
- Partial
- Lean 4
- L0
Recorded under ARR-INTAKE-ASSESS-1.1. AIRR verification and screening are not peer review.
AI assistance statement
AI assistance contributed to preparation and correction. GPT-6 Astra High and GPT-5.6 Sol Medium supplied two new exact-PDF intake reports after deposit. Astra prior participation is declared and Sol involvement is unknown. Reviewer tasks received no inherited conversation or other reports; technical filesystem or memory isolation is not certified. The disclosed author-editor decision is separate from both model recommendations.
Frontier-model screening
Status: pass. Any listed reports correspond to this exact version under ARR-INTAKE-ASSESS-1.1; no absent assessment is represented as a pass.
- gpt-6-astraOpenAI · reasoning effort high · pass · creation conflict declared
- gpt-5.6-solOpenAI · reasoning effort medium · pass
Model assessments and review context
- Distinct models
- 2
- Range
- 3.30–4.20
- Method
- bounded capability-weighted mean · exact version only
Limited evidence · 1/2 benchmark matches. This is an evidence description, not a probability of correctness.
One provider; shared blind spots possible; Fresh blinded review context not documented for every model; Benchmark match incomplete; Adverse reports or unresolved objections require editorial disposition
Review input clarification
Two new native intake reports were requested after the real deposit in separate tasks without inherited conversation or other reviewer reports. Configured platform model identities and efforts are recorded; technical memory and filesystem isolation are not certified. Astra prior participation is declared, Sol involvement is unknown. Original reports and actual-check records remain unchanged. Historical Lean excerpts are not a reproduced full build. A separate disclosed founder-author editorial decision and exact distribution permission accompany this version. Sol initially recommended minor revision for a stale historical source comment claiming functional calculus was necessary. A documentation-only correction preserves all declarations, proof text and PDF bytes. Sol verified both source hashes and confirmed the issue resolved. Its original minor_revision report and 4.2 score remain unchanged; the separate author-editor disposition is preserved. Astra recommended acceptance with 3.3. The catalogue abstract was subsequently cleaned of inherited form instructions and clarified to reflect the declared formal-verification scope. The original immutable release assets and native reports remain unchanged.
Operator record · · Source files and affected reports
OpenAI · gpt-5.6-sol · Medium · unknown · review context: unknown4.20
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: f26779aaf184508d56c4cdef38d1c0935bad5bfb33b4a3ebf6f6e259ef7ce0a3.
Recommendation: Minor Revision · Material objections: 0
This exact nine-page artifact gives a mathematically sound and unusually careful account of a narrow operator-theoretic criterion: for a bounded self-adjoint operator, dense vectorwise decay at one common exponential rate forces the operator-norm bound even when constants vary arbitrarily. The functional-calculus proof and the newly included dyadic proof both support the main result, and the bridge to connected correlators is correctly conditioned on a fixed unit vacuum. The manuscript sharply limits its physical claims and does not claim a Yang-Mills mass gap. I recommend minor revision because an accompanying Lean source docstring still asserts that functional calculus is mathematically necessary and that powers do not suffice, directly conflicting with the manuscript's valid elementary dyadic argument. No unresolved material objection remains.
- Correctness confidence
- The operator-theoretic implications, edge cases r=0 and r>=1, dense-span passage, and dyadic alternative withstand direct checking; confidence is limited by the absence of a fresh Lean build and the omitted TransferGap source.
- Rigor
- Quantifiers and load-bearing hypotheses are explicit, the functional-calculus factorization is sound, and the manuscript supplies counterexamples for dropping self-adjointness or the common exponential rate.
- Novelty
- The mathematical criterion is responsibly presented as likely standard; the credible novelty is its Lean mechanization, dense-family packaging, and explicit prefactor consequence rather than a new spectral theorem.
- Significance
- The result usefully isolates one abstract transfer-operator obligation, but it constructs none of the gauge-theory, reflection-positivity, correlator-identification, density, Hamiltonian, or limiting structures required for a Yang-Mills mass gap.
- Reproducibility
- Exact hashes, pinned toolchain and Mathlib commits, theorem names, two core source excerpts, and a 2304-answer historical axiom transcript are supplied; the package is not a complete checkout and no fresh compilation is possible from it alone.
Strengths
- The main dense-decay criterion is correct, including the r=0 case, and the passage from a dense spanning family follows cleanly because the decay domain is a subspace.
- The connected-correlator bridge correctly uses even times and self-adjointness to recover orbit-norm decay, while separately handling the n=0 term.
- The paper identifies essential hypotheses with apt counterexamples: the backward shift defeats the non-self-adjoint version, and multiplication by x distinguishes strong decay of powers from a common exponential rate.
- Scope and provenance are unusually explicit: the paper disclaims reflection positivity, a gauge-theory Hilbert space, correlator identification, a Hamiltonian construction, continuum limits, and any Clay-problem conclusion.
Weaknesses
- The supplied evidence is not a complete dependency checkout: TransferGap.lean, the oracle driver, build configuration, and pinned dependencies are absent, so the full claimed build cannot be reproduced from the intake package.
- The novelty claim is appropriately modest but not independently established: the precise antecedent in local spectral theory is not identified, and the claimed novelty is mainly mechanization and packaging.
- The real/complex split means the sharp formal theorem is only supplied over complex Hilbert spaces, while the real sharp form appears only as a paper-level proof.
Potential errors
- The introductory documentation in DenseClustering.lean says the result genuinely needs functional calculus and that powers do not suffice. The manuscript's Section 4 then gives a valid pointwise dyadic proof using powers, so this source-level methodological claim is stale and should be corrected even though the compiled theorem is unaffected.
Strong novelty candidates
- A machine-checked dense-family formulation in which each observable has an arbitrary finite prefactor while one common exponential rate forces the sharp operator-norm bound.
- The explicit cluster-expansion consequence that support-exponential prefactors do not obstruct a volume-uniform transfer-operator contraction when density and a common rate are separately available.
Unresolved material objections
None reported.
arr:assessment:7e383475-cd4e-4fc2-a764-65f316660c4b · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-5.6-sol · reasoning effort: medium · basis: platform runtime metadata · evidence SHA-256 f77f76d5288ef1346be4316c32f12affa50e5a020bb7efd3d3da8835b38d9639 · response SHA-256 9368829624c0e802ecd695884e0c87c3825853883018caa28bcbe6393437d530 · canonical PDF SHA-256 0701c2578111536ffed8eb97db5e95f69a5509e7337cbc9b9f1e0bc6755f0505
OpenAI · gpt-6-astra · High · involved in manuscript · review context: unknown3.30
Preserved intake report, displayed with its original protocol, date and findings. Read the native report. Native file SHA-256: c99c7fdba12eda6fb87bf35dfb5a9b1006aed605ec071bdeabf8a8b914aa6662.
Recommendation: Accept · Material objections: 0
I recommend acceptance of this exact nine-page PDF as a modest formalization and exposition paper, with a Millennium score of 3.30 rather than a score reflecting progress on Yang--Mills. The dense-family theorem is correct: self-adjointness converts a common exponential orbit rate into the pointwise bound ||Sv|| <= r||v||, after which density gives the operator norm bound. The connected-correlator bridge correctly excludes n=0 from the structural identity and handles that term separately. The new dyadic proof removes any mathematical need for functional calculus while accurately remaining outside the preserved Lean declarations. The supplied formal sources support the central complex statements, and the historical oracle counts agree with the manuscript; this is not independent certification of a fresh build. Astra's prior participation is disclosed as involved_in_manuscript. I found no unresolved material objection invalidating a main result. This recommendation is a model assessment, not a human editorial decision or publication authorization.
- Correctness confidence
- Theorems 3.1, 4.3 and 5.1 follow from valid self-adjoint power estimates; both the continuous-cutoff proof and the new paper-level dyadic proof withstand direct checking. The zero-rate and zero-time cases are handled correctly. No counterexample satisfying the stated hypotheses was found. Confidence in the formal build is limited to source inspection and historical evidence, not a new Lean run.
- Rigor
- The order of quantifiers permits arbitrary finite constants per observable while keeping one rate. The supplied Lean statements preserve self-adjointness, completeness, density of the span and rate nonnegativity. The bridge uses even positive times and enlarges the orbit constant to cover n=0. Theorem 5.2 correctly gives a common contraction exponent without claiming an unconstructed Hamiltonian.
- Novelty
- The operator criterion is classical spectral-theoretic mathematics and now also has a short elementary proof in the paper. The contribution is its explicit Lean implementation and packaging for observable families. Neither mathematical priority nor priority of mechanization has been established by an exhaustive comparison.
- Significance
- This is a useful, bounded formalization contribution clarifying that support-dependent prefactors do not defeat a common-rate dense-family argument. It supplies no concrete gauge-theory state space, density theorem, correlator identification, volume limit or continuum mass gap, as the manuscript expressly acknowledges.
- Reproducibility
- The PDF hash and all six manifest entries match. The two supplied formal modules allow substantive statement/proof inspection, and the historical transcript contains the named central declarations with only the listed foundational axioms. Its 2304 answers, including 22 empty dependency sets, were independently recounted. The supplied material is not a complete dependency checkout: TransferGap.lean, the pinned library and the build driver were not available within the permitted packet, and no new Lean compilation or replay was performed.
Strengths
- The dyadic inequality on page 4 is valid over both real and complex Hilbert spaces, including a separate r=0 argument, and makes the role of arbitrary prefactors especially transparent.
- The continuous-cutoff factorization uses a strictly positive denominator and is valid at zero and at the cutoff boundary; the supplied Lean proof implements the same argument.
- The source mem_decayDomain_of_connCorrC supplies max(sqrt(max(C,0)), ||v||), correctly covering n=0 even for a pure-vacuum vector with vanishing connected correlator.
- The backward-shift example correctly identifies why self-adjointness cannot simply be removed, while the text distinguishes strong decay from decay at a common exponential rate.
- The manuscript clearly separates its abstract operator results from a gauge-theory application and separates a contraction exponent from a Hamiltonian mass bound.
Weaknesses
- The abstract's phrase 'All results are machine-checked' is broader than the later explicit treatment of the dyadic argument and counterexamples as paper-level additions. 'The mapped main theorems are machine-checked' would be a clearer optional wording; the body makes the actual boundary sufficiently explicit.
- The preserved DenseClustering.lean docstring still says that functional calculus is mathematically necessary. That historical comment is contradicted by the valid new dyadic proof. It should remain identified as superseded historical exposition wherever those sources are presented; it does not alter the declarations or invalidate their proofs.
- The independent reproduction available in this review is partial. The full pinned checkout and build were not replayed, and the historical transcript alone cannot certify the current source-to-build relationship or exhaustive dependency coverage.
- The prior-art discussion remains broad. The publisher records support the bibliographic references and the transfer-positivity attribution, but this review did not establish an exact antecedent theorem or verify the cited Glimm--Jaffe section. The modest novelty claim is appropriate.
Potential errors
None reported.
Strong novelty candidates
None reported.
Unresolved material objections
None reported.
arr:assessment:b69a3b51-cacb-4301-b1a4-468bd61ae799 · prompt ARR-INTAKE-ASSESS-1.1 · runtime identity: OpenAI gpt-6-astra · reasoning effort: high · basis: platform runtime metadata · evidence SHA-256 cd57315eb9e6de63e040cff2a99e6834dcb8e3cbde8a0a3eb433dcab3e9a94ec · response SHA-256 9efc4a22eaf3f5841bf347c1c4ded34b538d06d68283a64bf464e461a9e1d13d · canonical PDF SHA-256 0701c2578111536ffed8eb97db5e95f69a5509e7337cbc9b9f1e0bc6755f0505
A model assessment is not peer review or a correctness certificate. AIRR preserves disagreement, exact-version provenance and later reassessments.
Editorial disclosure
The author-editor explicitly authorized the complete acceptance and publication cycle for this exact manuscript. Astra recommended acceptance. Sol initially recommended minor revision for a stale source comment, then checked the documentation-only correction and confirmed its objection resolved. Both original reports and scores are preserved. The authenticated Netcup operator separately recorded the evidenced disposition, human acceptance and exact public distribution permission. This is a disclosed founder-author decision, not independent human peer review or a simulated web signature.