rest_frame
plain-language theorem explainer
The recognition cost function evaluates to zero at unit ratio, establishing the rest frame as the equilibrium in the Recognition Science derivation of special relativity. Researchers constructing Lorentz symmetry certificates from recognition principles cite this as the zero anchor. The proof is a direct term application of the unit lemma for the recognition cost definition.
Claim. $J(1) = 0$, where the recognition cost is given by $J(x) = (x-1)^2 / (2x)$.
background
The recognition cost is the function induced by a multiplicative recognizer on positive ratios, expressed as the squared ratio $J(x) = (x-1)^2 / (2x)$. In the Special Relativity from RS setting, this supplies the principle that the rest frame corresponds to recognition equilibrium with zero cost, alongside divergence at the speed of light and symmetry under inversion. The upstream unit lemma states: J(x) expressed as a squared ratio: J(x) = (x-1)²/(2x).
proof idea
The proof is a one-line term wrapper applying the unit lemma for the recognition cost, which evaluates the squared-ratio definition at argument 1 to yield zero.
why it matters
This result supplies the rest-zero component in the special relativity certificate structure and the rest-frame component in the Lorentz symmetry certificate. It realizes the zero-cost equilibrium for the rest frame in the recognition-to-special-relativity derivation, anchoring the five canonical effects and the symmetry properties. In the broader framework it corresponds to the fixed point of the J-uniqueness relation at the recognition equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.