Simplex3
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not impose gluing conditions or manifold topology on collections of simplices.
- Does not embed vertices into a global coordinate chart or enforce metric consistency.
- Does not compute or constrain J-cost, variation, or pattern states.
- Does not reference the phi-ladder, mass formula, or Recognition Composition Law.
formal statement (Lean)
24structure Simplex3 where
25 vertices : Fin 4 → (Fin 3 → ℝ)
26 volume : ℝ
27 vol_pos : volume > 0
28
29/-- **DEFINITION: Simplicial Ledger**
30 A collection of 3-simplices that form a manifold covering. -/
used by (20)
-
simplicial_loop_tick_lower_bound -
eight_tick_uniqueness -
is_recognition_loop -
local_J_cost -
local_variation -
recognition_loop_has_surjection -
SimplicialLedger -
SimplicialSheaf -
defaultEuclideanInterior -
defaultMinkowskiInterior -
FlatInteriorMetric -
InteriorFlatCert -
interior_holonomy_trivial -
interior_jcost_const_consistent -
InteriorLoop -
NonHingeStratum -
trivial_interior_loop -
AreaOperator -
is_ledger_eigenstate -
simplicial_area_decomposition