singletonHinge
singletonHinge constructs a HingeDatum containing exactly one ordered edge (i, j) with assigned nonnegative weight w. Downstream code in the cubic deficit module invokes it to populate the full hinge list for the lattice and to evaluate per-hinge area and deficit products. The definition is a direct record constructor whose only nontrivial clause is the weight_nonneg predicate, discharged by a two-case split on edge equality.
claimLet $n$ be a natural number, $i,j$ indices in the finite set of size $n$, and $w$ a real number with $w$ nonnegative. The singleton hinge datum is the structure whose edge list is the singleton pair $(i,j)$, whose weight function returns $w$ on that pair and zero elsewhere, and whose weight function satisfies nonnegativity by construction.
background
HingeDatum packages the edges incident to a hinge together with their geometric weights, which in the continuum limit represent shared face areas. The module builds a deficit-angle functional that realizes the leading-order Regge linearization on the cubic lattice: deficit at each hinge equals the squared difference of log-potentials, while area is proportional to ledger weight. This supplies the exact linearization identity needed for the field-curvature identity of the draft paper's Theorem 5.1.
proof idea
The definition is a record literal that directly supplies the three fields of HingeDatum. The weight_nonneg field is proved by introducing an arbitrary edge e and splitting on whether e equals the target pair; the two branches simplify immediately to the hypothesis or to zero.
why it matters in Recognition Science
This definition supplies the atomic building block for cubicHinges, which enumerates one singleton hinge per ordered pair, and thereby for regge_sum_cubicHinges and the linearization discharge. It therefore participates in the reduction of the Regge sum to a weighted sum of squared potential differences, which is the exact content of the leading-order identity needed for Phase A of the four-phase program. The construction is used in the cubic lattice presentation that realizes the eight-tick octave and three-dimensional spatial structure.
scope and limits
- Does not require i and j to be adjacent in any underlying graph.
- Does not compute deficit or area values; those are separate functions.
- Does not impose any relation between w and edge lengths.
- Does not handle multiple edges or higher-valence hinges.
formal statement (Lean)
92def singletonHinge {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
93 HingeDatum n :=
proof body
Definition body.
94 { edges := [(i, j)]
95 , weight := fun e => if e = (i, j) then w else 0
96 , weight_nonneg := by
97 intro e
98 by_cases h : e = (i, j)
99 · simp [h, hw]
100 · simp [h]
101 }
102