Research paperHistorical importARR-2026-3A3YP2CEH79D4RV0 · v1
Lluis Eriksson
Repeated projective measurements are usually discussed either in the ballistic Zeno scaling or after reduction to classical outcome probabilities. We study a different regime in which each nonselective measurement retains a full matrix algebra inside every degenerate outcome block. Let E(X)=sum_a P_a X P_a, let E_tau be its rotation by exp(-i tau H), and close one cycle by Phi_tau=E E_tau E. We prove, uniformly on compact time intervals and in diamond norm, that Phi_{sqrt(t/n)}^n converges to exp(-tK)E, where K=E ad_H(1-E)ad_H E=C_H^* C_H. The limit is a genuinely quantum Markov semigroup on the direct sum of the block matrix algebras, with explicit jumps sqrt(2) P_b H P_a. Beyond upper bounds, we identify three exact local obstructions for the unprocessed physical product. The cubic map M_H produces a nonzero n^{-1/2} coefficient; after it vanishes, the quartic product obstruction J_H produces a nonzero n^{-1} coefficient; after both vanish, the quintic obstruction P_H produces a nonzero n^{-3/2} coefficient. If all three vanish, the error is O(n^{-2}). All three coefficient transforms are injective. An exact three-record algebraic example has M_H=J_H=0 but P_H nonzero, proving that the third branch is attained. The fixed algebra is A intersect {H_off}', and the least singular value of the commutator frame C_H defines a noncommutative connectivity gap. In the primitive case that gap is the exact exponential mixing exponent in diamond norm and is Lipschitz robust under Hamiltonian perturbations. Rank-one blocks reduce exactly to twice the squared-coupling graph Laplacian. An eight-dimensional rational architecture with four qubit blocks is certified irreducible; its gap is the unique root in (0.4545,0.4547) of an explicit quartic. Symbolic certificates, semidefinite diamond-norm replays, and convergence tests accompany the paper.
Research paperHistorical importARR-2026-127X6SRKAV9ZSVFM · v1
Lluis Eriksson
A subspace quantum speed limit usually records only the largest canonical angle. Passive scattering theory usually records either the largest proper delay or their total trace. Both compressions discard how a rank-k routing event is distributed across modes. We derive the missing vector law: the integrated spectral-spread vector weakly majorizes twice the canonical-angle vector. More strongly, for every symmetric gauge Φ and every pair of k-subspaces in N ≥ 2k dimensions, we solve the variational problem exactly: the minimum spectral-spread action is 2Φ(β). The same value holds for the leading-proper-delay action under positive generators, and one constant coupled-mode path minimizes all gauges simultaneously. The Ky Fan members recover the bandwidth limit, strengthen the trace-action law, and expose every intermediate modal budget. An exact nonnegative slack decomposition separates common-mode delay, inefficient spectral coupling, and nongeodesic subspace motion. Robust corollaries convert heterogeneous pass/stop leakage spectra and finite tomography errors into certified Lorenz curves for delay and, for rational inner networks, McMillan-degree lower bounds. A deterministic artifact tests 8,192 random generators, 1,536 time-dependent paths, sharp equality families, and 2,048 noisy tomography instances.
Research paperHistorical importARR-2026-6352FQW52B9AGB8Z · v1
Lluis Eriksson
Exact interpolation can force the internal degree of a passive network, but laboratory calibrations are approximate. We prove a sharp frequency-domain speed limit requiring neither exact zeros nor analytic continuation away from the measured frequency axis. Let (S(e^{itheta})) be an absolutely continuous unitary scattering path with positive Wigner—Smith generator (Q(theta)=-iS(e^{itheta})^astpartial_theta S(e^{itheta})succeq0). If a fixed (k)-dimensional input subspace is routed approximately between complementary output sectors with amplitude leakages (varepsilon_p,varepsilon_s), define (alpha=[pi/2-arcsinvarepsilon_p-arcsinvarepsilon_s]_+). Every transition then requires Wigner—Smith trace action at least (2kalpha) and largest-proper-delay action at least (2alpha). Costs add over disjoint frequency arcs. For a rational inner network of McMillan degree (n), (M) alternating pass/stop pairs imply (nge 2Mkalpha/pi), recovering (nge Mk) at zero error. An explicit (2k)-port interferometric family attains the bounds for every admissible error pair. A tomography-error corollary converts finite scattering measurements directly into certified degree and delay lower bounds. Reproducible certificates audit equality cases, positive-block inequalities and random Blaschke—Potapov products.
Research paperHistorical importARR-2026-07EH3CZRD89YC8JN · v1
Lluis Eriksson
How many internal passive modes are required to transmit prescribed quantum noise channels without loss while suppressing all signal directions elsewhere? We prove an architecture-independent answer for finite-dimensional rational networks. Let a causal rational inner scattering matrix S have McMillan degree n, signal block G, and complementary loss block C. At distinct regular boundary frequencies, suppose that G is isometric on input subspaces of dimensions k_j. If G is a strict contraction at one other frequency, then sum_j k_j ≤ n.Every lossless direction lies in the kernel of C; a nonzero maximal minor of C therefore has a zero of multiplicity at least k_j. Exterior powers of a minimal Blaschke—Potapov factorization show that no minor can have more than n zeros. The same factorization yields the exact topological delay identity(1/2π) ∫ tr Q(θ) dθ = deg_McM S = n,where Q = −i S* ∂θS is positive semidefinite. Thus lossless calibration multiplicity is bounded by integrated Wigner—Smith delay. The bound is sharp in every dimension. We establish robustness under analytic passive perturbations, prove why unstructured approximate samples cannot imply a degree bound, and show that a previously constructed six-port reservoir filter is universally optimal up to six internal states. Proofs and numerical certificates are reproduced by the linked public repository.
Research paperHistorical importARR-2026-4F7SF8FXM18ANAXH · v1
Lluis Eriksson
We study whether passive reservoir filtering can suppress decoherence more effectively when its channel mixing is irreducible, even after fixing the passband responses and rational complexity. For every integer S ≥ 5, we construct an explicit causal inner six-port network with three signal and three vacuum-loss ports. Its signal block is a rational Schur transfer satisfying 3(S−1) delayed full-spark tangential calibrations and exhibiting exponentially small leakage on two stop arcs. In contrast, every transfer of the same bidegree possessing a constant nontrivial reducing channel and satisfying the same calibrations retains unit stopband norm.We strengthen this exact separation with a quantitative finite-error obstruction: for calibration defect δ and sampled reducing-line defect β, comparator leakage is bounded below by [1−C_S(δ+β)]_+, with C_S given explicitly by finite singular-value margins. A scalar Schur construction proves that every bound of this form must deteriorate at least as 2 exp(9S/20)(1+o(1)); hence uniform robustness is impossible for the chosen clustered calibrations.For uniformly nondegenerate bath spectra, the signal-level separation is squared at the Kossakowski-rate level. A closed Markov pure-dephasing model includes all auxiliary vacuum ports exactly, producing an architecture-independent measurable baseline and an explicit total Ramsey-rate advantage. Finally, we prove that strong passive suppression requires large dwell time: under a peak-delay budget D, the rate-improvement factor is asymptotically at most quadratic in D/S. The construction therefore moves the coherence-maintenance resource into passive memory, vacuum noise and conditioning rather than eliminating it. All certificates, figures and numerical audits are publicly reproducible.
Research paperHistorical importARR-2026-26MRFNJPNM82XVWG · v1
Lluis Eriksson
Scalar Chebyshev filtering treats every vector in a block Krylov iterate with the same polynomial, while simultaneously diagonalizable matrix coefficients amount to independent scalar filters after a fixed channel rotation. We study the larger class of Hermitian matrix-polynomial filters under tangential pass constraints. Already at fixed channel dimension d=3, we construct rationally generated signatures with quantitative full-spark margin for which an irreducible symmetric filter has stopband leakage O(exp(-cN)). In contrast, every exactly calibrated symmetric coefficient family with any common nontrivial invariant channel subspace has leakage at least one; this comparator strictly contains the pairwise-commuting class and permits a fully noncommutative 2 by 2 block. A quantitative theorem covers approximately reducible filters by charging their sampled off-block coupling together with calibration error. The signature margin and the admissible combined error are both exp(-O(N)), not exp(-N^3). This exponential scale is unavoidable: for arbitrary pass nodes and signatures in the same separated bands, an explicit scalar binomial-tail polynomial has both pass error and stopband leakage at most exp(-2N/81). Thus constant-error separation is impossible, while the irreducible construction achieves the correct exponential scale class. An affine cosine substitution gives the same robust law for fixed-latency reciprocal linear-phase MIMO FIR filters. We also give an exact rational five-tap certificate with stopband norm at most 25/32 and prove that its advantage survives reducible calibration errors delta < 7/1920. A second exact-arithmetic certificate is calibrated from a public triaxial pump-vibration data set: it gives leakage below 0.96 versus one for every exactly calibrated reducible symmetric class, while its maximum directional error on six held-out records is 0.00385. In a frequency-domain-decomposition test on the frozen held-out cospectra, filtering rotates the leading modal direction by at most 0.222 degrees and changes its leading spectral ordinate by at most 2.4 × 10^-5 relatively. Numerical programs test the mechanism and expose an ordinary graph-denoising setting in which scalar Chebyshev filtering is instead preferable. Tangential matrix interpolation, MIMO filtering, scalar two-band approximation and convex FIR design are not claimed as new; the contribution is the fixed-order reducible/irreducible separation together with its two-sided calibration scale.
Research paperHistorical importARR-2026-1PEAQQ7JWA8X19W4 · v1
Lluis Eriksson
For the spatial Z_2 (Ising-slice) system inside the Dobrushin window 2 tanh|beta| + 2 tanh|gamma| <= alpha < 1, we machine-check in Lean 4 an end-to-end chain from the Gibbs measure to the spectrum of the reconstructed transfer operator. (i) The Osterwalder-Schrader (site-form) reconstruction of the transfer operator is unitarily conjugate, by the explicit sqrt(w) boundary dressing, to the symmetrised Dobrushin kernel. (ii) The unnormalised Gibbs sums themselves are exact matrix elements of that operator's powers: gibbsPathSum(w,beta,N,A,B) = lambda^N , with the partition function the same shape at the dressed constant. These are identities, not bounds, and they hold at every real beta and every positive weight. (iii) There is one mass m > 0 such that for every spatial extent L the projected operator norm is at most e^{-m} and every mixed connected correlator obeys | - | <= ||u|| ||v|| (e^{-m})^n, the zero-time case included. (iv) The connecte two-point function of the normalised Gibbs measure decays at that same rate with a constant independent of the time depth; dividing by the partition function is licensed by a denominator floor uniform in N, which the positive cone supplies and the spectrum does not, since the spectral route controls only the even powers. (v) The N -> infinity limit state exists, is the vacuum state of the reconstructed operator, and does not depend on the strictly positive observable terminating the chain. (vi) The reconstructed operator is a reversible Markov chain -- stochastic and in detailed balance for pi = Omega^2, both proved -- and in that stationary state the connected correlator of bounded observables obeys |E_pi[f P^N g] - E_pi[f] E_pi[g]| <= K_f K_g (e^{-m})^N, with quantifier order "there exists m, for all L": no factor depending on the spatial extent. Summing over time separations gives a susceptibility bound K_f K_g / (1 - e^{-m}), independent of the cut-off and of the extent. The window is non-empty at an interacting point (beta = gamma = 1/10, alpha = 1/2), machine-checked, so none of these conditionals is vacuous. The analytic input is inherited: the mass is the one the Dobrushin corollary already produced, and the window is not widened. What the reconstruction contributes is the identification, the exact identities, and the normalisation in which both the rate and the constant lose their dependence on the volume.
Research paperHistorical importARR-2026-6EVZ1F28PK8YDR6X · v1
Lluis Eriksson
We determine when rapid exact maintenance of a rank-deficient quantum target produces logarithmically divergent free-energy restoration power in algebraic quantum field theory. On every sigma-finite properly infinite factor we construct a bounded quantum Markov semigroup, a nonfaithful normal target and a faithful invariant reference state for which Araki relative entropy reduces exactly to a binary divergence. We derive the semigroup first from localized thermal fermionic probe collisions and then from one autonomous finite-bandwidth Dirac KMS reservoir with fixed smooth coupling. Exact memory equations yield an explicit finite-coupling Davies bound on finite van Hove windows. For a displayed compactly supported massless Dirac form factor, Araki—Wyss regularity, threshold behaviour and Fermi-golden-rule positivity give a completely bounded Davies approximation uniformly for all times with error of order (O(|lambda|)); the sharper (O(lambda^2)) result is isolated under additional reduced-resonance hypotheses. We construct a background-covariant two-Dirac-field completion using Green operators, Møller maps and relative Cauchy scattering, proving naturality, causal factorization and exact spacelike triviality. A locality obstruction shows why a strictly local multiplier cannot coincide exactly with the solvable rank-one reservoir coupling, while a Feshbach reduction quantifies the correction. Finally, we prove that no fixed faithful vacuum or KMS restriction can exhibit the rank-boundary mechanism, but faithful families with a vanishing spectral floor recover its complete coefficient. The results separate algebra type, target faithfulness, microscopic realizability and regulator uniformity, and provide reproducible numerical audits of the finite-dimensional identities and explicit Dirac form factor.
Research paperHistorical importARR-2026-51CS1EZ4K28W7TB3 · v1
Lluis Eriksson
We present a Lean 4 formalization of a thermodynamic-limit construction for the anisotropic nearest-neighbour Ising model on the two-dimensional integer lattice. A telescoping comparison argument and the classical Dobrushin resolvent produce a volume-uniform expectation bound. Exact restriction and reindexing maps between finite Gibbs measures yield convergence of the complete free-boundary sequence, independence of auxiliary envelopes and cofinal samplings, stability under receding boundary perturbations, and equality of free and periodic limits.Finite-support cylinder presentations are quotiented by equality of their represented functions on the full spin space. The resulting local algebra carries a genuine lattice-translation action, and the limiting functional is positive, normalized, real-linear, and invariant under every integer translation. We equip this algebra with its intrinsic uniform norm, construct its complex star-algebra representation, take the corresponding commutative C*-closure, and extend the limiting functional to a positive complex-linear functional of norm one. We also formalize normalized Gibbs conditional kernels for arbitrary finite conditioning sets and prove positivity, exterior locality, idempotence, and the exact finite-volume Gibbs tower identity.All results remain within the classical anisotropic Dobrushin region. The infinite-volume DLR fixed-point equation for the completed state is not claimed.
Research paperHistorical importARR-2026-7EPM3V3DP796BBRR · v1
Lluis Eriksson
We study whether a flat lattice-gauge Hodge form supplemented by a penalty depending only on a line-integral block variable can control the full fine one-cochain norm uniformly in the block side. The constant-field sector selects the exponent (d-2)/2 only under exact scale neutrality, but this scaling test does not address the kernel of the block map. We construct transverse, divergence-free, block-periodic Fourier cochains that are annihilated exactly by the block map. Their first-mode Hodge Rayleigh quotient is 4 sin²(pi/L), forcing every admissible full-space Poincaré constant to grow at least quadratically with L. The obstruction applies to every scale-dependent scalar functional factored through the block variable and satisfying only that it vanishes at the coarse zero field; no linearity, continuity, positivity, or growth condition is required. For linear postconditioners, higher Fourier frequencies yield an orthogonal real subspace of dimension 2R and a min—max bound on the 2R-th eigenvalue, establishing a growing low-energy spectral cluster. We also derive an exact repair identity and a necessary witness-channel budget for modified block measurements and additional fine-space terms. The kernel construction, Hodge energy, factorized no-go theorem, repair identity, and necessary repair budget are formalized in Lean 4. The result concerns a finite periodic flat full-domain form and makes no claim about interacting coercivity, gauge quotients, continuum limits, or the Yang—Mills mass gap.
Research paperHistorical importARR-2026-3FHSR0Q6W49X38F6 · v1
Lluis Eriksson
For beta > 0 let I_m = I_m(beta) denote the modified Bessel functionof the first kind and define a_m = I_m^2 ((m-1) I_(m-1)^2 + (m+1) I_(m+1)^2), b_m = m I_m^4,with sine series F_A(t) = sum_(m>=1) a_m sin(mt) andF_B(t) = sum_(m>=1) b_m sin(mt). The associated Wronskian is negativeexactly when F_A/F_B is decreasing. We isolate what can and cannot beproved from two natural inputs: the Neumann convolution kernelI_0(2 beta sin(phi/2)) and the small-coupling anchor whose normalizedlimit is 4 sin^3(t).First, the convolution does prove F_B(t) > 0 for 0 < t < pi. Second,the endpoint is governed by two alternating quantities, c_3 and B_pi,through an exact cubic law. We prove B_pi > 0, derive integralrepresentations, and establish that the cancellation lost by replacingthe alternating quantities with positive-term majorants has exponentialrate 8 - 4 sqrt(2). Finally, we prove a smooth one-parameter perturbationtheorem: one may keep F_B and its kernel unchanged, preserve positivityand strict coefficient-ratio ordering, and preserve every jet at beta = 0,while choosing either sign of the endpoint cubic coefficient.Consequently those structural data, even taken together, do not implyglobal Wronskian negativity. This is a no-go theorem for a proofarchitecture, not a counterexample to the original Bessel conjecture.A short high-precision kill-test accompanies the paper; nocomputer-assisted inequality is used in the proofs.
Research paperHistorical importARR-2026-3BQ8ENXN868SKV43 · v1
Lluis Eriksson
A formal Lean 4 development revisits a two-dimensional spatial transfer kernel whose earlier uniform spectral argument relied on constant row sums. We show that the loss of row-sum constancy obstructs that method, not the conclusion. With no sorry and no project axiom, we prove twelve machine-checked theorems.The chain establishes the sharp field-uniform one-bond influence envelope tanh J; assembles these bounds into a finite-volume Dobrushin matrix; proves a volume-independent resolvent estimate under row-sum bounds alpha < 1 without assuming constant rows; mechanises Dobrushin's comparison inequality with the attained 1/4 covariance constant; constructs Gibbs measures, heat-bath kernels and intrinsic influence matrices from arbitrary strictly positive finite weights; and specialises to anisotropic Ising interactions. For L x T rectangles with free boundary, the condition 2 tanh|beta| + 2 tanh|gamma| <= alpha < 1 yields exponential decay of correlations with beta, gamma, alpha and the prefactor fixed before the volume quantifiers.The transport into the operator formulation is closed: an exact finite band identity relating endpoint covariances to matrix elements; an abstract theorem showing that a common exponential decay rate for band covariances - a hypothesis on finite path measures, carrying no operator, norm or spectrum - implies a uniform positive gap for a family of projected transfer operators; a Perron-boundary tilt identity that preserves the decay rate while absorbing boundary costs into extent-dependent constants; an exact currying identification of the free strip measure with the rectangle Ising measure; and the resulting corollary: inside the window there is one m > 0 bounding the projected transfer operator of the coupled kernel's normalised Perron data by exp(-m) at every extent, with m = -log alpha.Numerical measurements at L <= 12 provide counterevidence to attributing spectral degeneracy solely to nonzero spatial coupling. No infinite-volume state, thermodynamic limit or boundary-condition independence is constructed; the window is sufficient, not sharp. The underlying Dobrushin mathematics is classical; the contribution is a non-vacuous, reproducible mechanisation and composition of the full chain, ending at a volume-uniform operator gap. No consequence for Yang-Mills theory is claimed.
Research paperHistorical importARR-2026-627PF1B4KK9VTRYT · v1
Lluis Eriksson
Let a fine periodic lattice have side LN' and let Q_L be the L^{-d}-normalized block average of length-L line integrals. In four dimensions, the rescaling Q_L -> LQ_L repairs the elementary constant-field scaling obstruction to a Poincare estimate. We prove that it cannot yield coercivity on the full one-cochain space with a constant uniform in the block side.For every L >= 2, every fixed N' >= 1, and N_c >= 2, we embed the first within-block Fourier phase zeta_L = exp(2 pi i/L) in a real two-plane of the internal coordinate space and construct a transverse one-cochain A_L. It satisfies Q_L A_L = 0 and div A_L = 0. For every dimension d >= 2,||A_L||^2 = (LN')^d, = (LN')^d lambda_L,where lambda_L = 4 sin^2(pi/L) <= 4 pi^2/L^2.Thus the Rayleigh quotient of K_0 + (s_L Q_L)^*(s_L Q_L) is exactly lambda_L for every scalar rescaling s_L. Every admissible full-space Poincare constant obeys C_P(L) >= 1/lambda_L >= L^2/(4 pi^2), so no constant chosen before L can work. Here "volume-uniform" means uniform while the block/fine side L varies at an arbitrary fixed positive coarse side N'; it is not a claim about N' -> infinity at fixed L.The construction, kernel identities, exact Hodge energy, Rayleigh identity, and quantified no-go theorem are formalized in Lean 4. The focused axiom audit reports only propext, Classical.choice, and Quot.sound. The theorem concerns the stated flat full-domain form; it does not contradict gauge-restricted propagator constructions and makes no infinite-volume, continuum, or Yang-Mills mass-gap claim.
Research paperHistorical importARR-2026-5V5K6T6DQT9J8SY6 · v1
Lluis Eriksson
We machine-check the exact measure and differential bridge between thefour-edge SU(2) crossing chart and the two effective group coordinates used bya finite-dimensional Ward identity. The quotientr(a)=(a2 a4^-1,a1 a3^-1) pushes normalized four-fold Haar measure exactly tonormalized two-fold Haar measure. Two gauge-compensated flows on the originalfour edges intertwine with independent right multiplication of the quotientcoordinates, so first and mixed derivatives of the crossing Wilson worddescend without choosing a gauge. The three Pauli directions are verifiedindividually, their mixed generators close into direct and reverseresolutions, and the two-coordinate Ward theorem lifts to a literal four-edgeintegral with coefficients -1/4 and -1/2. This compensated operator is notidentified with the ordinary-edge mixed operator of Driver-Hall-Kemp: thepaper writes both operators and their distinct reverse resolutions and markstheir comparison as open. The Lean producer has 26 public declarations and 16audited theorems. No weak four-face heat-kernel identity, area derivative, orfull Makeenko--Migdal equation is claimed.
Research paperHistorical importARR-2026-0JTZHGRV1C8G98TM · v1
Lluis Eriksson
We formalize extended gauge invariance at a simple four-edge SU(2) crossing and connect the geometric edge chart to the two-coordinate chart used by a machine-checked crossing Ward identity. On SU(2)^4 we define the two opposite-edge right actions from the abstract Makeenko--Migdal theorem, prove that they are commuting product-Haar-preserving actions, and show that their common parameter composes to ordinary vertex gauge invariance. The four-edge Wilson word tr2(a3^-1 beta a2 a4^-1 alpha a1) is proved invariant under both half-actions. We construct the explicit quotient r(a)=(a2 a4^-1,a1 a3^-1), a canonical section, and prove existence and uniqueness of the universal factorization for every extended-gauge-invariant complex function. The complete map from the cyclic four-edge chart to physical and gauge coordinates is proved to preserve literal four-fold Haar measure in one public endpoint. Finally, the four-edge Wilson word is identified exactly with the prior two-coordinate crossing word evaluated on r(a). The Lean producer has 56 public declarations in 488 physical lines; all 36 theorems depend only on propext, Classical.choice, and Quot.sound, with no local proof escape. No heat-kernel area derivative or full Makeenko--Migdal equation is claimed.
Research paperHistorical importARR-2026-3B7MWNSJS18TYAA4 · v1
Lluis Eriksson
We formalize a finite-dimensional crossing Ward identity for fundamental SU(2) Wilson words. On every finite edge space SU(2)^E, two distinct coordinates are inserted into a concrete normalized trace word. Lean proves entrywise that right multiplication by each of three explicit SU(2) curves produces the normalized Pauli generators i sigma_a/2, differentiates the trace word once at each selected coordinate, and identifies the Pauli-summed mixed derivative with the rank-two Fierz contraction. Two applications of Haar integration by parts transfer the corresponding mixed generators from a density to the Wilson word. The resulting integral closes exactly on the direct and reverse single-trace resolutions, with coefficients -1/4 and -1/2 in the chosen normalization. The producer contains 19 public declarations in 487 physical lines; all 13 new theorems depend only on propext, Classical.choice, and Quot.sound, with no local sorry, admit, or axiom. This is not a full Makeenko--Migdal area equation: the remaining physical input is a weak four-face identity against crossing-certified extended-gauge-invariant observables. In the program's heat time, generated by the Pauli Laplacian, its coefficient is kappa = 2.
Research paperHistorical importARR-2026-7S1XA3PZEB9QM8FQ · v1
Lluis Eriksson
A positive site weight acts on a transfer kernel by congruence, K -> DKD with Dpositive diagonal, not by similarity. Similarity preserves the entire spectrum;congruence preserves strictly less, and strictly more than nothing. We determineboth halves for the kernel of L decoupled Ising bonds. Rigid half: the sign ofevery quadratic form value survives, so definiteness in either sign is acongruence invariant -- the definite case of Sylvester's law of inertia, in aform a machine can check without diagonalisation. Fragile half: the subdominantratio r (second eigenvalue modulus over the Perron root) does not survive atall, and we locate exactly how far it moves. Restricting the L-site kernel tothe two antipodal configurations leaves one Ising bond of coupling bL, of ratiotanh(bL) for b>0: a weight concentrating there fuses the L sites into a singleeffective site carrying L times the coupling. Since tanh(bL) -> 1, no boundr <= rho < 1 holds simultaneously in L and over the whole positive-diagonalcongruence orbit; the obstruction to volume-uniformity is a property of thecongruence, not of any spectral estimate, so an argument bounding r throughcongruence invariants alone cannot produce an L-uniform bound. For arbitraryweights we prove sup_{D>0} r(DMD) = (1-m)/(1+m), where m is the leastoff-diagonal entry: the least correlated pair determines the supremum. (Weevaluate the supremum; we do not classify its maximisers.) The proof isgeometric rather than spectral -- Hilbert's projective diameter is itself acongruence invariant, and Birkhoff's contraction theorem converts it into thebound -- and uses no definiteness, only positivity of the entries. The lowerbound uses no limiting argument about spectra: a two-supported fluctuationvector gives the estimate at each strictly positive epsilon, so no continuity ofeigenvalues is imported anywhere.
Research paperHistorical importARR-2026-2FKPJ10YES8A0TWE · v1
Lluis Eriksson
We formalize the finite-dimensional integration-by-parts mechanism used inlocal proofs of the Makeenko—Migdal equation. For a measure-preserving realflow on a finite measure space, Lean verifies differentiation under theintegral from an explicit locally uniform integrable majorant and proves thatthe integral of the generator vanishes. A bounded dominated product interfacethen yields integration by parts, and two successive applications transfer amixed pair of generators from a density to an observable with positive sign.These results are instantiated on normalized Haar probability measure ofconcrete SU(2) and on every finite product SU(2)^E, for left and rightmultiplication of one selected edge. To fix the representation normalization,we construct three explicit trigonometric curves in SU(2) and prove entrywisethat their tangents at the identity are i sigma_1/2, i sigma_2/2, and isigma_3/2. The producer contains 30 public definitions, structures, andtheorems in 519 physical lines; its audit contains no local sorry, admit, oraxiom, and the headline results depend only on propext, Classical.choice, andQuot.sound. This closes the Haar integration-by-parts layer. It does not claimthe full four-area Makeenko—Migdal identity: the remaining formal inputs arethe heat-density directional identity, extended gauge invariance at acrossing, and their geometric assembly.
Research paperHistorical importARR-2026-4H8JZ663XA9XCBMN · v1
Lluis Eriksson
We give a kernel-checked positive-area calculus for the concrete SU(2) classheat kernel used in two-dimensional Yang—Mills theory. With irreducible labeln, dimension n+1, and Casimir c_n=n(n+2)/4, Lean verifies at every positivetime and every derivative order that the infinite spectral jet converges anddifferentiates term by term to the next jet. The hierarchy is packaged as aC-infinity map on the positive-time half-line, using explicit uniform summablemajorants on positive-time neighbourhoods. We then differentiate the literalnormalized-Haar two-face Migdal integral, prove that its left and right areaderivatives equal the first spectral jet at the merged area, and showinfinitesimal invariance under (s,t) -> (s+u,t-u). Finally, every normalizedWilson character satisfies its exact Casimir area ODE as an actual Haarintegral against the infinite heat kernel. The artifact contains 25 publicdefinitions and theorems, no local placeholders, and audited dependencies onlyon propext, Classical.choice, and Quot.sound. We do not claim the four-faceMakeenko—Migdal crossing equation; the remaining inputs are local Lie-groupintegration by parts and certified crossing geometry.
Research paperHistorical importARR-2026-7C7E7PRA1Y8MNAWK · v1
Lluis Eriksson
Finite-rank Makeenko-Migdal equations generate products of Wilson traces at self-intersections. For SU(2), this apparent multitrace obstruction closes exactly on single traces, but the statement is normalization-sensitive: the traceless Lie algebra contributes a finite-rank correction that disappears for U(2) and must not be dropped. We give a Lean 4/Mathlib formalization of the complete group-algebraic closure mechanism on Mathlib's concrete special unitary matrix group. With normalized trace tau(A)=Tr(A)/2 and normalized anti-Hermitian Pauli directions X_j=i sigma_j/2, the kernel checks the Casimir identity, the rank-two Fierz identity, the induced crossing contraction, and the SU(2) trace-skein identity tau(g)tau(h)=(tau(gh)+tau(gh^{-1}))/2. Consequently, the finite-SU(2) crossing term tau(g)tau(h)-tau(gh)/4 equals tau(gh)/4+tau(gh^{-1})/2. We then formalize a universal local interface with four cyclically ordered branch holonomies, an independent orientation on each branch, the two opposite-strand words, and precisely the two direct/reversed reconnections. Its corrected crossing term closes on those reconnections for every branch assignment and orientation choice. A recursive theorem also extends the reduction to products of arbitrarily many fundamental traces. The identities are classical; the contribution is a concrete, kernel-checked normalization bridge from Pauli contraction to the single-trace closure used in finite-rank loop equations. We do not claim a formal derivation of the Yang-Mills area derivative, planar loop geometry, or the full Makeenko-Migdal equation.
Research paperHistorical importARR-2026-223XBWQ8PQ8Z2RDS · v1
Lluis Eriksson
BOND REFLECTION, AND THIS ONE IS ABOUT THE MEASURE. A whole path X of 2m+2slices has a past half past(X) and a future half; write rev(X) for the futurehalf READ BACKWARDS FROM THE FAR END, which is the reflected copy. Let F be acomplex observable of an entire half. Then for every L, every m, everystrictly positive source weight w and every beta >= 0, sum over whole paths X of conj(F(past X)) * F(rev X) * W(X) >= 0the sum running over all whole paths and W being the ordinary Gibbs weight.This is the finite-volume Osterwalder-Schrader reflection-positivityinequality for this model at odd separation. The sum is UNNORMALISED, which isthe form the axiom is about; dividing by the partition function is division bya positive number and preserves the sign. The Gram matrix of a finite familyof such observables, with complex coefficients, satisfies it as well. It isobtained by proving that assembling a past half, a crossing bond and areversed future half is a BIJECTION onto paths, and that the weights multiplywith exactly one crossing factor.SITE REFLECTION, AND THIS ONE IS NOT, YET. Through a site the two halves SHAREthe middle slice, so the assembly is not a product of two independent halvesand its bijection is a different statement. What is proved there is thehalf-chain form, its collapse identity and its Gram positivity -- at EVERYbeta, negative coupling included -- but NOT its identification with the pathmeasure. For that geometry the object remains a candidate, and the statustable says so row by row.ON THE BETA HYPOTHESIS. beta >= 0 is proved SUFFICIENT and is not provednecessary here; at L = 0 it could not be, since the bare kernel is then thescalar 1. The witness that would make the boundary exact from one site upwardsis authorised by a gate and is not written.THE MECHANISM, IN ONE SENTENCE. Summing out the interior of a half sends F toa vector indexed by its boundary slice alone, after which the bond casereduces to positive semidefiniteness of the kernel -- machine-checked in thecompanion paper -- and the site case to a weighted squared norm, which uses noproperty of the kernel at all.WHERE THE TWO REFLECTIONS DIFFER, AND IT IS NOT COSMETIC. Through a bond thetwo halves are disjoint and meet through one kernel factor, so positivityneeds the kernel itself positive semidefinite -- which, for L >= 1, holdsexactly when beta >= 0. Through a site the halves SHARE the middle slice; theform is then a sum of squared moduli divided by the weight of that slice, soit is non-negative for EVERY beta, negative coupling included, and no propertyof the kernel is used at all.WHAT THE SOURCE WEIGHT DOES. In the companion paper the weight was handled bycongruence: conjugation by sqrt(w) cannot change the sign of a quadratic form.Here it is not conjugated away, it is SUMMED away -- and what is left overdiffers between the two geometries. In the bond case every source weight isabsorbed into the collapse and the bare kernel remains; in the site case theshared boundary slice survives as a factor 1/w(sigma), because each halfcarries that slice's weight and the product would count it twice. Differentreasons, same conclusion: nothing in the hypotheses depends on w beyondpositivity.WHAT THIS IS NOT. No reconstruction: the physical Hilbert space as thequotient of the past algebra by the null space of this form is not built.Nothing here concerns uniformity in the extent, SU(N), the continuum limit, orthe Yang-Mills mass gap.ON THE PRE-REGISTRATION. Four gates were committed before a line of the modulewas written; the status table reports what happened to each. Two of them reada minimum eigenvalue rather than sampling observables, which is the instrumentthe previous campaign's autopsy said was needed.
Research paperHistorical importARR-2026-02YRWX53DG9M3R0R · v1
Lluis Eriksson
WHAT IS PROVED, STATED BEFORE ANYTHING ELSE. The reflected two-point form ofthe Gibbs measure, at the two ENDS of a path, for REAL observables of a SINGLEslice, is non-negative under the parity and coupling hypotheses stated below-- at even separation for every beta, and at every separation exactly for beta>= 0 -- and the Gram matrix of a finite family of such observables is positivesemidefinite under the same hypotheses. THIS IS NOT YET THEOSTERWALDER-SCHRADER AXIOM, which quantifies over observables of the wholepast half-chain and over complex ones. The half-chain algebra, the reflectionmap and the sesquilinear form are not built here; the scope section says whatis missing and why it is a construction rather than a further inequality.Eleven papers in this lane end with REFLECTION POSITIVITY IS UNTOUCHED. Thistouches the endpoint form of it, and the interesting part is what the spatialsource weight does -- namely nothing. Earlier papers do prove statements aboutthe coupled kernel; specGap < lambda holds there too. What is new is that thisresult is UNCHANGED by the weight: same hypothesis, same conclusion, and noconstant that depends on w. Every earlier coupled-kernel statement contains anumber that moves when w does. Positivity is the SIGN of a quadratic form, andconjugation by sqrt(w) is a congruence, so there is nothing for the weight tomove.TWO REFLECTIONS, TWO HYPOTHESES. The reflected two-point sum is with v the dressed observable, and the two cases have genuinely differentcontent. Through a SITE (N even) the sum is a square, hence non-negative forEVERY beta -- negative coupling included -- with nothing used but symmetry ofthe kernel. Through a BOND (N odd) it is , which needs Kitself positive semidefinite; that holds exactly for beta >= 0, by aninduction on the extent.AND THE SECOND HYPOTHESIS IS ACTIVE. At beta < 0 and odd separation thesingle-site sign observable gives the reflected sum in closed form, 2(e^beta -e^-beta)^N, which is negative. Congruence is invertible, so the same witnessdivided by sqrt(w) shows the COUPLED kernel is indefinite below zero for EVERYstrictly positive weight, at every extent with at least one site. At L = 0there is nothing to witness -- one configuration, and there the decoupledkernel is 1 while the coupled one is the positive scalar w(empty) -- and thatexception is recorded rather than left to be found. The boundary beta = 0 issharp and exhibited, not inferred.WHAT THIS IS NOT. Neither the full axiom (above) nor any reconstruction: thephysical Hilbert space as the quotient of the past algebra by the null spaceof this form is not built. And the degeneration of specRatio(L) under a ringweight is MEASURED, not proved; no theorem here or elsewhere in the lane saysthe weight destroys uniformity, only that no uniform bound is proved for it.Nothing here concerns uniformity in the extent, SU(N), the continuum limit, orthe Yang-Mills mass gap.ON THE PRE-REGISTRATION. Three ACTIVE gates were committed before any Lean waswritten, and the gates section reports what happened to each. A fourth ispreserved there and not counted: the original Gate B, which failed because ofa design error of ours, and which two of the three active gates replaced.
Research paperHistorical importARR-2026-5SGNYDASRB9V9VF9 · v1
Lluis Eriksson
We formalize in Lean 4 the thermodynamic limit of bounded local Gibbs expectations for a periodic lattice gauge model in a uniform Kotecky-Preiss regime. The proof treats the complete finite-volume sequence: an exact one-volume marked expansion cancels the extensive far gas algebraically, common-window terms are transported exactly, and the remaining boundary contribution is bounded by an existing volume-uniform pinned cluster tail. The resulting explicit Cauchy modulus tends to zero, so completeness constructs an infinite-volume positive normalized real local state. On the intrinsic integer-coordinate local-observable algebra, the state carries a genuine additive action of Z^d and is invariant under every integer translation, including inverses. For SU(2), Haar probability measure, and the physical Wilson plaquette energy Re tr(U), the hypotheses are discharged throughout the explicit punctured intervals 0 < |beta| <= 10^-5 in d=2 and 0 < |beta| <= 10^-6 in d=4. We construct a genuine centered free-boundary exhaustion and prove that its complete cofinal sequence converges to the same state as periodic boundary conditions. The normalized finite-volume two-plaquette truncated-correlation bound also passes to the state under explicit eventual realization and separation hypotheses. We do not claim arbitrary boundary conditions, a C*-algebraic state, a continuum limit, Osterwalder-Schrader reconstruction, or progress on the continuum Yang-Mills mass-gap problem.
Research paperHistorical importARR-2026-3EXXMXJD119J1R6R · v1
Lluis Eriksson
Every rate in this lane so far has been a fixed-extent rate. The gap paper provedstrict spectral separation at each extent and said plainly that it was notuniform; the modulus paper gave that separation a number, specRatio(L), andreported measurements saying the number tends to 1 outside the disordered region.A geometric bound whose rate tends to 1 is empty in the volume limit, so nothingin the lane survived L -> infinity, and the word CLUSTERING was never used.PROVED. For the DECOUPLED kernel - the transfer kernel at constant source weight- the modulus is specRatio = tanh(beta) at EVERY extent, with L nowhere in it.Both directions: an operator bound by induction on the extent, and attainment bythe single-site observable the extent paper already built. Composing with themodulus paper's endpoint, the normalised Gibbs two-point function obeys|E[A(X_0)A(X_N)]| <= C_A tanh(beta)^N past one threshold serving everyobservable - a bound whose RATE contains no L, and therefore the first statementin this lane that survives the volume limit.WHY THE PROOF IS NOT THE SPECTRAL DECOMPOSITION. The decoupled kernel is aproduct over sites, so its spectrum is a product; that route needs the spectrumof a Kronecker power, which the library does not carry. It is not needed. Themodulus paper proved that specGap is the GREATEST norm ratio on the fluctuationsector, so bounding it above is an operator inequality and nothing else, and thatfalls to induction: the even part of an observable keeps its mean zero andinherits the rate, the odd part keeps nothing and gets only Schur's test, and thetwo recombine EXACTLY, because tanh(beta) Z = D with Z the row sum and D the oddeigenvalue of a single bond.NOT PROVED, AND A JUDGE THAT FAILED. The COUPLED kernel is untouched. Before anyof this was written we pre-registered two falsifiable predictions. The first -that the decoupled rate is exactly tanh(beta) at every extent - passed to 1e-16,and authorised the work above. The second - that the coupled uniformity boundaryis the Onsager curve - failed on one of eight pre-registered cells, and it staysfailed: that claim is reported as NOT ESTABLISHED, not softened. At constantsource weight the spatial slices are independent, so what is proved here is astatement about a product measure; that is exactly why it is reachable, and it issaid in the paper rather than left to be noticed. Reflection positivity isuntouched, and nothing in this paper is a claim about SU(N), the continuum limit,or the Yang-Mills mass gap.
Research paperHistorical importARR-2026-1A7WS4SDF0894BPS · v1
Lluis Eriksson
Two companion papers were left carrying the same debt from opposite sides. Thegap paper proved that every eigenvalue of the coupled slice other than thePerron eigenvalue is STRICTLY smaller in modulus, and said plainly that thisprovides NO MODULUS of separation. The bridge paper proved that the Gibbscorrelations of the spatial system are matrix elements of a self-adjointtransfer operator, and obtained geometric decay only UNDER A CONTRACTIONHYPOTHESIS IT DID NOT DISCHARGE. The missing step is identical in both: finitelymany strict inequalities are not an operator-norm bound.PROVED. We construct specGap, the largest |mu| over the eigenvalues differentfrom the Perron eigenvalue lambda, and prove specGap < lambda. We then prove theoperator bound: for every observable u orthogonal to the Perron vector,||Ku|| <= specGap*||u||. That is exactly the hypothesis the bridge papercarried, so its bound becomes unconditional. The bound is SHARP: whenever thestate space has at least two points, some nonzero fluctuation observable attainsit. The argument splits at specGap = 0, where the maximising index need notsupply a NON-PERRON eigenvector (it does supply the Perron one), hence none inthe fluctuation sector. Stated about an object too: the set of Rayleighnorm ratios on the fluctuation sector has a greatest element, equal to specGap(same two-point hypothesis: with fewer, that set is empty).A WARNING WE STATE BEFORE ANYONE ELSE HAS TO. specGap < lambda is NOTspecGap < 1: the kernel is unnormalised, so both are typically far above one andspecGap^N GROWS. On its own the unnormalised bound controls growth, it does notexhibit decay. The rate that is below one is the RELATIVE one,specRatio = specGap/lambda < 1, and the decay statement is that the fluctuationcontribution is suppressed by specRatio^N RELATIVE to the Perron scalelambda^N. Both forms are proved; only the second is called decay.The step that does not follow from the inequalities is the one abouteigenvectors AT lambda: geometric simplicity, proved in the Perron paper for anarbitrary eigenvector rather than a positive one, makes them INVISIBLE to afluctuation observable, so the top term of the spectral sum vanishes instead ofmerely being bounded.NOT PROVED. specGap DEPENDS ON THE EXTENT, and nothing here bounds it away fromlambda uniformly. Direct diagonalisation gives specGap/lambda = 0.9205, 0.9829,0.9964, 0.9992 at L = 2,3,4,5 for one parameter pair: a geometric bound whoserate tends to 1 is empty in the limit, and that is reported, not hidden. Thenormalised Gibbs EXPECTATION is now bounded too: splitting the dressed constantobservable along the Perron direction bounds the partition function below withno eigenbasis index identified, so at a fixed extent the two-point function isbounded by C*specRatio^N past an explicit threshold. That rate depends on theextent, so this is not clustering. The bound and its attainmentare both proved, which is what it means for specGap to be the operator norm onthe fluctuation sector; what is NOT done is introducing that norm as a definedobject and proving an equation about it. And the threshold N_0 does not dependon the observable: it is built from the dressed CONSTANT observable, so ONE N_0serves every fluctuation observable at once and only C sees A. Reflectionpositivity is untouched, and nothing in this paper is a claim about SU(N), thecontinuum limit, or the Yang-Mills mass gap.
Research paperHistorical importARR-2026-2TTA0WSQBT89X964 · v1
Lluis Eriksson
Four companion papers studied an OPERATOR: a strictly positive kernel on thespatial configuration space of a Z_2 slice, its Perron vacuum, and the strictseparation of its spectrum. None of them exhibited a MEASURE. That omission isthe kind this programme is built to notice: a transfer operator is a matrixuntil something says which Boltzmann weights it transfers, and until then avacuum is an eigenvector and a gap is a statement about eigenvalues. Neither isyet a statement about a statistical-mechanical system.PROVED. We define the two-dimensional Gibbs weight of the spatial system fromBoltzmann factors alone - a spatial factor at every time slice, a time-bondfactor between consecutive slices - and prove the DRESSING IDENTITY: that weightequals the path weight of the SYMMETRISED kernel multiplied by a factorsupported entirely on the two boundary slices. Hence every UNNORMALISED Gibbstwo-point sum of the spatial system is a matrix element of an iteratedSELF-ADJOINT transfer operator between boundary-dressed observables, and theNORMALISED expectation is the RATIO of two such matrix elements - the numeratoralone is not the correlation. The generic half holds for an arbitrary symmetrickernel on an arbitrary finite type; no positivity and no structure of theconfiguration space enter it. We further show that the operator the bridge landson is the one the companion papers analysed, that the fluctuation sector isinvariant, and that under an explicit contraction hypothesis the connectedtwo-point function decays geometrically in the time separation.NOT PROVED, AND THIS IS THE POINT OF THE LAST SECTION. The contractionhypothesis is carried as a theorem hypothesis and is NOT discharged. Thecompanion papers prove a STRICT gap with no modulus, and a strict inequalityamong finitely many eigenvalues does not by itself produce the operator-normbound a decay rate requires. Converting one into the other needs the spectralmaximum over the fluctuation sector, which is not constructed here. Inparticular NOTHING UNIFORM IN THE SPATIAL EXTENT is obtained, and none issuggested: with r = r(L) approaching 1, the bound is empty in the limit.Reflection positivity is not addressed. Nothing in this paper is a claim aboutSU(N), the continuum limit, or the Yang-Mills mass gap.
Research paperHistorical importARR-2026-1A608PTGTC9XX9JZ · v1
Lluis Eriksson
A companion paper supplied the vacuum of the coupled Z_2 slice at every spatialextent: a strictly positive eigenvector, unique up to scale, carrying thespectral radius. It listed PERIPHERAL SEPARATION as out of scope, and thatomission is not cosmetic - without it |mu| <= lambda leaves mu = -lambda open,and no gap follows at all.This paper closes it, and then draws the consequence that matters, which isnegative.PROVED. For a strictly positive kernel on a finite nonempty type, -lambda is notan eigenvalue, hence every real eigenvalue other than the Perron eigenvalue isSTRICTLY smaller in absolute value. Specialised to the coupled slice: at everyextent L, every beta, and every strictly positive source weight, the transferoperator has a strict spectral gap. The proof of peripheral separation avoidsthe equality case of the triangle inequality, which is where the classicalargument spends its effort: writing u = |w|, p = u - w and q = u + w, one getsA p = lambda q and A q = lambda p, so a nonzero p would make A p strictlypositive, hence q strictly positive, hence w nonnegative, hence p = 0.The separation is then extended from the real eigenvalues to ALL of them. Thecoupled kernel is conjugate by a positive diagonal to its symmetrised form,which is symmetric; and a real symmetric kernel has real eigenvalues, by acomputation that pairs the eigenvector against its image twice and is tworearrangements of a double sum. So there are no complex peripheral eigenvaluesleft to exclude, and the strict gap is a statement about the whole spectrum.That composition is itself a single machine-checked theorem(coupled_gap_all_eigenvalues), not a step left to the reader. We also deliverthe vacuum in Euclidean normalisation, norm(Omega) = 1 with T Omega = Omega.NOT PROVED, AND THIS IS THE TITLE. The gap is STRICT, not QUANTITATIVE: thetheorem provides no modulus of separation, and in particular nothing uniform inL. Direct numerical diagonalisation shows the subdominant ratio running0.9205, 0.9829, 0.9964, 0.9992 at L = 2,3,4,5 for beta = 0.8, gamma = 1.2 -collapsing towards 1. That computation is reported as measured and unproved, andno theorem here depends on it; its role is to say that a paper reporting onlythe positive half would be reporting the half that does not matter.Nothing in this paper is a claim about SU(N), the continuum limit, or theYang-Mills mass gap.
Research paperHistorical importARR-2026-2YDE42KFDY8Y3AA0 · v1
Lluis Eriksson
Two companion papers established, for a Z_2 lattice gauge slice with a spatialcoupling, that the elementary route to the vacuum stops, and that the naturalreplacement - the Hilbert projective metric - is blind to the coupling anddegenerates in the volume. Both had to work around the same absence: the pinnedmathlib carries no Perron-Frobenius theorem. The first paper could therefore onlysay the vacuum had become unavailable; the second had to build its dominationbound from scratch, and could exhibit the vacuum in closed form only at two sites.This paper discharges that dependency. For a strictly positive kernel on a finitenonempty type we prove, in Lean 4 with mathlib: a strictly positive eigenvectorEXISTS; its eigenvalue is strictly positive; any two strictly positiveeigenvectors are proportional and share their eigenvalue; and every realeigenvector for that eigenvalue is a scalar multiple of it. Together with thedomination theorem of the companion paper this gives the Perron statement thelane needs: the eigenvalue is the spectral radius.The existence proof does not use a fixed-point theorem, because the pinnedmathlib revision contains none. It maximises r over the compact set of pairs(r,x) with x in the simplex and r x <= A x; maximality forces equality, since astrict inequality anywhere would let one further application of A produce anadmissible pair with a larger r. The bound that keeps the set compact is obtainedby summing the constraint: r = r * sum x <= sum (A x).The application is the point. At EVERY spatial extent, and for EVERY strictlypositive weight on the source configuration - the class that contains the coupledkernel of the first paper - the vacuum exists, is unique up to scale, and carriesthe spectral radius. The obstruction of that paper was never an absence; it wasan unavailability, and it was an unavailability of one route rather than of theobject.NO SPECTRAL GAP IS PROVED HERE, uniform in the volume or otherwise, and none isclaimed. Nothing in this paper is a claim about SU(N), the continuum limit, orthe Yang-Mills mass gap.
Research paperHistorical importARR-2026-6M8PMVHTMH8YZ9ND · v1
Lluis Eriksson
A companion paper proved that when a spatial coupling is switched on in a Z_2lattice gauge slice, the transfer kernel loses constant row sums, so the uniformvector is no longer fixed and the elementary route to the vacuum stops. Thestandard replacement, when row sums fail, is the Hilbert projective metric: astrictly positive kernel contracts it, and the contraction factor bounds thesubdominant spectral ratio. This paper asks what that replacement gives here, andanswers in Lean 4 with mathlib.It gives no coupling-sensitive and no volume-uniform information, for twoindependent reasons, and both are proved. First, BLINDNESS: the projectivecross-ratio is invariant under multiplication by any nowhere-zero function of thesource configuration alone. The coupled kernel is exactly such a product, so themetric assigns the interacting and the non-interacting kernels the same diameterat every spatial extent - the route cannot see the coupling at all. Second,VOLUME DEGENERATION: two constant configurations realise the cross-ratioe^(4 beta L), so every admissible projective diameter is at least 4 beta L andevery contraction factor obtainable this way is at least tanh(beta L), which lieswithin 2 e^(-2 beta L) of the trivial bound 1. At the one place where the truthis known - the decoupled kernel, whose subdominant ratio the companion papercomputes to be exactly tanh beta at every L - this route already returnstanh(beta L) instead. The degeneration is the method's, not the model's.We then hand over the object the elementary route stopped producing, at thesmallest interacting size. In the character basis the coupled two-site kernelsplits into two 2x2 blocks, and we exhibit a strictly positive eigenvector inclosed form, together with a second exact eigenpair. The identity A - B = 4between the two decoupled even-sector eigenvalues drives every estimate. Theblindness is proved two-sided, so it covers the symmetrised conventionw^(1/2) K w^(1/2) as well, and the positive eigenvector is proved to dominateevery eigenvalue, real or complex - so its eigenvalue is the spectral radius,which is the Perron statement this development needs and proves without aPerron-Frobenius theorem in the library.NO VOLUME-UNIFORM STATEMENT ABOUT AN INTERACTING SYSTEM IS PROVED HERE, AND NONEIS CLAIMED; the general-L behaviour is recorded separately as measured andunproved. Nothing in this paper is a claim about SU(N), the continuum limit, orthe Yang-Mills mass gap.
Research paperHistorical importARR-2026-3CEWH763KG84B8TM · v1
Lluis Eriksson
For beta > 0 let I_m = I_m(beta) denote modified Bessel functions ofthe first kind, and set a_m = I_m^2 [(m-1) I_(m-1)^2 + (m+1) I_(m+1)^2], b_m = m I_m^4, F_A(t) = sum_(m>=1) a_m sin(mt), F_B(t) = sum_(m>=1) b_m sin(mt), E(t) = F_A(t)/(2 F_B(t)).The global ratio-monotonicity problem for the surface expansion of atwo-dimensional SU(2) lattice gauge observable is: (i) F_B > 0 on(0,pi), and (ii) E' < 0 on (0,pi), for every beta > 0. Bothstatements are proved. Positivity of F_B has two exact proofs. Ratiomonotonicity is reduced to exact algebraic identities andoutward-rounded interval certificates: small and compact beta arehandled by pair identities and interval Taylor models;20 <= beta <= 1000/9 by a direct Wronskian cover; andbeta >= 1000/9 has three certified moving-edge lambda lanes. Theremaining lambda >= 3 lane is closed by the exact identityE'/(-sin(t/2)/2) = Q + X_full, where Q > 19/20, an exactmain--mirror--rest decomposition, and a division-free covariancecertificate proving X_main > -1/20 on two adjacent rectangles thatcover the full angular interval. The exact near and far relay marginsare positive. All load-bearing production and independent replaytranscripts are checked for exact rational coverage, dependencyhashes, strict outward-rounded decision endpoints, and byte equality.The structural core is exact: E is, as an algebraic identity, the meanof cos(psi) under the midpoint law of a four-step killed von Misesbridge; the generating kernels reduce, via the Neumann additiontheorem, to two-dimensional integrals of a single Bessel functionwhose saddle deficit is an exact sum of two squares; and exact saddlecancellations yield the coefficients of the verified closedsecond-order law E = cos(t/2)(1 - c(t)/beta) + O(beta^-2), c(t) = (4 cos^2(t/4) - 1)/(2 cos(t/4) cos(t/2)).Three certified negative results (interval arithmetic, twoimplementations, nested enclosures) kill every monotone full-pathcoupling, with an exact mechanism at threshold beta |cos t| = 3/2. Atthe pi endpoint we also give exact identities for the cubiccoefficient c_3 (telescoped alternating form, integral form, parity)together with its verified prefactor law. Every claim is labelledexact / certified / verified; the machine-checked lemmas are Lean4/Mathlib, machine-checked modulo classical Bessel inputs carried asnamed hypotheses.
Research paperHistorical importARR-2026-4X084GVAYF87PB3F · v1
Lluis Eriksson
Two companion developments verified an Osterwalder-Seiler reconstruction end toend for a lattice gauge chain whose spatial slice is a single point. Every stepof that chain begins by knowing the vacuum, and in the one-dimensional case thevacuum is free: the normalised transfer kernel has constant row sums, so theuniform vector is fixed, and T*Omega = Omega follows from normalisation alone.This paper asks what survives when the slice acquires spatial extent, andanswers in Lean 4 with mathlib.The algebraic half survives untouched. With time bonds only, the row sums of thetransfer kernel are constant for every spatial extent L, so the uniform vacuumpersists on a space of dimension 2^L; and the single-site sign observable is aneigenvector whose normalised eigenvalue is exactly tanh beta, with L free in thestatement.The uniform vacuum does not survive. Switching on a coupling between sites inside aslice makes the spatial weight depend only on the source configuration, so itfactors out of the sum over the target and the row sums becomeconfiguration-dependent. We exhibit two explicit configurations of a two-siteslice with different row sums, and conclude that no constant row sum exists: theuniform vector is not fixed, so T*Omega = Omega is FALSE for it. The vacuumbecomes a Perron vector that row-sum normalisation no longer supplies in closedform, and every later step of the reconstruction loses its starting point.We state plainly what the positive half is and is not. The decoupled system is Lnon-interacting copies of a two-state system, and the rate it yields - theeigenvalue tanh beta of the single-site sign mode - is independent of L fortrivial reasons, so it is physically empty and is recorded only because itisolates which half of the construction survives. NO GAP FOR THE COUPLED SYSTEM IS PROVED HERE, AND NONE IS CLAIMED.Nothing in this paper is a claim about SU(N), the continuum limit, or theYang-Mills mass gap.
Research paperHistorical importARR-2026-2TBRDN2DE598KSXD · v1
Lluis Eriksson
The Osterwalder-Seiler reconstruction passes from a reflection-positive measureto a Hilbert space by quotienting out the null space of the reflected pairing.In a companion development that step was present but did nothing: the pairingthere was definite, so the quotient was the identity, and that paper says so inits own abstract. This paper supplies the missing case, in Lean 4 with mathlib.For the Z_2 lattice gauge chain we take half-space observables of two timeslices - a four-dimensional space - and form the reflected pairing directly fromthe Boltzmann weights. For beta > 0 the reconstructed physical space istwo-dimensional. Integrating out the future collapses four observables onto twostates, and that collapse is the null space. We prove: the pairing factors through anindependently defined reconstruction map Phi; its self-pairing rearranges into amanifest sum of two non-negative terms, from which positivity and the null spacefollow together; the null space is EXACTLY ker Phi, not merely non-empty; anexplicit non-zero observable lies in it; and the quotient is isomorphic to thephysical space BY THE MAP Phi ITSELF, not by a dimension count.The degeneracy is the mechanism the reconstruction exists to handle, and the oneexpected to reappear in systems with larger half-space algebras. What is notclaimed: this is twotime slices and not m; still Z_2, one variable per slice, fixed finite size, andnot volume-uniform; Z_N for N > 2 is untouched; and the completion step of thereconstruction is trivial here because every space in sight isfinite-dimensional, which we state rather than present as work done. Nothing inthis paper is a claim about SU(N), the continuum limit, or the Yang-Mills massgap.
Research paperHistorical importARR-2026-3NE8S0F70089P8PF · v1
Lluis Eriksson
We give a finite-dimensional Osterwalder-Schrader reconstruction for an anisotropic Ising model on open rectangular strips and prove a spectral gap whose rate is uniform in the finite spatial extent. For temporal coupling beta, spatial coupling gamma, and parameters satisfying 0 < alpha < 1 and 2 tanh|beta| + 2 tanh|gamma| <= alpha, one number m > 0 works for every spatial length. Reflection positivity is proved directly for the Gibbs measure; the null space of the reflected form is identified with the kernel of an explicit boundary-collapse map; the OS quotient is linearly equivalent to the finite boundary-vector space; and the transfer operator forced by the site and bond forms is intertwined with a symmetrised transfer matrix.Dobrushin comparison supplies positive Perron data and a projected operator norm bounded by exp(-m) for every spatial length. Consequently, connected reconstructed correlations decay at the same common rate. Lean 4 checks thecomposition without assuming reflection positivity, Perron data, a vacuum, a gap, or clustering at the public endpoint. This replacement extends the point-slice, fixed-size v1 to finite strips with one rate uniform in spatial size. It does not construct an infinite-volume operator or Hamiltonian, provea unique particle excitation or relativistic mass shell, or claim a Yang-Mills mass gap.
Research paperHistorical importARR-2026-10JJK0VCCS87VTQH · v1
Lluis Eriksson
We machine-check, in Lean 4 with no sorry and no project axioms, theOsterwalder-Seiler reflection positivity of a lattice gauge theory with finiteabelian gauge group. The development is organised so that the three ingredientsare separated and each is proved on its own: an analytic step, a geometric step,and the single place where a property of the Boltzmann factor is actually used.The analytic step is that a crossing kernel of the formK(x,y) = sum_i c_i phi_i(x) conj(phi_i(y)) with c_i >= 0 is positivesemidefinite, that this class is closed under products, and that it is closedunder conjugation by a positive diagonal. Formulating the hypothesis as anon-negative combination of characters rather than as non-negativity of Fouriercoefficients removes any need for Bochner's theorem on a finite abelian groupand for the Schur product theorem: the development uses no spectral and nomatrix-positivity API.The geometric step is a splitting of the configuration space across thereflection plane under which the reflection is the swap and the Gibbs weightfactors as w(x) w(y) K(x,y). We prove that the Osterwalder-Seiler pairing of anobservable of one half against its reflection is then exactly the quadratic formof w(x) K(x,y) w(y), so that reflection positivity follows from the analyticstep.The physical step is the instance. For Z_2 the Wilson factor exp(beta s),s = +-1, expands in the two characters with coefficients(exp(beta) +- exp(-beta))/2, both non-negative exactly when beta >= 0; so theZ_2 Wilson crossing kernel is positive semidefinite at non-negative coupling. Asingle endpoint combines a gauge system with a nontrivial time reflection, aconcrete splitting, that weight at positive coupling, and the conclusion; itsplaquette straddles the reflection plane, so the entire Gibbs weight is thecrossing kernel. It is a two-edge system, and a full temporal box is nottreated. For Z_N with N > 2 the coefficients are discrete Bessel-type sums andtheir non-negativity is not established here.We are explicit about what is absent: no Gelfand-Naimark-Segal quotient, notransfer operator, no identification of a Euclidean correlator with a matrixelement, and therefore no mass gap. Nothing here is a claim about SU(N), thecontinuum limit, or the Clay problem.
Research paperHistorical importARR-2026-31ED4MTKC18JPSDE · v1
Lluis Eriksson
Inside a Lean 4 formalization programme for four-dimensional SU(N_c) latticeYang-Mills, we machine-check the operator-theoretic criterion that standsbetween exponential decay of a Euclidean correlator and a spectral gap of atransfer operator. Let T be a bounded self-adjoint operator on a Hilbert spaceand W a unit vector fixed by T, so that TW = W, and put S = T - |W><W|.Exponential decay at rate r of the connected two-point function<v, T^n v> - |<W,v>|^2 at every v is equivalent to the operator-norm bound||S|| <= r.The substantive part is the dense-family criterion. WritingD_r = {v : there is C with ||S^n v|| <= C r^n for all n}, we prove that D_r isa linear subspace and that its density alone forces ||S|| <= r, the constantsbeing entirely unconstrained: a family of observables whose span is dense, eachcarrying its own finite constant, suffices. Consequently prefactors that growwith the support of the observable - the shape cluster expansions produce - donot obstruct the gap, provided the exponential rate is common to the family andthe family spans densely. Those two provisos are essential; without them thestatement is false.No mathematical novelty is claimed for the criterion itself, which we expect tobe known in the language of local spectral theory; what is offered is itsmechanization, its packaging for families of observables, and the consequencefor prefactors. We also record what the formalization does not contain: noOsterwalder-Seiler Hilbert space for any gauge theory, no reflection positivityof the Wilson measure, no identification of a Euclidean correlator with a matrixelement. Nothing here is a claim about the continuum limit or about the Clayproblem. All results are machine-checked with no sorry and no project axioms. (W stands for the vacuum vector Omega. If the form's preview renders Unicode cleanly you may substitute the real symbols; the ASCII form above is the safe default and matches the PDF's content either way.)
Research paperHistorical importARR-2026-151JHERTA88SSBWJ · v1
Lluis Eriksson
We give a machine-checked reduction of the finite-dimensional fluctuation integral in Balaban's CMP116 large-field analysis. Starting from the physical block constraint Q, the formal development constructs a sparse right inverse E and the constraint-elimination operator C = I - EQ. It proves QE = I, QC = 0, C² = C, the exact sparse norm ||EB|| = M^(d-1)||B||, and the volume-independent bound ||C|| ≤ 1 + M^(d-1) for d ≥ 3. An exact physical/CMP116 isometry transports C to finite Gaussian coordinates without norm loss. The same development constructs the physical localization projector P_Z0, evaluates the complex quadratic Gaussian, localizes its determinant to rank |I(Z0)|, performs the outer Gaussian integration, and absorbs both costs into an explicit exp(c|Z0|) factor.Two corrections exposed by formalization are central. First, the useful domination occurs after Gaussian integration rather than through an unavailable pointwise supremum in the fluctuation field. Second, the localized quadratic matrix is A = -alpha_5 P_Z0. In the exactly identified trivial-background sector, the terminal Lean theorem inserts the concrete C, the flat Hessian, complement localization, and covariance root directly into the printed source Gamma_k = C^T Delta_k (C P_Z0^c)(C^(k))^(1/2), returning an explicit Cauchy bound without an ambient-volume factor. CMP116, however, requires the base Hessian at a generally nontrivial small background Ubar. We do not construct D²S_Wilson(Ubar) or the random-walk estimate (2.16), and therefore do not prove the physical domination, (2.26), hraw, hRpoly, a continuum limit, or a mass gap. The contribution is an auditable reduction that closes the constraint and Gaussian layers and identifies the first genuinely missing interacting construction.
Research paperHistorical importARR-2026-2PB36YR0B89WSB71 · v1
Lluis Eriksson
We present an end-to-end Lean 4/Mathlib formalization of the exact evaluation of the two-dimensional SU(2) heat-kernel lattice model on certified finite combinatorial disk cellulations. The development starts from normalized Haar probability on the concrete matrix group SU(2). It identifies its transport to S^3 with the canonical spherical measure, proves an all-order orbital integration formula, derives translated character convolution, and passes from finite character sums to the infinite heat-kernel semigroup by dominated convergence. A genuine shared-edge integral then yields the two-face Migdal move.The geometric layer is independent of any reduction tree. A cellulation stores vertices, paired half-edges, cyclic face words, incidence, Euler characteristic, and positive face areas. Connected dual graphs admit certified elimination schedules, every valid schedule reduces to the heat kernel at total area, and all schedules give the same amplitude. For the original edge model, a rooted spanning tree produces a measurable, product-Haar-preserving gauge equivalence SU(2)^E ≃ SU(2)^(V{r}) × SU(2)^(ET). A compatible tree-cotree construction then retains the exterior holonomy rather than integrating it out. For every certified physical disk cellulation, the boundary-conditioned original-edge amplitude is exactly the SU(2) heat kernel at the total face area. Coefficient extraction gives, for every irreducible label n, the normalized exterior-boundary identity E_P[W_n(H_boundary)] = exp[-n(n+2)(sum_f t_f)/4], where H_boundary is the retained holonomy of the complete exterior boundary word. The universal record is demonstrably inhabited: a concrete three-spoke disk has (V,E,F)=(4,6,3) and derived dual graph K_3. A reproduced audit covers 177 audited declarations, explicitly including both headline theorems, and finds only propext, Classical.choice, and Quot.sound in their dependency cones. The analytic solution is classical. The contribution is a concrete kernel-checked composition from Haar measure and characters to physical edge variables, gauge fixing, tree-cotree elimination, and the exact boundary-observable endpoint.
Research paperHistorical importARR-2026-3Q0VH7PMNV8C9VQE · v1
Lluis Eriksson
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.
Research paperHistorical importARR-2026-0WG9YDY5BA9S3RF4 · v1
Lluis Eriksson
For SU(N_c) Wilson lattice gauge theory on d-dimensional periodic tori (d >= 2), we present a machine-checked (Lean 4, pinned Mathlib) renormalization-group interface for two-plaquette truncated correlators, in which every structural ingredient is a theorem rather than a postulate: the scale transformation is a concrete decimation map, defined once -- measurable, local, and gauge-covariant -- and its induced pushforward preserves probability; the effective measures are its literal iterated pushforwards of the Wilson Gibbs measure; the multiscale decomposition of the correlator is proved by telescoping, never carried as data; the terminal scale of the decomposition is a fixed index kTerm(n) = n with typed range 1 <= kTerm(n) <= n, which excludes, in the type, the circular depth-zero layer in which an infrared clause would hypothesize the bound being sought; the conditional decay conclusion is stated in the physical distance 2^n u with a single constant pair (C, m) quantified before every torus base and depth; and the terminal observable is operationally support-certified: the infrared object consumed by the interface equals a base-measure integral of an explicitly composed pullback observable whose dependence is contained in a transported support set, for which the separation lower bound 2^n(2u) - (2^n + 1), strictly positive on the whole interface window, is proved. The design is deliberately adversarial: four natural naive formulations are presented together with the explicit countermodels that defeat them -- scalar relabeling of known decay, sink flows on measures, clamped scales and per-volume constants, and depth-zero circularity -- and with the typed repairs that exclude each. The central hypothesis, PhysicalTerminalScaleWilsonGate, is an open proposition: no witness is provided, and the infrared/ultraviolet bounds it demands of the actual Wilson measure are exactly the open analytic mathematics (Balaban-type single-scale estimates). The final theorem is conditional: a witness of the gate yields |Cov(2^n u)| <= C e^{-m 2^n u} with one pair (C, m), m > 0, for every base M_0 >= 4 and every depth n >= 1. No mass-gap claim, no claim of gate satisfiability, and no thermodynamic or continuum limit is made or implied.
Research paperHistorical importARR-2026-1DNF7Z9F579X8SQA · v1
Lluis Eriksson
SUPERSEDED BY AI.VIXRA:2607.0039V1 FOR THE ORIGINAL-EDGE AND TREE-COTREE CLOSURE. This replacement preserves public version 1 and corrects its publication-level scope. Version 1 establishes the compact-group analytic chain, heat-kernel reductions, schedule independence and reduced-model results, but pages 7 and 9 leave open the bridge from the post-gauge-fixed evaluator to the original-edge physical integral for arbitrary cellulations. ai.viXra:2607.0039v1 supplies the missing original-edge gauge fixing, simultaneous face-holonomy transport and compatible tree-cotree closure and is therefore the authoritative source for the full exact simple-loop area-law theorem at the stated finite two-dimensional SU(2) heat-kernel scope. Neither paper constructs four-dimensional continuum Yang-Mills theory or proves a four-dimensional mass gap. The preserved version 1 follows the two-page notice unchanged.
Research paperHistorical importARR-2026-39Y0F83F4Z9JK90G · v1
Lluis Eriksson
For the one-parameter family B(x) = x/(nu+c+sqrt((nu+c)^2+x^2)) of Amos-type expressions, whose member c = 1/2 is the classical Amos-type upper bound for the modified Bessel ratio I_{nu+1}/I_nu, we formalize in Lean 4, at every real order nu >= 0 over the Gamma-power series, the classification of the parameter: B is a uniform upper bound for the ratio exactly when c <= 1/2, and a uniform lower bound for every c >= 1, with explicit rational counterexample witnesses (the classification itself is known mathematics, due to Ruiz-Antolin and Segura; we claim only the machine-checking). The contribution is the regime between the ends: for every nu >= 0 and c strictly between 1/2 and 1 we prove that the fixed family member crosses the ratio exactly once on (0, infinity) -- a transversal crossing in an explicit finite window, strictly above an explicit threshold, with globally determined sign on both sides and a two-sided scale law; degenerate contact is excluded by an exact second-derivative identity. The chain carries the axiom oracle [propext, Classical.choice, Quot.sound] and no analytic hypothesis beyond nu >= 0, x > 0; a pre-registered certified interval-arithmetic companion verifies the crossing phenomenon independently of the crossing theorems at 30 parameter pairs spanning the hard regimes, all passing at 128 bits.
Research paperHistorical importARR-2026-6YFENMGGBY9PPBF1 · v1
Lluis Eriksson
Soft spectral filtering has a more severe effect at finite filling than in a dilute edge-mode code. We consider two odd Su-Schrieffer-Heeger (SSH) rails, fill every negative-energy orbital, and encode one additional fermion in the zero mode of either rail. The code has fixed total number and supports physical coherence. For a boundary transfer at a site with zero-mode weight w_x, the desired logical Davies line has squared matrix element w_x^2. We prove the exact many-body leakage identity W_leak^filled(x) = (1 + 2w_x - 3w_x^2)/4. At the remote boundary, w_x = Theta(zeta^(2 ell)), so the logical line is Theta(zeta^(4 ell)) while the summed particle-hole leakage tends to 1/4. This differs qualitatively from the dilute identity w_x(1 - w_x) = Theta(zeta^(2 ell)).For a Davies filter whose off-target tail is epsilon_ell = exp[-q ell + o(ell)], the bounded-latency exact-refresh power obeys the exponent law lim_(ell to infinity) -(1/ell) log P_(ell,tau) = min{4m,q}, where m = -log zeta, under explicit uniform-envelope and resource-ledger assumptions. A width-independent tail, a special case with q = 0, produces a nonzero maintenance floor rather than merely halving the membrane exponent. More generally, q = 0 means only that the decay is subexponential. Every nonzero tail also makes the exact rapid-refresh limit logarithmically singular at each fixed width.The floor is not a free-fermion accident. For arbitrary interacting number-conserving rails, we prove an exact static identity expressing leakage as a local occupation product minus the logical matrix element. Uniform finite filling and remote-edge indistinguishability force a positive leakage floor. A new local spectral-window lemma places a fixed fraction of that weight in a width-independent Bohr-frequency window using only a commutator norm. Consequently, any bath tail bounded below on that window yields an interaction-stable Davies leakage floor. Quasi-local spectral flow shows persistence in a neighborhood of a symmetry-preserving gapped SSH phase. Exact diagonalization of the interacting spinless SSH chain shows that repulsive and attractive interactions change the observed edge-localization exponent while the leakage is already driven close to 1/4 at accessible widths.
Research paperHistorical importARR-2026-2PYSR8HXMA8RD8RV · v1
Lluis Eriksson
Exact rapid maintenance behaves singularly at the boundary of quantum state space. Let a finite-dimensional target rho have support projector P, and let an uncontrolled quantum Markov semigroup have outward support-leakage rate a = Tr[(1-P)L(rho)]. We prove that, whenever a > 0, the nonequilibrium free-energy loss has the universal short-time form F(rho) - F(exp(tL)rho) = k_B T a t log(1/t) + O(t). Under an explicit fresh-resource-cell ledger, the optimal period-t exact-refresh power therefore diverges as k_B T a log(1/t). For GKLS generators, a is a positive sum of squared support-crossing jump amplitudes. We prove the complete dichotomy: a > 0 gives logarithmically infinite rapid power, while a = 0 gives finite rapid power even when Hamiltonian rotation produces population outside the fixed initial support at second order. We also define a periodic threshold-reset corridor and prove its sharp k_B T a log(1/r) + O(1) small-corridor law.The general singularity has an unexpected geometric consequence. In a fixed-parity dual-rail SSH code, a boundary transfer has desired logical weight w_x^2, but its exact summed zero-mode-to-bulk weight is w_x(1-w_x). At the remote boundary, these scale respectively as Theta(zeta^(4 ell)) and Theta(zeta^(2 ell)). Thus a soft spectral tail changes the exponential rate of bounded-latency refresh from 4|log zeta| to 2|log zeta| unless the tail itself is suppressed at least as zeta^(2 ell). We prove the general rate formula min{4m, 2m+q}, where m = -log zeta and q is the exponential suppression rate of the spectral tail. Exact rapid maintenance and the wide-membrane limit do not commute: every nonzero tail gives infinite rapid power at fixed width, while fixed-period power still vanishes exponentially with width. The result turns perfect filtering from a technical convenience into the sharp boundary between finite and singular exact maintenance.
Research paperHistorical importARR-2026-4GJP1XS78A95XS6H · v1
Lluis Eriksson
The tangent cone of quantum state space at a rank-deficient density matrix is known to have a positive exterior block, and recent work identifies all of its directions with Lindbladian velocities. We derive a quantitative stabilization consequence of this geometry. Let rho be a finite-dimensional target with support projector P, set Q = 1 - P, and let an uncontrolled GKLS generator L have outward support-leakage rate a = Tr[Q L(rho)] > 0. Every additive GKLS controller, including a bounded time-dependent controller, has its own nonnegative outward rate at rho and therefore cannot cancel a. Consequently, no finite-rate additive Markovian controller can keep the system exactly at the target. The conclusion persists for arbitrary finite-dimensional autonomous ancillas, provided the adverse system generator remains additive and local to the system.Under induced trace-norm bounds ||L|| <= M and ||K_t|| <= Gamma, we prove the dynamic corridor inequality limsup ||rho_t - rho||_1 >= 2a/(M + Gamma), without assuming convergence to a stationary state. An autonomous Poisson-reset generator supplies a matching inverse-rate upper bound, establishing the order-optimal minimax law Theta(Gamma^{-1}).For a soft-filter dual-rail SSH family, the microscopic leakage coefficient scales as exp[-(2m + q)ell + o(ell)], whereas the ideal logical disturbance scales as exp[-4m ell + O(1)]. We derive the exact controller-growth threshold g_min = max{0, 2m - q}. Thus, below the filter threshold q = 2m, retaining ideal logical accuracy requires an exponentially growing autonomous correction intensity.
Research paperHistorical importARR-2026-77MR0BB1E487CAYR · v1
Lluis Eriksson
Lower bounds based on the instantaneous free-energy loss of a target state are often interpreted as lower bounds on the power required to maintain that state. We show that this interpretation depends decisively on the control task. If maintenance only requires exact restoration at periodically sampled endpoints and the intervention period is unrestricted, the infimal average power can vanish even when the target has strictly positive instantaneous entropy production. A full-rank dephasing qubit gives an exact energy-conserving SWAP counterexample. We repair the formulation by separating endpoint restoration, bounded-latency maintenance, and continuous holding.For continuous-time finite Markov chains we adopt the established trajectory-relative-entropy holding cost and review the known reversible optimizer and Dirichlet-form representation. Our first composition result is then an exact geometric additivity theorem for suppressible and persistent generators sharing a detailed-balance reference. A two-state counterexample shows that this hypothesis is essential: channels with incompatible equilibria can cancel at a finite membrane width. A dual-rail pair of odd fermionic SSH chains supplies the microscopic layer: exact edge modes, a uniform bulk gap, and an explicitly filtered number-conserving Davies coupling produce two-sided holding-cost bounds without an assumed rate-inheritance bridge. The logical basis has fixed particle number and parity, so arbitrary logical coherence is physical under fermionic superselection. Finally, under a fully axiomatized resource-cell ledger, fresh target-state cells and energy-conserving SWAPs saturate the fixed-period free-energy bound; the correctly ordered rapid-control limit closes the SSH theorem for coherent logical targets. The fresh-copy construction is related to earlier collision-model stabilization work and is not claimed as a work-only controller. The remaining frontier is autonomous work-only control without preloaded target copies.
Research paperHistorical importARR-2026-3AJ7W5BS3N9VR8KM · v1
Lluis Eriksson
The Amos-type upper bound for the modified Bessel function ratio, rho_nu(x) = I_{nu+1}(x)/I_nu(x) < x/(nu + 1/2 + sqrt((nu+1/2)^2 + x^2)), is classical, and its derivation through the qualitative theory of the associated Riccati equation is an established technique. A companion paper formalized the bound at integer order over a factorial power series. This paper extends the formalization to every real order nu >= 0: the function I_nu is defined by its Gamma-power series (real exponents via rpow), and the complete chain — convergence, positivity, the three-term recurrence, termwise differentiation with a dominated-derivative argument that must treat the leading term separately (its exponent nu-1 is negative for nu < 1), the Riccati equation, a small-argument zone bound uniform in nu, and a first-crossing barrier — is machine-checked in Lean 4 with axiom oracle [propext, Classical.choice, Quot.sound] and no analytic hypothesis beyond nu >= 0, x > 0. Two structural locks tie the result to the integer development: an identification theorem proves that at nu = n the Gamma-series object coincides with the factorial-series object, so the integer-order theorem of the companion development is recovered as a corollary in three rewrites; and a genuinely non-integer instance at nu = 1/2 witnesses that the endpoint lives outside the natural-number embedding. The theorem is proved for the in-core Gamma-series definition; no identification with an external special-functions library object is claimed.
Research paperHistorical importARR-2026-17K7KRR6NH9ZVAEJ · v1
Lluis Eriksson
Amos's upper bound for the modified Bessel function ratio, rho_n(x) = I_{n+1}(x)/I_n(x) < x/(n + 1/2 + sqrt((n+1/2)^2 + x^2)) = B_n(x), is a classical theorem, and its derivation through the qualitative theory of the associated Riccati equation is an established technique. This paper contributes, to our knowledge, the first formalization: a complete, machine-checked Lean 4 proof of the bound for every integer order n >= 0 and every x > 0, over the power-series definition of I_n carried in the same pinned development, with axiom oracle [propext, Classical.choice, Quot.sound] and no analytic hypothesis of any kind. The formalized route runs through the Riccati equation rho_n' = 1 - ((2n+1)/x) rho_n - rho_n^2 (itself derived from the formalized series calculus), the observation that B_n is exactly the positive root of the Riccati quadratic, a small-argument zone bound uniform in n obtained from pure geometric tail estimates, and a first-crossing barrier argument in a transformed variable psi_n = x(1/rho_n - rho_n) whose structural feature — every touch of the critical level forces rho_n' = 0, so the barrier never needs to be differentiated — is the simplification this formalization contributes. As corollaries, the unit-step inequality, the strict monotonicity of the logarithmic derivative across orders (in deriv form), and a phi-monotonicity step used by a lattice-gauge surface expansion all become unconditional theorems. The theorem is proved for the in-core power-series definition of the integer-order modified Bessel function; no formal identification with an external special-functions library object, and no extension to noninteger order, is claimed.
Research paperHistorical importARR-2026-6DP8SDRZ678H9AY9 · v1
Lluis Eriksson
The Amos-type upper bound on the modified-Bessel ratio, I{nu+1}(x)/I_nu(x) < x/(nu + 1/2 + sqrt((nu+1/2)^2 + x^2)), has a distinguished algebraic property: its right-hand side U satisfies the exact calibration identity 1/U - U = (2nu+1)/x. From that identity alone — by ordered-field algebra, with no further analytic input — follow a unit-step inequality rho_nu - rho{nu+1} < 1/x for consecutive ratios, the strict increase of the log-derivative (log I_nu)' = rho_nu + nu/x across orders, and the strict monotonicity of a phi-sequence arising in a two-dimensional lattice-gauge surface expansion. We formalize this calculus in Lean 4: a single module defines the bound once (AmosBound) and proves the calibration engine and four consequence theorems through that one definition, together with two rational satisfiability witnesses whose Amos hypothesis holds by exact Pythagorean arithmetic; all eighteen Lean statements of the development pass the axiom oracle with exactly [propext, Classical.choice, Quot.sound] against a pinned Mathlib. A certified companion (256-bit interval arithmetic, self-contained series-plus-tail enclosures, committed transcript) certifies the bound provably strictly at all 1206 points of a pre-registered grid covering the arguments the applications consume. A Bessel interface completes the closure: integer-order I_n is defined by its power series in the same pinned development, with positivity, the three-term recurrence, the termwise-differentiated derivative identity I_n' = I_{n+1} + (n/x) I_n, and the logarithmic-derivative identity (log I_n)' = rho_n + n/x all proved as theorems, so the consequence theorems — including the unit step read as strict log-derivative monotonicity, in deriv form — hold for genuine Bessel ratios with the Amos bound as the single remaining hypothesis. The scope is stated exactly: the Amos bound itself remains a classical cited theorem taken as hypothesis — this paper unifies its three previously scattered uses in our formal development into one named proposition with one oracle and one certified numerical witness, and no downstream result changes its verification class.
Research paperHistorical importARR-2026-505NQZHR7P9TQ8SA · v1
Lluis Eriksson
We present a machine-checked quantitative toolkit for cluster expansions of polymer systems with excluded regions (holes), in the discrete cube geometry of Balaban-Dimock renormalization-group analyses. Five Lean 4 theorems, checked against a pinned Mathlib revision, provide: (i) the identity sum_T prod_v c_T(v)! = n! C_n for child factorials over spanning trees of the complete graph K_(n+1), with the rooted-tree majorant 4^n as corollary; (ii) a marked-root leaf summation for the tree-graph majorant of an Ursell-type expansion with holes, with the moment constant M paid once at the root and closed leaf ratio 4M^2 per additional vertex, together with its Catalan-sharpened form M^(2n+1) C_n (a gain of order n^(3/2) in the n-th coefficient); and (iii) a target-preserving orderwise bound in which the target union itself survives until the modified-metric exponential is extracted. A certified companion (interval arithmetic, 120-bit precision, committed transcript with a committed reproduction witness) tabulates the smallness gate and encloses every derived constant. Non-vacuity is machine-checked: a concrete hole family satisfying every hypothesis is exhibited in Lean, and the two distinct hypothesis sets among the polymer-facing theorems are both instantiated at it with a strictly positive weight. Each claim is labelled with its verification layer: exact (Lean theorem), certified (interval transcript), or paper-level.
Research paperHistorical importARR-2026-1FPFA1TSMY9M3T9S · v1
Lluis Eriksson
SUPERSEDED BY AI.VIXRA:2607.0089V1 FOR THE TERMINAL GLOBAL-SIGN CLAIM; INDEPENDENT REPLAY PENDING. This replacement preserves public version 1 and records the later terminal-claim paper without overstating its audit status. Version 1 proves positivity of F_B, the ratio sign for 0 < beta <= 3, exact bridge and single-Bessel reductions, certified negative results, asymptotic structure and a two-scale closure map; pages 11-13 leave the global sign as a quantified conjecture. ai.viXra:2607.0089v1 claims the global ratio-monotonicity theorem through exact identities and outward-rounded interval certificates. It supersedes this record for that terminal claim, but independent replay of every exact-to-Arb handoff and interval regime remains pending in this audit. No PASS is inferred from a printed or green transcript alone. The preserved version 1 follows the two-page notice unchanged.
