global_J_cost
plain-language theorem explainer
Global J-cost aggregates local recognition costs across all simplices in a finite simplicial ledger by summing the volume-weighted J-cost of the sheaf potential on each simplex. Researchers modeling discrete manifolds or recognition processes in Recognition Science cite this when moving from local events to total ledger cost. The definition is a direct finite summation that applies the local J-cost definition to each simplex.
Claim. Let $L$ be a simplicial ledger of 3-simplices forming a manifold covering and $S$ a simplicial sheaf assigning a recognition potential to each simplex, with finitely many simplices. The global J-cost is the sum over all simplices $s$ in $L$ of the local J-cost of $s$ evaluated at the potential $S(s)$.
background
A Simplicial Ledger collects 3-simplices into a set that forms a manifold covering, supplying a coordinate-free representation instead of a fixed cubic lattice. A Simplicial Sheaf on such a ledger assigns a recognition potential to each simplex, with boundary consistency left as a placeholder. The module therefore unifies local and global J-cost variations on a simplicial 3-complex. Upstream, local J-cost on one simplex is the product of the J-cost function and the simplex volume, inheriting from cost definitions in multiplicative recognizers and observer forcing.
proof idea
This is a one-line definition that sums the local J-cost over the finite set of simplices supplied by the ledger, feeding each simplex and its sheaf potential into the local definition.
why it matters
The definition supplies the global aggregation step required by the simplicial ledger module, completing the passage from local J-cost on individual simplices to total ledger cost. It supports the Recognition Science program of deriving physics from a single functional equation by furnishing a manifold-native expression for total J-cost, consistent with the shift to simplicial complexes. No downstream theorems are yet attached, leaving open how this global quantity enters higher forcing-chain results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.