coupling_quadratic
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.
claimLet ε₁, ε₂ ∈ ℝ 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 in Recognition Science
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.
scope and limits
- Does not retain the O(ε⁴) remainder terms of the J-cost expansion.
- Does not define the adjacency weights w_ij or perform the full sum over the complex.
- Does not include the overall normalization factor κ = 8φ⁵.
- Does not prove convergence of the discrete equations to the Einstein field equations.
formal statement (Lean)
86def coupling_quadratic (ε₁ ε₂ : ℝ) : ℝ := (ε₁ - ε₂) ^ 2 / 2
proof body
Definition body.
87
88/-! ## Discrete Laplacian Structure
89
90The quadratic J-cost coupling is a discrete Laplacian action.
91On a simplicial complex with N simplices and adjacency weights w_ij:
92
93 S_quadratic = (1/2) Σ_{i~j} w_ij · (ε_i − ε_j)²
94
95This is the standard graph Laplacian energy. -/
96
97/-- A weighted simplicial graph representing the ledger. -/