WightmanStatusCert
plain-language theorem explainer
The declaration defines a record type that certifies the five Wightman axioms hold on the Recognition Science Hilbert space H_RS via the J-cost function. A researcher in axiomatic QFT or RS unification would cite it to record that Lorentz invariance, spectral positivity, vacuum existence, completeness and commutativity are satisfied. The structure simply packages the axiom enumeration with three properties extracted from J-cost symmetry and the vacuum definition.
Claim. A structure consisting of: the set of Wightman axioms has cardinality 5; the J-cost of the vacuum gauge-bond configuration equals zero; for every positive real $r$ with $r$ not equal to 1 the J-cost is strictly positive; and the J-cost is invariant under $r$ to $r^{-1}$.
background
The module summarises the status of the Wightman axioms on the RS Hilbert space H_RS. The inductive type WightmanAxiom enumerates exactly five constructors: W0_lorentz (Lorentz invariance from J-cost symmetry), W1_spectral (positive-energy constraint), W2_vacuum (J=0 state), W3_completeness and W4_commutativity (sector-dependent). The upstream vacuum definition sets every gauge bond to rung 0 and supplies the zero J-cost reference state.
proof idea
This is a plain structure definition. It records the Fintype cardinality of WightmanAxiom together with the three properties (vacuum J-cost zero, spectral positivity, Lorentz invariance) that are supplied by sibling definitions in the same module. No tactics or lemmas are invoked inside the structure itself.
why it matters
The structure supplies the type that wightmanStatusCert inhabits, thereby closing the summary of the five Wightman axioms (W0-W4) in the Recognition Science framework. It directly encodes the J-cost symmetry that enforces W0 and W1 and the vacuum from the Yang-Mills mass-gap construction. The module notes that W4 remains sector-dependent and that the continuum limit is still open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.