SimplicialEdgeData
plain-language theorem explainer
SimplicialEdgeData records a finite collection of positive real edge lengths indexed by Fin nE for use in a simplicial complex. Workers on Regge calculus and discrete gravity cite it when setting up the edge-length variables for Schläfli's identity. The declaration is a plain structure definition that directly introduces the length map and its positivity predicate with no further obligations.
Claim. For a natural number $n_E$, simplicial edge data consists of a function $L: {1,2,…,n_E} → ℝ$ such that $L(e) > 0$ for every edge index $e$.
background
The module formalizes Schläfli's identity for piecewise-flat simplicial complexes as Phase C3 toward discharging the Regge deficit linearization hypothesis. For a simplicial n-complex K the edge lengths L_e and hinge areas A_h determine dihedral angles θ_σ,h via the Cayley-Menger determinant; the identity then states that Σ_h A_h (∂θ_h / ∂L_e) = 0 for each edge e. This structure supplies the abstract edge-length assignment L_e that enters the partial derivatives in the identity. Upstream results supply the J-cost and ledger structures used to calibrate lengths in the broader Recognition framework, while the module itself records the identity as a named hypothesis because Mathlib lacks the required geometric calculus.
proof idea
The declaration is a structure definition that directly introduces the two fields len and len_pos; no lemmas or tactics are applied.
why it matters
The structure supplies the edge-length data required to state Schläfli's identity and thereby reduce the Regge equations from two terms to one, as described in the module documentation. It supports the linearization step that converts δS_Regge / δL_e into a single sum over hinge deficits. The declaration touches the open question of discharging the Regge deficit linearization hypothesis on general complexes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.