singletonHinge_weight
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply to multi-edge hinges or general weighted graphs.
- Does not incorporate O(|ε|³) corrections to the Regge deficit.
- Does not prove nonnegativity or other global properties of cubicDeficitFunctional.
- Does not address the continuum limit or Berry creation thresholds.
formal statement (Lean)
103theorem singletonHinge_weight {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
104 (singletonHinge i j w hw).weight (i, j) = w := by
proof body
One-line wrapper that applies unfold.
105 unfold singletonHinge; simp
106