flatSchlafliReggeData

Track 1.C of the quantum-gravity plan equates the contracted discrete Bianchi identity $\nabla_\mu G^{\mu\nu}=0$ on a Regge substrate with the Schläfli identity at each interior vertex: $\sum_{b\ni v}\varepsilon_b,\partial A_b/\partial x_v=0$, with $\varepsilon_b$ the deficit at bone $b$ and $A_b$ its area.

Abstract Regge data supply vertex positions, incidence, deficit angles, and bone areas. A Schläfli-satisfying Regge triangulation is Regge data plus a proof that Schläfli holds at every vertex; that named hypothesis is what makes contracted discrete Bianchi automatic at the structural level.

Flat Regge data set every deficit and every area gradient to zero. The companion lemma shows Schläfli holds there vacuously (sum of zeros). This definition packages that pair into the Schläfli-satisfying structure.

One-line structure instance. The underlying Regge data field is the flat witness (zero deficits, zero area gradients). The Schläfli field is filled by the already-proved lemma that flat data satisfy Schläfli at every vertex, via simp on the zero deficit and gradient fields.

Supplies the concrete inhabitant that makes the Schläfli-satisfying hypothesis space nonempty. Downstream, the inhabited theorem is exactly ⟨flatSchlafliReggeData V B⟩, so every later appeal to a nonempty Schläfli class rests on this witness.

In the module narrative this is the "canonical witness": the trivial all-deficits-zero substrate where Schläfli holds by construction. It closes the structural half of Track 1.C without waiting on the full geometric Schläfli proof (simplex volume-area calculus), which remains multi-session Mathlib work. The conditional master theorem then gets contracted discrete Bianchi on any Schläfli-satisfying triangulation, with flat data as the non-vacuous base case.