Jcost_near_identity
plain-language theorem explainer
Recognition Science derives the spatial metric coefficient from the J-cost quadratic near identity: for any ε with 1 + ε > 0, J(1 + ε) equals ε squared over 2(1 + ε). Researchers deriving Lorentzian geometry from cost functionals cite this identity to obtain the positive curvature of spatial directions. The proof reduces directly to the algebraic identity J(x) = (x - 1)² / (2x) by substitution and ring simplification.
Claim. For any real number $ε$ satisfying $-1 < ε$, the J-cost satisfies $J(1 + ε) = ε² / (2(1 + ε))$.
background
The J-cost is defined via the Recognition Composition Law as J(x) = (x + x⁻¹)/2 - 1, equivalently expressed as the squared ratio (x - 1)² / (2x) for x ≠ 0 by the upstream lemma Jcost_eq_sq. This module derives 4D Lorentzian spacetime as a theorem of cost minimization under the forcing chain T0–T8, with spatial directions carrying positive metric coefficient from J''(1) = 1 and temporal direction carrying negative sign from the 8-tick operator. The module documentation states: 'The complete structure of 4D Lorentzian spacetime — metric signature (−,+,+,+), causal light-cone, Lorentz factor, arrow of time — is FORCED by the J-cost functional and the forcing chain T0–T8.'
proof idea
The proof is a term-mode reduction: first establish 1 + ε ≠ 0 via linarith, then rewrite with the lemma Jcost_eq_sq and finish by congr 1 followed by ring to match the target quadratic.
why it matters
This identity is invoked by the downstream theorem spatial_cost_positive to establish that spatial cost is strictly positive for nonzero displacement, which supports the positive definite spatial metric in the forced Lorentzian signature η = diag(−1, +1, +1, +1). It supplies the local quadratic step in the derivation chain RCL → J unique (T5) → J''(1) = 1 (spatial curvature) + φ forced (T6) → 8-tick (T7) + D = 3 (T8) → c = 1. It touches the open question of how cost minimization selects the temporal arrow.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.