jcost_cosh_is_gamma_minus_one
plain-language theorem explainer
The theorem shows that the J-cost of cosh θ equals cosh θ minus one for any real rapidity θ. Researchers deriving special relativity from the recognition cost function cite this when connecting rapidity to the Lorentz factor γ. The proof is a short algebraic reduction that unfolds Jcost, invokes cosh positivity, rewrites via the inverse formula, and simplifies by ring.
Claim. For every real number $θ$, $J(∅cosh θ) = ∅cosh θ - 1$, where $J$ is the J-cost function and $∅cosh θ$ is the Lorentz factor $γ$.
background
The Special Relativity Deep module derives special relativity structurally from the recognition framework with $c=1$. The J-cost satisfies $J(x) = (x + x^{-1})/2 - 1$ for $x>0$, equivalently $∅cosh(log x) - 1$. Rapidity $θ$ satisfies $γ = ∅cosh θ$ with $θ = atanh(v/c)$, so the identity reads $J(γ) = γ - 1 ≥ 0$. Upstream results supply rung definitions on the φ-ladder for masses and the BRF theta transform, but the present theorem rests only on the Jcost definition and standard hyperbolic identities.
proof idea
Unfold Jcost to expose the explicit form involving the inverse. Apply Real.cosh_pos to obtain the positivity hypothesis. Rewrite using Real.cosh_inv on the positive cosh θ. Finish with ring to cancel terms and obtain the identity.
why it matters
The result supplies the jcost_cosh_identity field inside specialRelativityDeepCert. It completes the structural link between J-cost and γ - 1 required for the recognition derivation of Lorentz symmetry, aligning with J-uniqueness (T5) and the eight-tick octave in the forcing chain. The module doc-comment states that Lorentz transformations are the symmetries of the J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.