lorentzTransformCount
plain-language theorem explainer
Recognition Science enumerates exactly five Lorentz transformation types from J-cost invariance under boost inversion. A physicist reconstructing Lorentz symmetry from the Recognition Composition Law would cite this cardinality to confirm that boosts, rotations, time reversals, spatial inversions, and CPT exhaust the discrete types matching configDim equals five. The proof is a one-line decision procedure that evaluates the automatically derived Fintype instance on the inductive type definition.
Claim. The set of Lorentz transformation types consisting of boosts, rotations, time reversals, spatial inversions, and CPT transformations has cardinality five.
background
The module treats J-cost invariance J(r) = J(r^{-1}) as the Recognition Science restatement of Lorentz symmetry, implying no preferred rest frame at the equilibrium point x=1. Five discrete transformation types are identified with the configuration dimension in the reconstruction, where Lorentz contraction arises from minimising J over intervals and time dilation from frequency ratios. Upstream results supply the inductive definition of the type together with collision-free structures from option-A empirical programs and simplicial edge lengths that underwrite the symmetry claims.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the Fintype.card expression. The tactic computes the cardinality by enumerating the five constructors of the inductive type, which derives its Fintype, DecidableEq, and BEq instances automatically from the declaration.
why it matters
The result supplies the five_types component of the lorentzSymmetryCert definition that certifies the full symmetry package including rest-frame equilibrium and moving-frame cost. It fills the structural slot in the module's reconstruction of Lorentz invariance from J-cost, aligning with the eight-tick octave and the claim that configDim equals five while remaining consistent with D equals three spatial dimensions in the unified forcing chain. No open scaffolding remains on this count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.