cubicFieldCurvatureCert
plain-language theorem explainer
The cubic lattice satisfies the Regge deficit linearization hypothesis exactly for its leading-order quadratic deficit functional. This lets the field-curvature identity hold without approximation on any weighted ledger graph. Workers on discrete gravity models and Recognition Science curvature derivations cite the result. The proof is a term-mode assembly of the certificate structure that applies the general discharge lemma and the cubic identity theorem.
Claim. For any $a > 0$ and weighted ledger graph $G$ on $n$ vertices, the cubic deficit functional (deficit at each hinge given by squared log-potential difference, area scaled by the Regge factor) satisfies the Regge deficit linearization hypothesis. Consequently the Laplacian action on a log-potential equals $(1/κ)$ times the Regge sum of that functional over conformal edge lengths, where $κ = 8φ^5$.
background
The module discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice. It constructs a deficit-angle functional whose value at a hinge is the squared difference of log-potentials and whose area weight is $(κ/2)$ times the ledger edge weight. The hinges are the ordered vertex pairs of the graph. The SimplicialLedger structure supplies the underlying 3-simplex collection whose manifold-covering property is assumed. Upstream, jcost_to_regge_factor_eq states that $κ = 8φ^5$ is the unique normalization matching J-cost to Regge curvature, while jcost_to_regge_factor_pos records its positivity.
proof idea
The proof is a term-mode construction of the CubicFieldCurvatureCert structure. The discharge field is supplied by applying cubic_linearization_discharge to the cubic functional and hinge list. The identity field is supplied by field_curvature_identity_cubic. The kappa_value and kappa_pos fields are filled directly by jcost_to_regge_factor_eq and jcost_to_regge_factor_pos.
why it matters
This declaration completes Phase A of the four-phase program that promotes the draft paper's Theorem 5.1 (field-curvature identity) to a genuine Lean theorem. It shows the linearization identity holds exactly for the cubic lattice, supplying the discharge needed for field_curvature_identity_cubic. The result relies on the J-cost to Regge normalization $κ = 8φ^5$ and sits inside the Recognition Science forcing chain that fixes spatial dimension $D=3$ and the eight-tick octave. It leaves higher-order $O(|ε|^3)$ corrections to Phase D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.