J_log_quadratic
plain-language theorem explainer
J_log_quadratic defines the leading quadratic term ε²/2 in the log-coordinate expansion of the J-cost functional. Researchers deriving the discrete-to-continuum limit from simplicial ledgers to the Einstein equations cite it when matching the action to the Regge form. The definition is a direct algebraic abbreviation implementing the Taylor expansion of cosh(ε) - 1 at order two.
Claim. Define the quadratic approximation to the J-cost in logarithmic coordinates by $J_ {log} (ε) := ε²/2$.
background
The module derives the continuum bridge by showing that J-cost stationarity on the simplicial ledger reproduces the Regge action and converges to the Einstein field equations. In log coordinates ε = ln ψ the functional satisfies J(e^ε) = cosh(ε) - 1, whose Taylor series begins ε²/2 + O(ε⁴). The quadratic piece therefore supplies the discrete Laplacian structure whose stationarity yields the Regge equations.
proof idea
This is a direct definition. It encodes the order-two term of the cosh expansion without lemmas or tactics.
why it matters
The definition is invoked inside the JCostToEFE structure and the deficit_jcost_correspondence theorem to equate J-cost mismatch with (deficit angle)²/2 at leading order. It completes the quadratic step in the module derivation chain that runs from SimplicialLedger.J_global through the discrete Laplacian identification to the continuum limit with coupling κ = 8φ⁵. The placement supports the claim that the field-curvature identity follows from the quadratic structure of J-cost rather than an extra hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.