flatReggeData
plain-language theorem explainer
Canonical flat Regge triangulation: all deficit angles, bone areas, and area gradients vanish, with every bone treated as incident to every vertex. It is the trivial witness that the Schläfli identity holds vacuously on a flat substrate. Downstream theorems cite it to inhabit the type of Schläfli-satisfying Regge data. The construction is a pure structure instance with zero fields and a reflexivity proof of the non-incidence gradient constraint.
Claim. For any vertex type $V$ and bone type $B$ with $B$ finite, there is abstract Regge data on $(V,B)$ in which every vertex position is the origin in $\mathbb{R}^4$, every bone is incident to every vertex, every deficit angle is $0$, every bone area is $0$, and every vertex-area gradient is $0$ (the non-incidence gradient law holds by reflexivity).
background
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,$$
where $\varepsilon_b$ is the deficit angle at bone $b$ and $A_b$ its area.
ReggeData V B packages the abstract fields needed to state that identity: vertex positions in Euclidean $4$-space, an incidence predicate, deficit angles, bone areas, and the partials of bone area with respect to vertex coordinates (forced to vanish off the incidence relation). The full geometric proof of Schläfli from simplex volume-area calculus is deferred; this module supplies the structural interface and a trivial witness.
Flat data means a substrate with vanishing curvature defects: every $\varepsilon_b=0$ and every area gradient zero, so the Schläfli sum is identically zero.
proof idea
Pure structure construction, not a proof. Each field of ReggeData is filled by a constant zero (or the constantly-true incidence predicate). The only proof obligation is nonIncident_gradient, discharged by rfl because the gradient is the zero function, so the required equality holds definitionally even when incidence is ignored. No upstream lemmas are applied.
why it matters
This is the canonical non-vacuous witness promised by the module doc: flat substrate data on which Schläfli holds by construction (zero deficits imply a zero sum). It feeds flatReggeData_schlafli, which proves the Schläfli identity at every vertex by simp, and flatSchlafliReggeData, which packages the pair into inhabited SchlafliReggeData. That inhabitation closes the structural half of Track 1.C (contracted discrete Bianchi via Schläfli) without waiting on full simplex-geometry infrastructure. In the broader RS gravity track it shows the kinematic Bianchi constraint is consistent on a flat background before curved or continuum (Track 1.B) content is restored.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.