LorentzSymmetryCert
plain-language theorem explainer
LorentzSymmetryCert packages four properties that certify emergence of Lorentz symmetry from the J-cost function. A physicist reconstructing special relativity via recognition costs would cite it to assert five transformation types together with invariance under velocity inversion and equilibrium at the rest frame. The declaration is a bare structure definition that collects pre-proved lemmas on J-cost symmetry and rest-frame zero without further derivation steps.
Claim. A structure that asserts: the set of Lorentz transformation types (boost, rotation, time reversal, spatial inversion, CPT) has cardinality 5; the recognition cost satisfies $J(r) = J(r^{-1})$ for all $r > 0$; the recognition cost vanishes at the unit ratio, $J(1) = 0$; and the recognition cost is strictly positive for all $r > 0$ with $r ≠ 1$.
background
The module reconstructs Lorentz symmetry from Recognition Science by treating J-cost as the recognition cost of an observed velocity ratio. J-cost invariance under inversion is presented as the RS restatement of no preferred rest frame, while the rest frame itself is the equilibrium point where cost vanishes. Upstream, the rest_frame theorem states that Jcost 1 = 0 as recognition equilibrium, and the LorentzTransformType inductive enumerates exactly the five types that match configDim D = 5.
proof idea
This is a structure definition with an empty proof body. The four fields are later instantiated by a one-line wrapper that supplies lorentzTransformCount for the cardinality, lorentz_symmetry for the inversion equality, rest_frame_equilibrium for the zero at unity, and moving_frame_cost for strict positivity away from rest.
why it matters
The structure supplies the certificate that J-cost symmetry restates Lorentz symmetry inside Recognition Science and directly supports the five-type count from configDim D = 5. It is the immediate parent of the lorentzSymmetryCert definition that assembles the full certificate. In the broader framework this closes the RS derivation of special relativity from the J-cost functional equation, consistent with the forcing chain steps that fix D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.