WightmanAxiom
plain-language theorem explainer
The inductive type enumerates the five Wightman axioms realized on the RS Hilbert space H_RS. Axiomatic QFT researchers cite it when verifying that the Recognition Science model meets the standard Wightman criteria. The definition consists of five constructors together with derived instances for decidable equality and finiteness.
Claim. Let $W$ be the inductive type generated by the five constructors $W_0$ (Lorentz invariance), $W_1$ (spectral positivity), $W_2$ (vacuum existence), $W_3$ (completeness), and $W_4$ (local commutativity). The type carries decidable equality, representation, boolean equality, and finite cardinality.
background
The module records the status of the Wightman axioms inside the Recognition Science Hilbert space $H_{RS}$. This space satisfies W0 via J-cost symmetry, W1 via the positive-energy constraint, W2 via the J=0 vacuum state, W3 via completeness of states, and W4 via local commutativity (still sector-dependent). The five axioms are identified with configuration dimension D=5. The Cost module supplies the Jcost function used in the concrete properties listed downstream.
proof idea
The declaration is an inductive definition that introduces the five constructors and derives DecidableEq, Repr, BEq, and Fintype instances via the single deriving clause.
why it matters
The enumeration feeds the certification theorems that confirm the RS model satisfies the Wightman framework. It is used by wightmanAxiomCount to establish cardinality 5 and by WightmanStatusCert to record the concrete properties vacuum Jcost 1 = 0, spectral positivity for r ≠ 1, and Lorentz invariance Jcost r = Jcost r^{-1}. The definition closes the foundation summary while leaving open the sector dependence of W4 and the continuum limit. It aligns with the derivation of physical dimensions and symmetries from the J functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.