local_variation
plain-language theorem explainer
The local variation approximates the derivative of J-cost with respect to potential at a 3-simplex voxel via finite difference. Researchers unifying local and global stationarity on simplicial manifolds cite it when stating hypotheses about J-cost minimization. It is realized as a one-line forward difference applied to the upstream Jcost function.
Claim. For a 3-simplex voxel $s$ and real potential value $ψ$, the local variation is defined by the forward difference quotient $(J(ψ + 0.001) - J(ψ))/0.001$, where $J$ is the J-cost function on the potential.
background
The Simplicial Ledger module encodes the ledger as a simplicial 3-complex whose atoms are 3-simplices (tetrahedra) with positive volume. Each simplex carries a local potential whose J-cost is supplied by the cost function of a multiplicative recognizer or recognition event. The module supplies a coordinate-free sheaf that unifies local and global J-cost variations, as described in the module documentation.
proof idea
This is a one-line definition that applies the forward finite-difference formula directly to the Jcost function with fixed step 0.001. It draws on the Jcost implementation imported from upstream cost definitions in MultiplicativeRecognizerL4 and ObserverForcing.
why it matters
The definition supplies the local stationarity predicate used inside the hypothesis H_LocalGlobalUnification and the theorem local_global_unification, which together assert that global J-cost stationarity on the simplicial manifold is equivalent to stationarity at every local simplex. It thereby closes a step in the Recognition Science forcing chain by ensuring scale-consistent minimization of J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.