wightmanAxiomCount
plain-language theorem explainer
The Recognition Science Hilbert space realizes exactly five Wightman axioms, enumerated by the inductive type whose constructors label Lorentz invariance, spectral positivity, vacuum existence, state completeness, and local commutativity. Axiomatic QFT researchers embedding the RS construction would cite this cardinality to confirm consistency with the spatial configuration dimension. The proof is a one-line decision procedure that computes the finite type cardinality directly from the five constructors.
Claim. The set of Wightman axioms realized on the Recognition Science Hilbert space $H_{RS}$ has cardinality five: Lorentz invariance (W0), spectral condition (W1), vacuum existence (W2), completeness of states (W3), and local commutativity (W4).
background
The module records the status of the Wightman axioms inside the Recognition Science framework on the Hilbert space $H_{RS}$. This space carries Lorentz invariance from J-cost symmetry, the positive-energy spectral condition, a vacuum state with J-cost zero, completeness of states, and local commutativity (sector-dependent). The inductive type enumerates precisely these five properties as W0 through W4, with W5 following automatically. Upstream, the vacuum is defined as the gauge bond configuration with all bonds at rung zero, and the spectral condition draws on the characteristic peak relation from the asteroid ore spectroscopy class.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the automatically derived Fintype instance of the inductive type with five constructors.
why it matters
This cardinality supplies the five_axioms field of the WightmanStatusCert certificate, confirming that the Recognition Science model meets the axiom count required for dimensional consistency with the framework's D = 3 spatial dimensions and eight-tick octave. It closes the enumeration step in the module's summary of W0-W4 status while leaving the sector-dependence of W4 and the continuum limit as the remaining gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.