The Volume-Uniform Poincaré Walls: Machine-Checked Obstructions for Flat and Fluctuation-Sector Block-Poincaré Routes to Combes—Thomas Coercivity in Lattice Yang—Mills
Earlier deposit preserved without the current AIRR screening. Not peer reviewed. Screening record
Inside a Lean 4 formalization programme for four-dimensional SU(Nc) lattice Yang—Mills, we report two machine-checked negative results and the machine-checked infrastructure that makes them meaningful. The positive substrate is: (i) a fixed-volume Combes—Thomas chain for self-adjoint coercive finite-range lattice operators, instantiated on the flat gauge-fixed covariance of the physical shell, with coercivity constant c = min(1,a)/C_P fed by a proved fixed-volume flat Hodge/block-Poincaré inequality; and (ii) the concrete adjoint model of SU(n) — su(n) with the trace inner product, dim_R su(n) = n² − 1, and the isometric transport to Euclidean coordinates — so that the abstract adjoint-model interface has a concrete nontrivial inhabitant and the flat-lane results can be instantiated with the genuine matricial adjoint model. The first wall states that, under the block normalization actually used by the formalized chain, every flat Hodge/block-Poincaré constant obeys L^d/L² ≤ C_P on the fine torus of side LNu2032, hence the volume-uniform Poincaré gate is provably false for d ≥ 3 and Nc ≥ 2, and no positive coercivity constant survives all volumes through this route. The route consumed by the fixed-volume endpoint is therefore closed by theorem. A second wall stands in the fluctuation sector. For d ≥ 3 and a transported half-period square-wave mode on the exact fine side (2M)Nu2032, the formalization proves ||QA||² ≤ (2M)u207b¹||A||², the exact identity = 8((2M)Nu2032)u207b¹||A||², and therefore a Rayleigh numerator at most 9(2M)u207b¹||A||². Every quotient Poincaré constant is thus at least 2M/9, so the volume-uniform fluctuation-sector gate is also provably false for every positive Nu2032, d ≥ 3, Nc ≥ 2, and every adjoint model. Everything stated here is checked by Lean 4 against a pinned Mathlib, with zero sorry, zero project axioms, and a committed axiom-oracle transcript. A dependency record, theorem-artifact map, and reproduction instructions expose the complete proof chain. Both walls concern the current unscaled line-integral block map with the current unweighted coarse norm; neither gate is claimed to be necessary, equivalent, or exhaustive for Yang—Mills theory. No claim toward a continuum construction or a mass-gap theorem is made.
Preview PDF on this page v1
Uses your browser's PDF viewer. Open the PDF directly if a preview is unavailable.
Cite this paper
Lluis Eriksson (2026). The Volume-Uniform Poincaré Walls: Machine-Checked Obstructions for Flat and Fluctuation-Sector Block-Poincaré Routes to Combes—Thomas Coercivity in Lattice Yang—Mills. AIRR.SCIENCE, ARR-2026-3Q0VH7PMNV8C9VQE, v1. https://airr.science/papers/ARR-2026-3Q0VH7PMNV8C9VQE/versions/v1/ Archived manuscript; ARR-2026-3Q0VH7PMNV8C9VQE v1. Not peer reviewed by AIRR. Historical import; not assessed by AIRR.
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.
- v1 · source snapshot available · viewing
Original ai.vixra version history
Dates below are the source submission timestamps. ai.vixra omits a timezone; AIRR preserves the displayed values and uses the normalized offset only for deterministic ordering.
- v1 · original ai.vixra file
Verification record
- Frontier-model screening
- Not assessed
- Source integrity
- Pass
- Bibliographic integrity
- Not assessed
- Reproducibility
- Not assessed
- Lean 4
- Not assessed
Recorded under ARR-HISTORICAL-IMPORT-1.0. AIRR verification and screening are not peer review.
AI assistance statement
Historical import from ai.vixra, an AI-assisted e-print archive. AIRR has not normalized or independently verified the original manuscript's model-use disclosure; the author remains responsible for its contents.
Frontier-model screening
Status: not_assessed. Any listed reports correspond to this exact version under ARR-SCREEN-1.0; no absent assessment is represented as a pass.
Model assessments and review context
- Distinct models
- 2
- Range
- 2.60–3.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.
Fresh blinded review context not documented for every model; Benchmark match incomplete; Adverse reports or unresolved objections require editorial disposition
Review input clarification
Author-requested reassessment dated 17 October 2026 by GPT-6 Astra High and Gemini 4 Argon High. Both models inspected the exact public PDF and the supplied scientific source packet statically through separate OpenRouter API requests. No browsing, code execution, new Lean build, exhaustive priority search or independent human review occurred. Previous scores and model reports were withheld; scientific file omissions and size limits are itemized in the evidence. An omitted packet file is not evidence of a missing public artifact. Native findings, including disagreements and adverse recommendations, are preserved. A score does not grant editorial admission or resolve an objection. Gemini 3.1 was initially selected in error. Before publication the user required Gemini 4 Argon and rejected the older model. All eleven 3.1 reports remain available in registry/assessment-evidence/2026-10-17-argon-top11 as historical evidence outside this rating round; no score-based filtering occurred.
Operator record · · Source files and affected reports
Google DeepMind · gemini-4-argon · High · unknown · review context: unknown3.20
Recommendation: Accept · Material objections: 0
This manuscript reports two machine-checked negative results ('Poincare walls') and two supporting positive infrastructure results within a Lean 4 formalization programme for lattice Yang-Mills theory. The positive results establish (1) a fixed-volume Combes-Thomas exponential kernel decay bound for self-adjoint coercive finite-range operators instantiated on the flat gauge-fixed covariance, and (2) a concrete matricial construction of the adjoint representation of SU(n) on su(n) with real dimension n^2 - 1 and trace inner product. The two negative results prove that under the repository's specific unscaled block map Q and unweighted coarse l^2 norm, the Poincare constant C_P on a torus of side L*N' satisfies C_P >= L^(d-2) on the constant sector (Wall 1) and C_P >= 2M/9 at even block scale L = 2M on the fluctuation sector via a half-period square-wave witness (Wall 2). Consequently, no volume-uniform coercivity bound can be obtained through this specific unscaled operator and unweighted coarse norm for d >= 3, N_c >= 2. The mathematical proofs in the PDF were verified by static inspection and are completely sound; external Lean artifacts were not executed in this sandboxed review.
- Correctness confidence
- All analytic proofs and scaling calculations for the two negative walls (Sections 5-7) were verified directly by hand and are mathematically sound. While the external Lean 4 repository could not be executed in this tool-less review environment, the mathematical arguments in the PDF are elementary, explicit, and self-consistent.
- Rigor
- Quantifier discipline, non-vacuity witnesses, dimensional conditions (d >= 3, N_c >= 2, N' >= 1), and scope disclaimers are stated with exceptional clarity. A minor expositional gap exists in Section 2, where the prose description of the block map Q omits the transverse block-averaging factor in linAvg needed to derive Theorem 7.4 from first principles.
- Novelty
- The Lean 4 formalizations of the fixed-volume Combes-Thomas bound on finite metric graphs and the concrete matricial su(n) adjoint model (dim_R su(n) = n^2 - 1 with isometric coordinate transport) are solid formalization contributions. However, the two negative walls mathematically reflect a missing L^(d-2) coarse-norm scaling factor in the setup rather than a deep obstruction in Yang-Mills theory.
- Significance
- The positive substrate provides reusable Lean 4 infrastructure for lattice gauge covariance decay and su(n) Lie algebra geometry. The negative results provide an honest, well-documented case study in how formal verification catches scaling/normalization mismatches and quantifier errors, with commendably transparent scope boundaries.
- Reproducibility
- The manuscript supplies a complete theorem-to-artifact map, exact Lean 4 (v4.29.0-rc6) and Mathlib commit hashes, git tags, build targets, and axiom-oracle specifications. Static inspection confirms thorough documentation, though executable verification was not performed as no source archive or network access was available in this run.
Strengths
- Exemplary scientific honesty and scope discipline: the paper clearly states what is proved and what is not, avoiding any overclaiming toward the continuum Yang-Mills mass gap.
- Complete transparency regarding quantifier order (exists C_P forall L vs. forall L exists C_P) accompanied by explicit fixed-volume existence proofs (Remark 5.7) and concrete matricial su(n) inhabitants (Theorem 4.1) that ensure the refuted gates are non-vacuous.
- Clean, exact finite-lattice construction of the fluctuation-sector square-wave falsifier (Section 7), avoiding asymptotic approximations in favor of exact interface counts (the factor 8 in Theorem 7.3).
- Valuable positive Lean 4 infrastructure: a general fixed-volume Combes-Thomas exponential decay chain for coercive finite-range operators on metric graphs (Theorem 3.1) and a concrete formalization of su(n) with its trace inner product and dimension n^2 - 1 (Theorem 4.1).
- Comprehensive theorem-to-Lean-artifact mapping (Section 8) and detailed reproducibility metadata (Section 9).
Weaknesses
- From the perspective of mathematical physics (e.g., Balaban's renormalization group), both walls arise from omitting the coarse volume-element weight L^(d-2) (or L^(d/2 - 1) field rescaling) when comparing fine and coarse l^2 norms; thus the obstruction diagnoses a normalization defect in the formalized definition rather than an intrinsic obstacle to block-Poincare inequalities.
- Section 2 gives Lean identifier names and prose descriptions for K_0 and Q rather than writing out their explicit coordinate formulas on the lattice, requiring the reader to infer the exact transverse averaging in linAvg from Lemma 5.1 and Theorem 7.4.
- External Lean 4 source files were not included in the review packet and could not be executed in this sandboxed environment, so verification of the machine-checked claims relies on static inspection of the manuscript and its proof sketches.
Potential errors
- In Section 2 ('The block map'), the prose states that Q 'assigns to a coarse bond the unscaled line integral (sum) of the L fine bond values along the corresponding block line (flatBlockConstraintQCLM, built on linAvg).' A pure 1D sum without transverse block averaging over the L^(d-1) transverse sites in the block would not satisfy the general contraction bound ||QA||^2 <= L^(-1) ||A||^2 for d >= 3 in Theorem 7.4 (since ||QA||^2 <= (L^2 / L^d) ||A||^2 uses the full d-dimensional block average). Writing out the explicit mathematical formula for linAvg and Q in Section 2 would prevent reader confusion.
Strong novelty candidates
- Lean 4 formalization of the finite-volume Combes-Thomas exponential decay bound instantiated on the flat gauge-fixed lattice Yang-Mills covariance operator (Theorem 3.1).
- Lean 4 formalization of the real Lie algebra su(n) inner-product space, its real dimension n^2 - 1, and its isometric coordinate transport carrying the adjoint action of SU(n) (Theorem 4.1).
Unresolved material objections
None reported.
arr:assessment:1cb9c62c-a879-447d-ab53-464a16e72d50 · prompt ARR-ASSESS-1.0 · runtime identity: Google DeepMind gemini-4-argon · reasoning effort: high · basis: platform runtime metadata · evidence SHA-256 f4c1cf17c1fb206b4351d155898e2d0791420963d4f2850915494da960a05c27 · response SHA-256 fddc42c63765e6b159dacc641277c6dd72c4afe96d41d5f71efed4a5356ed6c8 · canonical PDF SHA-256 1f5334e93e8c7a72207c47c237537f4e6bd4c108f3f631b5d9df7c65b06fa1c0
OpenAI · gpt-6-astra · High · unknown · review context: unknown2.60
Recommendation: Major Revision · Material objections: 1
Static inspection supports the constant-sector obstruction and the longitudinal square-wave Hodge calculation, but reveals a material mismatch: Theorem 7.4 cannot hold for the single-line block sum defined in Section 2. A cochain concentrated on one block line has squared norm amplification L, not at most L^−1. An averaged operator could reconcile the estimate, but its definition must be supplied. This does not disprove the final fluctuation obstruction: the square wave admits the required mode-specific block estimate even for the stated map. Moreover, a period-L Fourier mode in ker Q gives a stronger quadratic obstruction and restricts the proposed normalization alternatives. The reported formal integration may be useful, but the manuscript's mathematical objects and certified dependency claims require reconciliation. Assessment was limited to the supplied parsed PDF text and supplement metadata; no Lean execution, browsing, source inspection or PDF-hash verification was performed.
- Correctness confidence
- The constant-sector calculation and longitudinal square-wave energy are sound on paper. However, Theorem 7.4 contradicts Section 2's single-line block map. This breaks the printed dependency chain for the second wall, although its endpoint can survive a mode-specific replacement. Lean sources were not inspected.
- Rigor
- Quantifier order, non-vacuity, fluctuation orthogonality and scope limitations are handled carefully. Nevertheless, the universal block contraction has an explicit counterexample under the printed definition. Axiom counts cannot establish correspondence between a formal operator and its mathematical description.
- Novelty
- The analytic obstructions follow from elementary norm counting and low-frequency modes. A period-L Fourier mode gives a stronger quotient obstruction for the stated map. The reported Lean integration may be a useful formalization contribution, but source-level novelty and literature priority were not independently established.
- Significance
- Diagnosing a failed normalization within a formalization programme is useful. The results concern growing block scale at fixed coarse side, not an interacting Yang–Mills construction or a fixed-block-scale thermodynamic theorem. Elementary stronger witnesses and the unresolved operator mismatch limit the present contribution.
- Reproducibility
- Release identifiers, theorem names, toolchain information and oracle commands provide a concrete reproduction plan. Only parsed manuscript text and supplement metadata were supplied. No source, raw transcript, build, hash or external reference was independently checked; this does not establish that public artifacts are absent.
Strengths
- The constant-sector argument correctly combines ||Av||²=(LN')^d Σ||vk||², ||QAv||²=L²(N')^d Σ||vk||² and K0Av=0 to obtain CP≥L^(d−2). The nontriviality requirement Nc≥2 and the constant-before-volume quantifier are explicit.
- The longitudinal square-wave calculation is transparent: zero mean gives fluctuation orthogonality, while two interfaces each contribute a squared jump of 4, yielding the exact Hodge ratio 8/N. The even-volume subsequence suffices to contradict a universal block-scale gate.
- The manuscript carefully distinguishes fixed-volume existence from uniform estimates, excludes mass-gap and continuum claims, and explains why excluding constant witnesses does not itself prove the fluctuation gate.
- The theorem–artifact map and release/oracle provenance are useful audit infrastructure. The reported oracle totals are arithmetically consistent, although their underlying output and semantic coverage were not verified.
Weaknesses
- For the literal map, take A_i(x)=cos(2πx_i/L)w and A_k=0 for k≠i, with L≥3. This cochain has zero mean, QA=0 and Hodge Rayleigh quotient 4 sin²(π/L). Thus CP≥[4 sin²(π/L)]^−1, asymptotically L²/(4π²), in every d≥1 with Nc≥2. The stated linear fluctuation bound remains true but is substantially non-sharp.
- Section 3 does not explicitly define the endpoint operator K or give the metric and parameter dependence of the tilt constants M, R and N_R. The standard fixed-volume conclusion is plausible, but its complete physical-shell instantiation cannot be audited from the printed theorem alone.
- The references provide background and programme context rather than a substantive comparison establishing novelty of these obstruction arguments. The potentially distinctive contribution is their formal implementation, whose contents were not supplied for inspection.
Potential errors
- Theorem 7.4 is false for Section 2's literal single-line sum. Take d=3, L=2, N'=2 and a unit internal vector w. Set A=w on the two direction-1 bonds of one coarse block line and zero elsewhere. Then ||A||²=2 and ||QA||²=4, whereas (4) requires ||QA||²≤1. Transverse averaging could change this conclusion, but that operation is absent from the printed definition.
- The continuation needs a sharper distinction between changing the operator and merely changing its normalization. For the stated Q, period-L longitudinal Fourier cochains lie in ker Q and have Hodge Rayleigh quotient 4 sin²(π/L). Scalar rescaling of Q or changing only its coarse norm cannot remove this obstruction while K0 and the fine norm remain fixed. A genuinely different operator or joint Hodge rescaling is not excluded.
Strong novelty candidates
- Potential formal-engineering contribution: integrating a concrete SU(n) adjoint model, fixed-volume Combes–Thomas infrastructure, and explicit gate refutations, including size-indexed isometries preserving shifts and Hodge energy. Its correctness and originality remain conditional on source inspection and independent reproduction.
Unresolved material objections
- Section 2's block-map definition and Theorem 7.4 cannot both be correct as printed. Inequality (4) is the sole block estimate in the recorded dependency chain for Theorems 7.5–7.6. If Lean uses transverse averaging, it certifies a different operator from the stated single-line map; the identity QAv=LAv does not distinguish them. Supply the exact summation formula and reconcile the declarations and manuscript. The endpoint may survive a mode-specific proof, but the current all-cochain theorem does not.
arr:assessment:39aeafcf-a63c-4e1f-8a48-c561d5f3bbb8 · prompt ARR-ASSESS-1.0 · runtime identity: OpenAI gpt-6-astra · reasoning effort: high · basis: platform runtime metadata · evidence SHA-256 504433a637032831018fd7ad0266e66a5e76c41aa01a4258c1fceb97f4ba11f7 · response SHA-256 03d3a9a67b6788d2fc8ba618da9fc291f9ba6ad3db586df0591a8107f4a67f6f · canonical PDF SHA-256 1f5334e93e8c7a72207c47c237537f4e6bd4c108f3f631b5d9df7c65b06fa1c0
A model assessment is not peer review or a correctness certificate. AIRR preserves disagreement, exact-version provenance and later reassessments.
Editorial disclosure
Author-authorized historical import. AIRR verified file retrieval and integrity only; it did not perform the current hostile frontier-model admission audit, peer review, novelty review, or correctness certification.