Simplex4D
plain-language theorem explainer
A 4-simplex is specified by a map from the ten edges to positive reals. Workers on discrete gravity in Recognition Science cite this structure when assembling simplicial complexes for exact curvature on the RS lattice. The definition encodes the combinatorial count of edges in a 4-simplex together with the positivity condition that guarantees a realizable geometry.
Claim. A 4-simplex is given by ten edge lengths $e_i > 0$ for $i=1,2,5,6,7,8,9,10$ (indexed by Fin 10), with the geometry fixed entirely by these lengths.
background
The module formalizes exact Regge calculus on the RS lattice, replacing the linearized deficit-angle ansatz with the full nonlinear machinery. Curvature is concentrated on codimension-2 hinges and the Regge action is the sum over hinges of area times deficit angle. The structure Simplex4D supplies the basic 4-simplex datum: five vertices determine exactly ten edges whose lengths fix all angles and volumes via the Cayley-Menger determinant.
proof idea
The declaration is a direct structure definition. It introduces the field edges of type Fin 10 → ℝ together with the field all_pos enforcing strict positivity on each component. No lemmas or tactics are invoked.
why it matters
Simplex4D supplies the geometric primitive required by the Regge action and hinge data constructions in the same module. It closes the gap between the paper's Assumption A2 and the full discrete gravity programme on the Z³ × Z lattice. The definition therefore supports later results on non-negative action for flat configurations and the Gauss-Bonnet identity for closed surfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.