pith. sign in
module module high

IndisputableMonolith.Foundation.SpecialRelativityDeep

show as:
view Lean formalization →

The module develops special relativity within Recognition Science by establishing that the Lorentz factor satisfies gamma greater than or equal to 1 and by linking it to the J-cost function. Researchers extending the RS forcing chain to relativistic kinematics would cite these results. It consists of targeted sibling theorems and definitions that rest directly on the imported Constants and Cost modules.

claimThe Lorentz factor satisfies $gamma geq 1$. Related statements equate the J-cost of the hyperbolic cosine to $gamma minus 1$ and express mass-energy equivalence in RS-native units.

background

The module imports Constants, which fixes the fundamental RS time quantum as tau sub 0 equals 1 tick, and Cost, which supplies the J-cost function J(x) equals (x plus x inverse over 2) minus 1. It works inside the Recognition Science setting that derives all physics from a single functional equation, here specialized to special relativity. The key local claim is that the Lorentz factor is always at least unity.

proof idea

This is a definition module, no proofs. The module simply collects and organizes the sibling declarations gamma_ge_one, jcost_cosh_is_gamma_minus_one, mass_energy_RS and the associated certificate objects.

why it matters in Recognition Science

The module supplies the special-relativity layer that feeds SpecialRelativityDeepCert and specialRelativityDeepCert_inhabited. It fills the relativistic kinematics slot in the T0-T8 forcing chain, using J-uniqueness and the eight-tick octave to constrain gamma.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)