singletonHinge_weight
plain-language theorem explainer
singletonHinge_weight asserts that the weight function of the hinge datum built from indices i, j and nonnegative w returns exactly w at the edge (i, j). Workers discharging the Regge deficit linearization for the cubic lattice cite this to confirm area scaling before invoking the field-curvature identity. The proof is a one-line wrapper that unfolds the singletonHinge definition and simplifies the weight case.
Claim. Let $H$ be the hinge datum with single edge $(i,j)$ and weight $w$ where $w$ is nonnegative. Then the weight map of $H$ satisfies $H(i,j) = w$.
background
The CubicDeficitDischarge module discharges the ReggeDeficitLinearizationHypothesis for the RS-canonical cubic lattice as Phase A toward a Lean proof of the paper's Theorem 5.1 on the field-curvature identity. A hinge datum is built by singletonHinge, which produces a structure whose edges list contains only the ordered pair (i, j) and whose weight function returns the supplied w on that pair and zero on all others.
proof idea
The proof is a one-line wrapper that unfolds singletonHinge and applies simp to match the weight function case directly.
why it matters
This theorem supports cubicArea_singleton, which returns jcost_to_regge_factor times w over 2 for the area on a singleton hinge. It completes the Phase A step that discharges the linearization hypothesis exactly for the quadratic-in-ε truncation on the cubic lattice, allowing field_curvature_identity_under_linearization to be invoked. Higher-order O(|ε|³) remainders are deferred to Phase D and tracked via J_log_quadratic_approx.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.