cubicHinges
plain-language theorem explainer
cubicHinges builds the exhaustive list of singleton hinge data for any weighted ledger graph on n vertices by enumerating every ordered pair and attaching the corresponding edge weight. Authors of the continuum bridge chain and field-curvature certificate invoke this list when summing Regge deficits over the complete hinge set. The definition is a direct enumeration that applies the singleton hinge constructor once per pair.
Claim. Let $G$ be a weighted ledger graph on a vertex set of cardinality $n$. The hinge list is the ordered collection of all singleton hinge data, one for each ordered pair of vertices $(i,j)$, each carrying the edge weight $w_{ij}$ supplied by $G$.
background
A weighted ledger graph encodes a finite set of vertices together with a symmetric non-negative weight function on ordered pairs, serving as the discrete substrate for the cubic lattice in Recognition Science. HingeDatum packages the minimal data for one Regge hinge: the two endpoint indices, the edge weight, and a proof that the weight is non-negative. The singleton hinge constructor assembles one such datum from an ordered pair and its weight.
proof idea
The definition ranges over the finite set of all ordered pairs via the complete Finset on $n$ and maps each pair to a singleton hinge datum using the graph weight function together with its non-negativity certificate.
why it matters
This enumeration supplies the hinge list required by the regge sum in the cubic linearization discharge theorem. It is invoked by the complete bridge chain theorem, the continuum field curvature certificate, and the Einstein-coupling form of the field-curvature identity. The construction closes Phase A of the program that lifts the draft paper's Theorem 5.1 from pattern matching to an exact Lean statement, consistent with the J-cost quadratic truncation and the forcing chain steps that fix three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.