as
plain-language theorem explainer
The declaration defines the structure that equates the discrete Laplacian action built from J-cost differences on neighboring simplices to the Regge action summed over hinges. A researcher deriving Einstein equations from a discrete ledger would cite it to justify replacing the continuum curvature term with the quadratic J-form. The definition proceeds by direct structural matching of the two quadratic expressions after the log-coordinate expansion of J.
Claim. The structure identifies the weighted Laplacian action on log-coordinates, $½ ∑_{i∼j} w_{ij} (ε_i − ε_j)²$, with the normalized Regge action, $(1/κ) ∑_h δ_h A_h$, where the edge weights are $w_{ij} = A_{ij}/(κ · vol_i)$, ε = ln ψ, δ_h is the deficit angle at hinge h, and A_h its area.
background
The module establishes that the J-cost functional on the simplicial ledger coincides with the Regge action up to the normalization κ = 8φ⁵. In log coordinates the quadratic part of J(e^ε) = cosh(ε) − 1 supplies the squared differences (ε_i − ε_j)² that define the discrete Laplacian. The upstream result EdgeLengthFromPsi.is supplies the algebraic identification of edge lengths with the field values ψ, while J_global from SimplicialLedger supplies the global cost whose stationarity is under study.
proof idea
The declaration is a structure definition that encodes the equality of the two quadratic forms. It assembles the weights w_ij from the shared-face areas and simplex volumes already present in the ledger, then states the numerical identity between the summed squared differences and the summed deficit-angle contributions without further computation.
why it matters
It supplies the explicit bridge from J-cost stationarity on the ledger to the Regge equations, which in turn converge to the Einstein field equations. Downstream uses appear in the Euler–Lagrange and Noether sections of the Action module, where the same quadratic form reappears as the Hessian metric. The construction realizes the derivation chain listed in the module header: J_global → log expansion → discrete Laplacian → Regge identification → κ normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.