sr_symmetry
plain-language theorem explainer
The declaration establishes symmetry of the recognition cost under argument inversion for positive reals. Workers deriving special relativity from recognition principles cite it to confirm absence of preferred direction in the cost function. Proof proceeds by direct appeal to the core algebraic symmetry lemma.
Claim. For all $β > 0$, $J(β) = J(β^{-1})$, where $J$ is the recognition cost function.
background
The Special Relativity from RS module extracts SR principles from recognition science. It lists four core properties: J diverges as velocity approaches c, J(1) = 0 at rest, time dilation equals motion cost, and J is symmetric under sign flip of velocity (no preferred direction). The cost function Jcost implements these properties in the Cost module.
proof idea
One-line wrapper that applies the Jcost_symm lemma to the positivity hypothesis hr.
why it matters
It supplies the symmetric field inside specialRelativityCert, which bundles the five SR effects with the foundational RS properties. This realizes the fourth principle in the module documentation and closes the basic symmetry step before velocity addition or other effects are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.