J_stationary
plain-language theorem explainer
J_stationary(ψ) asserts that a local potential ψ on the simplicial ledger equals unity. Workers on local-global unification of J-costs cite the predicate when expressing equilibrium conditions at each simplex section. It is introduced by direct abbreviation of the equality ψ = 1.
Claim. The predicate $J_ {stationary}(ψ)$ for $ψ ∈ ℝ$ holds precisely when $ψ = 1$.
background
The SimplicialLedger module formalizes the ledger as a simplicial 3-complex with a coordinate-free sheaf representation that unifies local and global J-cost variations. J-cost is the cost of a recognition event or the derived cost of a multiplicative recognizer comparator, as supplied by upstream definitions in ObserverForcing.cost and MultiplicativeRecognizerL4.cost. The predicate appears inside the hypothesis H_LocalGlobalUnification, which states that vanishing local variations force every local potential to its unit value.
proof idea
The declaration is a one-line definition that sets the predicate equal to the condition ψ = 1. No lemmas or tactics are applied.
why it matters
The predicate supplies the stationarity marker for the local-global unification theorem in the same module, which asserts that global J-cost stationarity holds if and only if every local section is stationary. It encodes the fixed-point condition of the J function inside the simplicial ledger topology and touches the empirical hypothesis that global minimization forces local unit values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.