pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.SpecialRelativityDeep

show as:
view Lean formalization →

The SpecialRelativityDeep module establishes that the Lorentz factor γ is always at least one and connects the J-cost to γ minus one. Physicists deriving relativistic effects from the Recognition Science functional equation would reference these results. The module builds its claims through direct applications of the imported constants and cost structures, with each sibling declaration handling a specific identity or inequality.

claimIn RS-native units the Lorentz factor satisfies $γ ≥ 1$. The J-cost satisfies $J(γ) = γ - 1$ via the identity $J(x) = (x + x^{-1})/2 - 1$.

background

Recognition Science derives special relativity from the J-cost function defined on the forcing chain. The Constants module supplies the base time quantum τ₀ = 1 tick. The Cost module defines the J-cost via the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This module applies these to show relativistic kinematics emerge naturally, with γ tied to velocity through the self-similar fixed point.

proof idea

The module consists of discrete theorems rather than a unified proof. gamma_ge_one applies basic properties of the square root and velocity bounds to show γ ≥ 1. jcost_cosh_is_gamma_minus_one uses the definition of J and the hyperbolic identity to equate the cost to γ - 1. mass_energy_RS follows by combining these with energy definitions from upstream results.

why it matters in Recognition Science

These results anchor the special relativity sector of the framework and support downstream mass-energy relations such as mass_energy_RS. They realize the T5 J-uniqueness and T6 phi fixed point in the relativistic context. The module closes part of the path from the functional equation to observable physics without introducing new hypotheses.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)