Simplex3
plain-language theorem explainer
The Simplex3 structure defines a tetrahedron as four points in three-dimensional Euclidean space together with a positive real volume scalar. Modelers of the ledger as a coordinate-free simplicial complex cite this as the atomic volume element. The declaration is a pure structure definition carrying no proof obligations or computational content.
Claim. A 3-simplex consists of four points in $mathbb{R}^3$ together with a scalar $V > 0$ that represents its volume.
background
The module replaces a fixed cubic lattice with a simplicial 3-complex to obtain a coordinate-free sheaf representation that unifies local and global J-cost variations. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, whose strict convexity and unique minimum at $x=1$ are recorded in the upstream PhysicsComplexityStructure result. The IntegrationGap.A definition supplies the active edge count per fundamental tick, fixed at 1, which enters the phi-power balance identity at $D=3$.
proof idea
This is a structure definition; it introduces the type with three fields and the positivity constraint. No lemmas are applied and no tactics are used.
why it matters
Simplex3 supplies the volume element required by local_J_cost, local_variation, and the recognition_loop_has_surjection predicate. It is invoked directly in eight_tick_uniqueness to establish the minimal cycle length of 8 and in DimensionForcing.simplicial_loop_tick_lower_bound. The definition realizes the $D=3$ spatial dimension forced by the T0-T8 chain and supports the eight-tick octave periodicity on the simplicial manifold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.