HingeDataN
plain-language theorem explainer
Abstract hinge datum for an n-simplex: a single nonnegative real, the (n-2)-volume of a codimension-two face. Cited by the finite-index Schläfli data bundle and by flat 4-simplex Regge constructions. Pure structure definition: a measure field plus a nonnegativity proof obligation.
Claim. A hinge datum is a pair $(m, h)$ with $m \in \mathbb{R}$ and $h : 0 \leq m$. The real $m$ is the $(n-2)$-dimensional volume of a codimension-two face (hinge) of an $n$-simplex.
background
The module gives a dimension-parametric Schläfli interface in finite-index form, so that the classical 3D tetrahedral identity can later instantiate the same shape at $n=3$. In discrete geometry and Regge calculus, a hinge is a codimension-two face; dihedral angles live on hinges, and edge-length variations couple to those angles through the Schläfli relation.
Here a hinge is reduced to its measure alone: a real $(n-2)$-volume together with a proof that the measure is nonnegative. No combinatorial incidence or embedding data is stored at this layer. Downstream bundles attach finitely many such hinges and a matrix of partials $\partial\theta_h/\partial L_e$.
The classical Schläfli identity then reads, for each edge coordinate $e$, $\sum_h V_{n-2}(h),\partial\theta_h/\partial L_e = 0$. This structure supplies the $V_{n-2}(h)$ factors in that sum.
proof idea
No proof body: this is a structure declaration. Two fields are declared, a real measure and a Prop field measure_nonneg asserting $0 \leq$ measure. Inhabitants are built by supplying a concrete volume and a nonnegativity certificate (as in the flat 4-simplex hinge constructor, which takes a positive hinge area and applies le_of_lt).
why it matters
This is the atomic hinge type for the n-dimensional Schläfli interface. SchlaefliDataN packages a finite family of hinges of this type with a Jacobian of dihedral angles versus edge lengths, and states the identity $\sum_h V_{n-2}(h),\partial\theta_h/\partial L_e = 0$.
On the gravity side, flatHingeData builds instances from flat Freudenthal 4-simplex hinge areas, feeding the pathwise flat Schläfli vanishing theorems used in Regge 4D analysis. The definition therefore sits between pure discrete geometry and the discrete-gravity Schläfli path that supports curvature bookkeeping in the Recognition framework.
It does not itself force $D=3$ or the eight-tick octave; those enter only when the interface is specialized and tied to the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.