HingeTrivial
plain-language theorem explainer
HingeTrivial defines a hinge datum as trivial when its deficit angle vanishes under a given deficit functional and conformal edge-length field. Workers on cubic-simplicial equivalence in Recognition Science cite it to drop internal diagonals from Regge sums after Freudenthal triangulation. The definition is a direct predicate that sets the property equal to the vanishing of the deficit map.
Claim. A hinge datum $h$ is trivial relative to a deficit-angle functional $D$ and edge-length field $L$ when $D$.deficit$(L,h)=0$.
background
This definition appears in the module that establishes structural invariance between cubic and simplicial presentations of the Recognition ledger, addressing Beltracchi §5. The module shows that the standard triangulation of a 3-cube into six tetrahedra adds only internal hinges whose deficits vanish on conformal fields, so the Regge action is unchanged. DeficitAngleFunctional is the structure supplying a deficit map from EdgeLengthField to HingeDatum together with a nonnegative area map. EdgeLengthField records conformal lengths derived from vertex log-potentials. HingeDatum packages the list of incident edges and their geometric weights. Upstream, deficit is realized as $2π - ∑θ$ in both the DihedralAngle and Schlaefli modules.
proof idea
The declaration is a definition that directly sets the predicate to the equality D.deficit L h = 0. No lemmas are invoked; the body is the literal statement of the property.
why it matters
HingeTrivial supplies the predicate used in SimplicialRefinement to certify that extra internal hinges carry zero deficit and in regge_sum_append_trivial to prove that appending such hinges leaves the Regge sum invariant. These results feed the master certificate CubicSimplicialInvarianceCert, which establishes that cubic and simplicial ledger data produce identical J-cost to Regge identifications. The definition therefore closes the refinement-invariance step required for the T0-T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.