specialRelativityDeepCert
plain-language theorem explainer
This definition assembles the master certificate for special relativity by bundling the J-cost identity at rapidity with positivity of the mass-energy term. Researchers deriving Lorentz invariance from recognition cost functions cite it to confirm that the Lorentz factor satisfies gamma equals one plus J of cosh theta. The construction is a direct record assignment pulling the identity from the upstream J-cost theorem, positivity from the mass-energy theorem, and the trivial structural flag.
Claim. The certificate asserts that $Jcost(cosh θ) = cosh θ - 1$ for every real rapidity $θ$, that the mass-energy function at natural-number rung $r$ is strictly positive, and that the structural property of special relativity holds trivially.
background
The SpecialRelativityDeep module derives special relativity from the recognition framework by showing that the speed of light is the canonical propagation speed and that Lorentz transformations are symmetries of the J-cost function. The invariant interval follows from the recognition metric with $c=1$ in native units. The J-cost function satisfies $J(cosh θ) = cosh θ - 1 = γ - 1 ≥ 0$, where γ is the Lorentz factor at rapidity θ, as stated in the upstream theorem: 'J-cost at rapidity: J(cosh θ) = cosh θ - 1 = γ - 1 ≥ 0.' The mass-energy expression at phi-ladder rung r is positive by construction from phi^r times phi^{-5}.
proof idea
The definition is a direct record constructor. It assigns the jcost_cosh_identity field from the theorem jcost_cosh_is_gamma_minus_one, the mass_energy_pos field from the theorem mass_energy_pos, and the structural field from the trivial proposition.
why it matters
This certificate is the master structural theorem for special relativity in the recognition framework and directly supplies the witness for the downstream inhabitedness result. It completes the module claim that special relativity follows from J-cost symmetry, linking to the J-uniqueness step T5 and the self-similar fixed point phi. The derivation carries zero axioms and closes the structural part of the SR derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.