SimplicialLedger
plain-language theorem explainer
A simplicial ledger consists of a non-empty collection of three-simplices equipped with a manifold covering property. Researchers deriving lower bounds on recognition loop lengths in simplicial complexes cite this structure. The declaration is introduced directly as a structure definition with no separate proof body.
Claim. A simplicial ledger consists of a non-empty set of three-simplices together with a proposition asserting that the set forms a manifold covering.
background
This module formalizes the ledger as a simplicial three-complex rather than a coordinate-fixed cubic lattice. It supplies a coordinate-free sheaf representation that unifies local and global J-cost variations. A three-simplex is a tetrahedron whose vertices are given by a map from four indices to three-dimensional real space and whose volume is strictly positive. Upstream results fix the active edge count per tick at one and define the actualization operator as the map sending each configuration to its J-cost minimizer.
proof idea
The declaration is a structure definition that directly introduces the simplicial ledger type along with its three fields: the set of simplices, a non-emptiness witness, and a covering proposition.
why it matters
This definition supports downstream results including the eight-tick uniqueness theorem for recognition loops and the local-global unification of J-cost stationarity. It implements the simplicial manifold covering step within the Recognition Science framework, aligning with the eight-tick octave and three spatial dimensions. The covering property remains a scaffold requiring simplicial complex axioms for full discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.