wightman_5_eq_Dp2
plain-language theorem explainer
The declaration establishes that the inductive type of five Wightman axioms has cardinality exactly five, matching the configuration dimension D=5 in the Recognition Science lattice for relativistic QFT. A researcher deriving QFT structures from RS would cite this result to confirm the axiom count aligns with the five structural features. The proof is a one-line decide tactic that evaluates the finite type cardinality directly from the inductive definition.
Claim. The set of Wightman axioms has cardinality five: $|W_0, W_1, W_2, W_3, W_4| = 5$.
background
The module opens the derivation of relativistic QFT from the RS recognition lattice by listing five canonical features: Lorentz invariance via J(r) = J(r^{-1}), CPT symmetry from J symmetry, unitarity from total J conservation, causality from J vanishing at the lightcone, and locality from J couplings only between adjacent sites. These map directly to the five Wightman axioms W0 through W4, with the module stating that five axioms equal configDim D = 5 and that Lean encodes them structurally with zero sorrys or axioms.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic computes the Fintype.card of the inductive type WightmanAxiomW (with constructors W0Lorentz, W1Spectral, W2Vacuum, W3Completeness, W4Commutativity) and confirms the value equals 3 + 2 without invoking additional lemmas.
why it matters
This theorem supplies the five_Dp2 field in the rqftCert definition that certifies the full RQFT structure. It fills the structural claim that the five Wightman axioms correspond to D = 5, linking the RS lattice features (Lorentz invariance, CPT symmetry, unitarity, causality, locality) to the axiom set. The result supports the module's assertion of zero-sorry structural proofs for these axioms on H_RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.