coupling_quadratic
plain-language theorem explainer
The declaration defines the quadratic coupling cost between neighboring simplices in log-coordinates as (ε₁ - ε₂)² / 2. Continuum-limit researchers bridging discrete recognition ledgers to general relativity would cite it as the explicit discrete Laplacian term. It is supplied by direct definition that matches the second-order Taylor expansion of the J-cost functional.
Claim. Let ε₁, ε₂ ∈ ℝ be the logarithmic coordinates of two neighboring simplices. The quadratic coupling cost is given by (ε₁ - ε₂)² / 2.
background
The Continuum Bridge module establishes that the J-cost functional on the simplicial ledger coincides with the Regge action (up to κ = 8φ⁵ normalization) and that its stationarity yields the Einstein field equations in the continuum limit. The central expansion is J(e^ε) = cosh(ε) - 1 = ε²/2 + O(ε⁴), so the inter-simplex coupling J(ψ₁/ψ₂) reduces exactly to the quadratic form above. Upstream cost definitions from ObserverForcing and MultiplicativeRecognizerL4 establish that every recognition event carries non-negative J-cost; the IntegrationGap.A and CrystalStructure.Structure supply the discrete counting and lattice background.
proof idea
Direct definition that implements the quadratic approximation of the J-cost coupling term.
why it matters
This supplies the discrete Laplacian identification that lets J-cost stationarity be equated with Regge-equation stationarity, closing the step from SimplicialLedger.J_global to the continuum limit in the module derivation chain. It instantiates the quadratic structure required for the T5 J-uniqueness and T8 D = 3 landmarks to produce the Einstein equations without additional curvature hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.