deficit_jcost_correspondence
plain-language theorem explainer
The theorem identifies the leading-order J-cost mismatch on the simplicial ledger with half the square of the deficit angle for small angles. Researchers deriving discrete-to-continuum limits in recognition-based gravity would cite it to justify the quadratic curvature term. The proof is a direct one-line unfolding of the quadratic definition followed by algebraic simplification.
Claim. For a deficit angle $δϵ$ satisfying $|δϵ| < 1$, the quadratic approximation of the J-cost functional satisfies $J_{log}(δϵ) - (δϵ)^2 / 2 = 0$.
background
The Continuum Bridge module shows that J-cost stationarity on the simplicial ledger yields the Regge action and, in the continuum limit, the Einstein field equations. The quadratic approximation is defined by J_log_quadratic(ε) := ε²/2, which is the leading Taylor term of cosh(ε) − 1. Upstream results define the cost of a recognition event as its J-cost (ObserverForcing.cost) and the cost induced by a multiplicative recognizer as the derived cost of its comparator (MultiplicativeRecognizerL4.cost). The module doc states that in log coordinates the coupling term J(ψ₁/ψ₂) expands exactly as (ε₁ − ε₂)²/2 plus higher orders, producing a discrete Laplacian.
proof idea
The proof is a one-line term proof. It unfolds the definition of J_log_quadratic (which is literally ε²/2) and applies the ring tactic to obtain the algebraic identity.
why it matters
This step supplies the leading-order identification required by the module's derivation chain: SimplicialLedger.J_global → log-coordinate expansion → discrete Laplacian → Regge action → κ = 8φ⁵ normalization → continuum EFE. It confirms that the quadratic structure of J-cost (T5 J-uniqueness and the Recognition Composition Law) directly produces the deficit-angle term of the Regge action. The declaration touches the open question of full nonlinear convergence handled in the downstream NonlinearConvergence module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.