CubicFieldCurvatureCert
plain-language theorem explainer
This structure certifies that the Regge deficit linearization hypothesis holds exactly for the cubic deficit functional on any weighted ledger graph. It packages the resulting field-curvature identity equating Laplacian action to a scaled Regge sum together with the normalization factor fixed at 8 phi to the fifth. Researchers extending discrete gravity models within Recognition Science would cite it to confirm the leading-order equivalence between J-cost actions and Regge curvature on cubic lattices. The definition assembles the cubic-specific
Claim. A certificate structure asserting that for every natural number $n$, positive real $a$, and weighted ledger graph $G$, the Regge deficit linearization hypothesis holds for the cubic deficit functional at scale $a$ on the hinges of $G$. It further asserts that the Laplacian action of $G$ on any log-potential equals one over $kappa$ times the Regge sum of the cubic deficit functional applied to the conformal edge length field, where $kappa = 8 phi^5 > 0$.
background
The module discharges the Regge deficit linearization hypothesis unconditionally for the RS-canonical cubic lattice presentation. It constructs a deficit-angle functional implementing the leading-order Regge linearization in which the deficit at each hinge equals the squared log-potential difference while the area is proportional to the graph weight. The normalization factor relating J-cost action to Regge action is defined as $kappa = 8 phi^5$, chosen because the second derivative of the J-cost at unity equals one and the Regge action carries the conventional factor $1/(8 pi G)$ (from upstream: jcost_to_regge_factor doc-comment).
proof idea
The structure definition directly populates its four fields. The discharge field receives the output of the cubic linearization discharge lemma. The identity field is obtained by instantiating the general field curvature identity under linearization with the cubic deficit functional and the cubic discharge. The kappa value and positivity fields are taken from the explicit definition of the J-cost to Regge factor as eight times phi to the fifth together with its immediate positivity.
why it matters
This certificate supplies the missing discharge needed to promote the paper's Theorem 5.1 (field-curvature identity) from a pattern-matching argument to a Lean theorem for the cubic case. It is the explicit output of Phase A in the four-phase program described in the module documentation. The normalization $kappa = 8 phi^5$ links the construction to the J-uniqueness property and the self-similar fixed point of the Recognition framework. Higher-order corrections remain for Phase D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.