cubicDeficitFunctional
plain-language theorem explainer
The cubic deficit functional packages the quadratic deficit map and proportional area map for singleton hinges on an n-vertex weighted ledger graph. It is cited by every proof that discharges the Regge linearization hypothesis on the cubic lattice and then invokes the field-curvature identity. The declaration is a direct record construction that supplies the two maps together with the nonnegativity witness required by the DeficitAngleFunctional structure.
Claim. Let $n$ be a natural number. The cubic deficit functional is the deficit-angle functional structure whose deficit component returns the squared difference of recovered log-potentials on the two vertices of a singleton hinge (and zero otherwise), whose area component returns half the Regge factor times the hinge weight on a singleton hinge (and zero otherwise), and whose area-positivity component is the theorem that this area map is nonnegative.
background
A DeficitAngleFunctional consists of a deficit map, an area map, and a proof that the area map is nonnegative for every edge-length field and hinge datum. The cubic specialization sets the deficit to the square of the difference of recovered log-potentials on the endpoints of a singleton hinge and the area to half the product of the Regge factor with the hinge weight. This matches the leading-order quadratic truncation of the Regge deficit for conformal edge-length fields on the cubic lattice.
proof idea
The declaration is a one-line wrapper that constructs the DeficitAngleFunctional record by assigning cubicDeficit to the deficit field, cubicArea to the area field, and cubicArea_nonneg to the area_pos field.
why it matters
This definition supplies the concrete functional discharged by cubic_linearization_discharge, which is invoked by bridge_chain_complete and by the ContinuumFieldCurvatureCert structure. It realizes the exact quadratic truncation needed for the identity between Laplacian action and Regge sum at leading order, closing Phase A of the program that promotes the paper's Theorem 5.1 to a Lean theorem. The construction is the cubic-lattice instance of the linearization hypothesis required by field_curvature_identity_einstein.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.