cubicDeficit
plain-language theorem explainer
cubicDeficit supplies the deficit component of the leading-order Regge functional on cubic lattices by returning the squared difference of recovered log-potentials at singleton hinges. Researchers discharging the linearization hypothesis for Recognition Science discrete gravity cite it to obtain an exact identity between the weighted deficit sum and the Laplacian action. The implementation is a direct pattern match on the hinge datum edges list that yields zero for all non-singleton cases.
Claim. Let an edge length field on $n$ vertices with base spacing $a$ and a hinge datum $h$ be given. The cubic deficit equals $(ε_i - ε_j)^2$ when the edges of $h$ form exactly the singleton list $[(i,j)]$, and equals $0$ otherwise, where $ε_k := log(L_{kk}/a)$.
background
The module discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice presentation. It constructs a deficit-angle functional whose deficit map is given by cubicDeficit and whose area map is given by cubicArea. The upstream recoverEps definition recovers the log-potential via Recover ε i from a conformal edge-length field via the self-loop L_{ii} = a · exp(ε_i). The EdgeLengthField encodes the conformal ansatz $L_{ij} = a exp((ε_i + ε_j)/2)$. HingeDatum packages the incident edges and their weights for each hinge. This supplies the quadratic truncation of the J-cost that appears in the leading-order expansion of the piecewise-flat Regge deficit.
proof idea
The definition proceeds by pattern matching on the edges component of the supplied hinge datum. When the list is exactly the singleton [(i,j)], it evaluates to the square of the difference between recoverEps applied to i and to j; every other case returns zero.
why it matters
cubicDeficit is the deficit map inside cubicDeficitFunctional, which is used by regge_sum_cubicHinges to prove that the Regge sum equals a constant times the sum of weighted squared potential differences. This completes Phase A of the four-phase program that promotes the paper's Theorem 5.1 (field-curvature identity) to a genuine Lean theorem. It realizes the quadratic-in-ε truncation of the J-cost whose higher-order remainder is tracked in Phase D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.