ReggeData
plain-language theorem explainer
Abstract carrier for a Regge triangulation: vertices, bones, deficit angles, bone areas, and vertex-area gradients in 4D Euclidean coordinates, with the non-incidence convention that gradients vanish off the star. Anyone stating the Schläfli identity or contracted discrete Bianchi cites this type. It is a pure structure definition (no proof body).
Claim. An abstract Regge datum over index types $V$ (vertices) and $B$ (bones) consists of: vertex positions $x:V\to\mathbb{R}^4$; an incidence relation $b\sim v$; deficit angles $\varepsilon_b\in\mathbb{R}$; bone areas $A_b\in\mathbb{R}$; and vertex-area gradients $\partial A_b/\partial x_v\in\mathbb{R}^4$, required to vanish whenever $v$ is not incident to $b$.
background
Track 1.C of the quantum-gravity master plan asks for the contracted discrete Bianchi identity on a Regge substrate: the discrete analog of $\nabla_\mu G^{\mu\nu}=0$. In Regge calculus that identity is kinematic and coincides with the Schläfli identity at each interior vertex,
$$\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0.$$
The module therefore needs a minimal abstract package of triangulation data before it can name either property. Bones are the codimension-2 hinges (triangles in 4D) carrying deficit angle (holonomy of parallel transport around the bone) and area. Vertex positions live in Euclidean $\mathbb{R}^4$ for the structural form; Lorentzian content is deferred to the Track 1.B continuum side. The only structural law baked into the package is the non-incidence convention: if $v$ is not on bone $b$, the area gradient at that pair is the zero 4-vector.
proof idea
No proof: this is a structure declaration. The six fields are data plus one Prop field enforcing the non-incidence convention on the area gradient. Downstream definitions (Schläfli at a vertex, contracted discrete Bianchi) quantify over an inhabitant of this type; the flat witness sets all deficits and gradients to zero and satisfies the convention trivially.
why it matters
This is the substrate type for the entire DiscreteBianchi module. Every named property in Track 1.C is predicated on it: Schläfli identity at a vertex is the componentwise vanishing of $\sum_b\varepsilon_b,\partial A_b/\partial x_v$; contracted discrete Bianchi is definitionally identified with that identity; the one-statement master theorem and the DiscreteBianchiContractedCert package both range over Schläfli-satisfying Regge data built on this carrier. Downstream, Gravity.Track1BCPhysicalResidual's PhysicalReggeEHBianchiInterface consumes the same package to interface the structural Bianchi with the Einstein-Hilbert residual. Within Recognition Science this closes the structural half of Track 1.C (0 sorry, 0 RS-internal axiom): the continuum Einstein equation's contracted Bianchi has a discrete kinematic counterpart once Regge data are typed this way. The full geometric derivation of Schläfli from simplex volume-area relations remains multi-session Mathlib work; this definition only supplies the abstract interface that makes the equivalence and the flat witness formal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.