coupling_cost
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.