SimplicialSheaf
plain-language theorem explainer
SimplicialSheaf equips a simplicial ledger with a real-valued potential map on each 3-simplex together with a boundary consistency proposition. Researchers modeling J-cost stationarity on discrete 3-manifolds cite this structure when passing from local potentials to summed global costs. The declaration is a bare structure definition that introduces the two fields with no separate proof or lemmas.
Claim. A simplicial sheaf over a ledger $L$ is a pair consisting of a function assigning a real number (recognition potential) to each 3-simplex together with a proposition asserting consistency of the potential across simplex boundaries.
background
The SimplicialLedger collects 3-simplices (tetrahedra) into a non-empty set that forms a manifold covering, with each Simplex3 specified by four vertices in three-dimensional space and strictly positive volume. This module replaces coordinate-fixed lattices by a coordinate-free simplicial 3-complex whose sheaf data unifies local and global J-cost variations. Upstream definitions supply the relevant cost maps: ObserverForcing.cost equates recognition-event cost with J-cost, while MultiplicativeRecognizerL4.cost derives cost from comparator ratios on positive arguments.
proof idea
The declaration is a structure definition whose body consists solely of the two fields: potential of type Simplex3 to reals and the placeholder is_consistent proposition. No tactics, reductions, or upstream lemmas are invoked; downstream code simply supplies concrete data for these fields when constructing instances.
why it matters
The structure supplies the sheaf data required by global_J_cost, which sums local J-costs over the finite simplex set, and by the local_global_unification theorem that equates global stationarity with pointwise J-stationarity on each simplex. It realizes the coordinate-free sheaf representation described in the module documentation for simplicial ledger topology. The construction supports the framework's three-dimensional spatial structure by furnishing the discrete manifold on which J-cost functionals are evaluated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.