Hinge
Hinge equips a simplicial ledger with a real-valued deficit angle at codimension-2 edges, formalizing curvature concentration in a piecewise-flat 3-manifold. Workers on Regge calculus discretizations or simplicial gravity cite it when separating flat interiors from hinge deficits. The declaration is a one-field structure definition.
claimFor a simplicial ledger $L$, a hinge is a codimension-2 substructure equipped with a deficit angle $deltainmathbb{R}$.
background
The module addresses Beltracchi §7 by making explicit that each 3-simplex carries a flat Euclidean or Minkowski interior metric, so curvature is confined to codimension-2 hinges (edges in 3D). A simplicial ledger is a collection of 3-simplices forming a non-empty manifold covering. Upstream results supply the ledger structure and related factorization and forcing objects used to calibrate the deficit.
proof idea
The declaration is a structure definition that introduces the hinge with its single deficit field.
why it matters in Recognition Science
This definition supports the cubic deficit functional and the conformal edge length theorem in the flat vacuum. It realizes the Regge axiom that curvature support lies only on codimension-2 loci, consistent with D=3 in the unified forcing chain. It closes part of the scaffolding for interior holonomy triviality.
scope and limits
- Does not locate the hinge inside a specific simplex or edge.
- Does not impose positivity or bounds on the deficit value.
- Does not connect the deficit to the phi-ladder or J-cost.
- Does not prove flatness of the interior metric.
formal statement (Lean)
163structure Hinge (_L : SimplicialLedger.SimplicialLedger) where
164 deficit : ℝ
165
166/-- A *codimension-0 or codimension-1* stratum of the ledger: the
167 3-simplex interior or a 2-face shared between two simplices.
168 Neither carries curvature by the flat-interior axiom. -/