Jcost_near_identity
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not provide the J-cost expression when 1 + ε ≤ 0.
- Does not derive global or higher-order properties of the spacetime metric.
- Does not address the sign or reduction of cost along the temporal direction.
- Does not compute curvature or dynamics beyond the local quadratic form.
Lean usage
rw [Jcost_near_identity ε hε]formal statement (Lean)
81theorem Jcost_near_identity (ε : ℝ) (hε : -1 < ε) :
82 Jcost (1 + ε) = ε ^ 2 / (2 * (1 + ε)) := by
proof body
Term-mode proof.
83 have h_ne : (1 + ε : ℝ) ≠ 0 := ne_of_gt (by linarith)
84 rw [Jcost_eq_sq h_ne]; congr 1 <;> ring
85
86/-- The spatial cost is strictly positive for any non-zero displacement. -/