field_curvature_identity_cubic
plain-language theorem explainer
The cubic field-curvature identity equates the discrete Laplacian action on a log-potential field to a scaled Regge sum of cubic deficit functionals over the hinges of any weighted ledger graph. Discrete gravity researchers deriving continuum limits in Recognition Science cite it to justify the exact linearization step before higher-order corrections. The proof is a one-line wrapper that invokes the general under-linearization theorem after substituting the cubic-specific discharge.
Claim. For any natural number $n$, real $a > 0$, weighted ledger graph $G$ on $n$ vertices, and log-potential field $ε$, the Laplacian action satisfies laplacian_action$(G, ε) = (1/(8φ^5)) · regge_sum(cubicDeficitFunctional $n$, conformal_edge_length_field$(a, ε)$, cubicHinges $G)$, where the sum runs over all ordered vertex pairs with quadratic deficit truncation and area weights from $G$.
background
The module CubicDeficitDischarge discharges the ReggeDeficitLinearizationHypothesis unconditionally for the RS-canonical cubic lattice. A WeightedLedgerGraph is a symmetric nonnegative weight matrix on Fin n. laplacian_action is the quadratic form (1/2) ∑∑ w_ij (ε_i − ε_j)^2. jcost_to_regge_factor equals 8 φ^5, the constant matching J''(1) = 1 to the Regge normalization 1/κ. cubicDeficitFunctional implements the leading-order truncation: deficit at each hinge is (ε_i − ε_j)^2 and area is (κ/2) · weight(i,j).
proof idea
The proof is a one-line wrapper that applies field_curvature_identity_under_linearization to cubicDeficitFunctional, a, ha, cubicHinges G, G, the discharge cubic_linearization_discharge a ha G, and ε. This substitutes the exact cubic linearization hypothesis into the general identity relating Laplacian action to the normalized Regge sum.
why it matters
This theorem completes Phase A of the program to promote the draft paper's Theorem 5.1 (field-curvature identity) to a Lean theorem. It is invoked directly by field_curvature_identity_einstein to obtain the Einstein-coupling form with κ_Einstein = 8 φ^5 and by cubicFieldCurvatureCert to package the discharge and identity. In the Recognition framework it supplies the exact linearization step for the cubic lattice before the O(ε^3) remainder analysis in ContinuumTheorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.