cubicDeficit_singleton
plain-language theorem explainer
The cubic deficit functional returns the squared difference of recovered log-potentials when evaluated on a singleton hinge. Researchers discharging the Regge linearization hypothesis for the cubic lattice cite this evaluation when reducing the total deficit sum. The term proof rewrites via the singletonHinge_edges lemma to match the case clause inside the cubicDeficit definition.
Claim. For any natural number $n$, edge-length field $L$, indices $i,j$, and weight $w$ with $w$ nonnegative, the deficit at the hinge consisting of the single edge from $i$ to $j$ with weight $w$ equals the square of the difference between the recovered log-potentials at $i$ and $j$, where each recovered value is the logarithm of the normalized diagonal entry of $L$.
background
The module discharges the Regge deficit linearization hypothesis for the RS-canonical cubic lattice by constructing a deficit functional whose leading term is quadratic in the log-potential differences. The cubicDeficit definition returns $(recoverEps L i - recoverEps L j)^2$ precisely when the hinge datum contains exactly one edge, and zero otherwise. The recoverEps function extracts the conformal factor via the logarithm of the ratio of the diagonal length to the base spacing. The singletonHinge datum packages a single weighted edge for use in the hinge enumeration list. Upstream, PhiForcingDerived supplies the J-cost structure while LedgerFactorization calibrates the multiplicative group on positive reals; the module doc states that this quadratic truncation satisfies the field-curvature identity exactly, with higher-order remainders handled in later phases.
proof idea
The term-mode proof begins by showing that the left-hand side matches the match expression on the edges of the supplied hinge. It applies the lemma singletonHinge_edges to replace the hinge with its explicit edge list [(i,j)], after which the match collapses directly to the squared difference already written in the definition of cubicDeficit.
why it matters
This evaluation lemma is invoked inside singletonHinge_product to obtain the area-times-deficit identity that feeds the discrete Laplacian sum. It therefore closes the Phase A step of the four-phase program that promotes the paper's Theorem 5.1 from a pattern-matching argument to a Lean theorem. Within the Recognition framework the result confirms that the quadratic truncation of the Regge deficit reproduces the exact linearization identity on the cubic lattice, consistent with the T5 J-uniqueness and T6 self-similar fixed-point structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.