RQFTCert
plain-language theorem explainer
RQFTCert packages the assertion that the inductive type of five Wightman axioms has cardinality exactly 5 and satisfies the identity 5 equals 3 plus 2. Axiomatic QFT researchers would cite it to confirm that the recognition lattice reproduces the standard Wightman set via the J-cost features. The declaration is a bare structure definition that directly records the two cardinality equations.
Claim. Let $W$ be the inductive type whose constructors are the five Wightman axioms $W0Lorentz$, $W1Spectral$, $W2Vacuum$, $W3Completeness$, $W4Commutativity$. The structure $RQFTCert$ asserts that the cardinality of $W$ equals 5 and that this cardinality equals 3 plus 2.
background
The module extracts five canonical QFT features from the recognition lattice: Lorentz invariance via $J(r) = J(r^{-1})$, CPT symmetry from $J$ symmetry, unitarity through total conservation, causality at the lightcone, and locality between adjacent sites. These map directly onto the five Wightman axioms. The inductive type WightmanAxiomW enumerates exactly these five cases and carries the Fintype instance required for cardinality statements. The local setting equates the axiom count to configuration dimension $D = 5$.
proof idea
The declaration is a structure definition whose two fields simply state the cardinality equalities for WightmanAxiomW. No lemmas, tactics, or reductions are invoked.
why it matters
RQFTCert supplies the certified object instantiated by the downstream definition rqftCert, which applies the count lemmas wightmanCount and wightman_5_eq_Dp2. It thereby closes the structural opening that identifies the five RS-derived axioms with the canonical Wightman set and confirms five axioms equal configDim $D = 5$. The step supports derivation of QFT axioms from the recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.