HingeDatum
plain-language theorem explainer
A structure packages the edges incident to a hinge in an n-vertex simplicial complex together with nonnegative real weights that represent shared face areas in the continuum limit. It is invoked by modules computing cubic deficits and verifying equivalence between cubic and simplicial presentations of the Regge action. The definition consists of a record type whose sole constraint is nonnegativity of the weight assignment.
Claim. A hinge datum for an $n$-vertex graph consists of a list of incident edges (pairs from Fin $n$), a weight function from pairs to real numbers, and the assertion that all weights are nonnegative.
background
In the Recognition Science framework the J-cost Dirichlet energy on a scalar recognition potential defined on 3-simplices is identified with a linearized Regge action once a map from the potential to an edge-length field is supplied. The module closes that map and packages the linearization as a named hypothesis. The hinge datum records, for each hinge, the list of edges that meet there and the geometric weights (continuum face areas) attached to those edges.
proof idea
The declaration is a direct structure definition with three fields: the edge list, the weight function, and the nonnegativity axiom. No lemmas or tactics are invoked.
why it matters
This definition supplies the combinatorial skeleton for the cubic deficit discharge. It is referenced by the cubic area, cubic deficit, and hinge-list constructions, which together establish the master invariance certificate between cubic and simplicial ledger presentations. The construction therefore advances the field-curvature identity of the Gravity from Recognition draft (Theorem 5.1) by providing the hinge data needed to equate the J-cost energy with the Regge action under the stated linearization hypothesis. It leaves open the explicit discharge of that hypothesis via Cayley-Menger determinants or the Piran-Williams split.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.