LorentzTransformType
plain-language theorem explainer
LorentzTransformType enumerates the five Lorentz transformations recognized from J-cost invariance in the Recognition Science reconstruction. Physicists deriving frame-independent symmetry from the functional equation would cite this enumeration to fix the configuration dimension at five. The definition proceeds by direct inductive listing of the constructors boost, rotation, timeReversal, spatialInversion, and CPT, with Fintype derived for immediate cardinality access.
Claim. The type of Lorentz transformations consists of the five elements corresponding to boosts, rotations, time reversals, spatial inversions, and CPT transformations.
background
The module reconstructs Lorentz symmetry from the recognition cost J, where J(r) = J(r^{-1}) encodes invariance under velocity inversion and therefore the absence of a preferred rest frame. J-cost is applied to observed velocity ratios, with Lorentz contraction arising as its minimization over spacetime intervals and time dilation as its action on frequency ratios. The local setting identifies exactly five transformation types whose count equals the configuration dimension D = 5.
proof idea
Direct inductive definition with five constructors, deriving DecidableEq, Repr, BEq, and Fintype to enable decidable equality and finite-set cardinality.
why it matters
The enumeration supplies the five_types field required by the LorentzSymmetryCert structure and the immediate cardinality result in lorentzTransformCount. It realizes the structural claim that five transformation types implement configDim D = 5, thereby connecting J-invariance to the full Lorentz group in the Recognition Science framework. The parent certificates use it to certify symmetry, rest-frame equilibrium at Jcost 1 = 0, and positive cost for moving frames.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.