J
plain-language theorem explainer
The abbreviation J stands for the J-cost function inside the recognition sheaf over spacetime. Researchers deriving equilibrium conditions for local sections at unit recognition ratio would cite it when invoking the stable point of ledger dynamics. It is realized as a direct noncomputable abbreviation of the cost imported from the Cost module.
Claim. Let $J: (0,∞) → ℝ$ be the J-cost function on positive ratios, defined as the derived cost of the comparator in a multiplicative recognizer and satisfying $J(1)=0$ as global minimum.
background
The Recognition Sheaf module models the recognition potential as a sheaf ℛ over the spacetime manifold M, with the objective of showing that local sections obey the J-cost stationarity principle. The J-cost is calibrated on the multiplicative group of positive reals, as structured in LedgerFactorization, and equals the cost of any recognition event. Upstream results supply the explicit form: MultiplicativeRecognizerL4.cost returns derivedCost of the comparator on positive ratios, while ObserverForcing.cost assigns Cost.Jcost directly to the state of a recognition event.
proof idea
The declaration is a one-line abbreviation that directly aliases the J-cost definition from the Cost module.
why it matters
This abbreviation supplies the symbol J for the core lemma on stationarity at the unit ratio, the stable equilibrium of recognition-ratio dynamics. It supports the module's later results on section stationarity, local-to-global equality, and sheaf gluing. In the framework it realizes the J-uniqueness step (T5) of the forcing chain, where J(x)=(x+x^{-1})/2−1, and anchors the stationarity principle required by the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.