local_J_cost
plain-language theorem explainer
The definition assigns to each 3-simplex s and real potential ψ the product of the base J-cost evaluated at ψ and the volume of s. Researchers formalizing cost summations over simplicial ledgers cite it when passing from local to global quantities. It is realized by direct multiplication of the J-cost function by the simplex volume.
Claim. For a 3-simplex $s$ with positive volume $V(s)$ and real potential $ψ$, the local J-cost equals $J(ψ) · V(s)$, where $J$ denotes the J-cost function induced by the multiplicative recognizer.
background
The Simplicial Ledger module formalizes the ledger as a simplicial 3-complex, supplying a coordinate-free sheaf representation that unifies local and global J-cost variations. A Simplex3 is the 3-simplex (tetrahedron) that serves as the atom of volume, carrying vertices in (Fin 4 → (Fin 3 → ℝ)) together with a positive real volume. The J-cost function is taken from the upstream cost definitions: one induced by the comparator of a multiplicative recognizer and the other identifying the cost of any recognition event with J-cost of its state.
proof idea
The definition is a one-line wrapper that multiplies the J-cost of the supplied potential by the volume field of the simplex.
why it matters
This definition supplies the local term inside the global J-cost summation over a finite simplicial ledger. It is invoked by the interior-flat consistency theorem to confirm that J-cost remains stationary inside each simplex when the potential is constant. In the Recognition framework it realizes the local scaling step required for the simplicial unification of J-cost, consistent with the eight-tick octave and the emergence of three spatial dimensions through the volume measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.