Simplex3
plain-language theorem explainer
Simplex3 defines the 3-simplex as four vertices in R^3 paired with a strictly positive volume, serving as the indivisible volume element in the simplicial ledger. Discrete-spacetime modelers and researchers formalizing J-cost on manifolds would cite this structure when constructing coordinate-free coverings. The declaration is introduced as a bare structure with no reduction steps or lemmas.
Claim. A 3-simplex consists of a map assigning three real coordinates to each of four vertices together with a positive real volume: vertices : Fin 4 → (Fin 3 → ℝ), volume : ℝ with volume > 0.
background
The module formalizes the ledger as a simplicial 3-complex, supplying a coordinate-free sheaf that unifies local and global J-cost variations. Simplex3 packages the geometric atom: four points in three-dimensional Euclidean space and a positive scalar volume. Upstream structures supply the J-cost function J(x) = (x + x^{-1})/2 - 1, shown convex with unique minimum at x = 1, and the active-edge count A = 1 that balances φ-powers at D = 3.
proof idea
The declaration is a structure definition containing no tactics, lemmas, or computational content; it simply records the vertex map and volume datum required by sibling definitions such as local_J_cost and is_recognition_loop.
why it matters
Simplex3 supplies the volume primitive that downstream results such as eight_tick_uniqueness and simplicial_loop_tick_lower_bound rely upon to prove that every recognition loop contains at least eight ticks. It realizes the D = 3 spatial dimension forced by the T0-T8 chain and the eight-tick octave period, closing the passage from abstract J-cost minimization to concrete manifold coverings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.