coupling_cost
coupling_cost defines the interaction cost between neighboring simplices as J(exp(ε₁ - ε₂)) in log-potential coordinates. Discrete gravity researchers would cite it when matching the simplicial J-cost functional to the Regge action. The definition performs a direct substitution of the exponential map into the base Jcost function.
claimFor log-potentials $ε_1, ε_2 ∈ ℝ$, the coupling cost between simplices is $J(e^{ε_1 - ε_2})$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The module derives the continuum limit by showing that J-cost stationarity on the simplicial ledger reproduces the Regge action and hence the Einstein field equations. In log coordinates ε = ln ψ the expansion J(e^ε) = ε²/2 + O(ε⁴) supplies the quadratic structure that matches the deficit-angle term in Regge calculus. Jcost itself is the base cost imported from the Cost module and characterized in PhiForcingDerived.of and MultiplicativeRecognizerL4.cost as the non-negative function induced by multiplicative recognition on positive ratios.
proof idea
The definition is a one-line wrapper that applies Jcost directly to Real.exp(ε₁ - ε₂).
why it matters in Recognition Science
This definition supplies the explicit coupling term that lets the module identify J-cost minimization with Regge action minimization. It sits inside the derivation chain SimplicialLedger.J_global → log-coordinate expansion → discrete Laplacian → Regge identification → κ = 8φ⁵ normalization → continuum limit to the Einstein equations. The quadratic leading term aligns with the T5 J-uniqueness and T7 eight-tick octave landmarks of the Recognition Science forcing chain.
scope and limits
- Does not evaluate the cost for concrete numerical potentials.
- Does not derive the quadratic approximation; that follows from the Taylor series of J.
- Does not address convergence of the discrete equations to the continuum EFE.
- Does not incorporate the normalization factor κ = 8φ⁵.
formal statement (Lean)
83def coupling_cost (ε₁ ε₂ : ℝ) : ℝ := Jcost (Real.exp (ε₁ - ε₂))
proof body
Definition body.
84
85/-- The quadratic approximation of the coupling cost. -/