motion_cost
plain-language theorem explainer
The theorem establishes that the recognition cost J(r) is strictly positive for every positive real r different from one. Physicists deriving special relativity from recognition principles would cite it to confirm that motion away from the rest frame carries nonzero cost. The proof is a direct one-line application of the general J-cost positivity lemma.
Claim. Let $J$ denote the recognition cost function. Then $J(r) > 0$ for every real number $r > 0$ with $r ≠ 1$.
background
The module derives special relativity principles from recognition science. It records that $J(v/c)$ diverges as $v$ approaches $c$, $J(1) = 0$ at the rest frame, time dilation equals the recognition cost of the proper-to-dilated time ratio, and $J$ is symmetric under inversion. The J-cost function measures the recognition cost of a ratio $r$, vanishing only at equilibrium $r = 1$. The upstream lemma states: 'J(x) > 0 for x ≠ 1 and x > 0.' It is proved by rewriting via the squared-difference expression and verifying that the numerator square is positive while the denominator remains positive.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one. That lemma rewrites the cost via Jcost_eq_sq, notes that the numerator square is positive when the argument differs from one, and concludes positivity of the quotient.
why it matters
This result supplies the motion_positive field inside the specialRelativityCert definition that certifies the five SR effects. It directly implements the module statement that motion carries positive recognition cost off rest. In the framework it supports J-uniqueness from the forcing chain and the reduction of SR effects to configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.