spatial_cost_positive
plain-language theorem explainer
The J-cost is strictly positive for any nonzero real displacement ε satisfying -1 < ε. Researchers deriving Lorentzian geometry from cost minimization cite this to confirm spatial directions are cost-increasing. The argument rewrites the target via the near-identity expansion of Jcost and verifies the resulting quadratic-over-linear expression is positive by direct application of square positivity and denominator bounds.
Claim. For every real number $ε$ with $-1 < ε ≠ 0$, the J-cost satisfies $0 < Jcost(1 + ε)$, where Jcost is the cost functional minimized at the identity event.
background
The Spacetime Emergence module shows that 4D Lorentzian geometry, including metric signature (−,+,+,+), follows from the J-cost functional together with the T0–T8 forcing chain. The identity event is defined as the RecognitionEvent with state 1, the unique minimum of J-cost. Jcost_near_identity supplies the local expansion used here, reducing the claim to an algebraic expression whose positivity is immediate once ε > −1 keeps the denominator positive.
proof idea
One-line wrapper that applies the near-identity lemma Jcost_near_identity to obtain an explicit rational form, then invokes div_pos on the square of ε (strictly positive by hε_ne) over a positive denominator (2 times a term positive by linarith from hε).
why it matters
The result supplies the local positivity needed for the spatial metric coefficient in the emergence of η = diag(−1,+1,+1,+1). It supports the module's central claim that spatial curvature is positive definite (J''(1)=1) while the 8-tick operator supplies the opposite sign in the temporal direction, completing one step in the derivation of D=3 from T8 with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.