mass_energy_pos
plain-language theorem explainer
The declaration establishes that the mass-energy quantity on the recognition phi-ladder is strictly positive for every natural-number rung r. Researchers deriving special relativity from J-cost symmetries would cite this to confirm the energy scale remains positive in RS units. The proof is a one-line term-mode reduction that unfolds the definition and applies positivity of powers of phi.
Claim. For every natural number $r$, $0 < m c^2$ where $m c^2 = phi^r * phi^{-5}$ is the mass-energy on the phi-ladder at rung $r$ (with $c=1$ in recognition units).
background
The SpecialRelativityDeep module derives special relativity from the recognition framework: c equals 1, Lorentz transformations are symmetries of the J-cost function, and the invariant interval is the recognition metric. The mass-energy quantity is introduced via the upstream definition mass_energy_RS r := phi^r * phi^(-5), which places m c^2 on the phi-ladder at rung r and incorporates the RS-native constant hbar = phi^{-5}. This sits inside the broader structural claim that gamma = cosh(theta) with J(gamma) = gamma - 1.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of mass_energy_RS and applies mul_pos to the pair (pow_pos phi_pos r, zpow_pos phi_pos (-5)).
why it matters
This supplies the mass_energy_pos field inside the SpecialRelativityDeepCert structure, which certifies that special relativity follows from J-cost symmetry. It closes the positivity requirement for the mass-energy expression on the phi-ladder, aligning with the framework's T6 phi fixed point and the mass formula yardstick * phi^rung. The result feeds directly into the master certificate that packages jcost_cosh_identity, mass_energy_pos, and structural triviality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.