wightmanStatusCert
plain-language theorem explainer
This definition assembles a record that certifies five Wightman axioms hold on the Recognition Science Hilbert space H_RS. An axiomatic QFT researcher would cite it to record the current status of W0-W4 before addressing the remaining sector gap. The construction is a direct record literal that populates each field from the supporting theorems on cardinality, vacuum, positivity, and symmetry.
Claim. Let $J$ denote the J-cost function on positive reals. A certificate $C$ exists such that the set of Wightman axioms has cardinality 5, $J(1)=0$, $J(r)>0$ whenever $r>0$ and $r≠1$, and $J(r)=J(r^{-1})$ for all $r>0$.
background
The J-cost function satisfies J(1)=0 by Jcost_unit0, strict positivity off the unit by Jcost_pos_of_ne_one, and symmetry J(r)=J(r^{-1}) by Jcost_symm. The module states that H_RS carries W0 (Lorentz invariance from J-cost symmetry), W1 (spectral positivity), W2 (vacuum existence), W3 (state completeness), and W4 (local commutativity, sector-dependent). Five axioms correspond to configDim D=5; the upstream vacuum definition from Yang-MillsMassGap supplies the zero-bond configuration used for Jcost 1=0.
proof idea
The definition is a direct record construction. It assigns the five_axioms field to the decidable cardinality theorem wightmanAxiomCount, the vacuum field to vacuum_exists, the spectral field to spectral_positivity, and the lorentz field to lorentz_invariance.
why it matters
The certificate records that W0-W4 hold with zero sorrys inside the Recognition Science framework, closing the status summary for the S1 depth module. It sits downstream of the J-cost axioms and upstream of unification results such as the Yang-Mills vacuum. The module explicitly flags the open W4 sector-dependence and continuum-limit gap, consistent with the T0-T8 chain where D=3 is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.