J_stationary_at_one
plain-language theorem explainer
The J-cost function has a stationary point at the unit recognition ratio. Researchers modeling ledger equilibrium in sheaf-theoretic dynamics would cite this to anchor local section stability. The proof is a direct term application of the precomputed derivative result for the underlying cost function.
Claim. The derivative of the J-cost function satisfies $J'(1) = 0$.
background
The Recognition Sheaf module treats the recognition potential as a sheaf over spacetime, with local sections required to satisfy J-cost stationarity. J is the abbreviation for the Jcost function imported from the Cost module; its derivative at argument 1 is the object of study. The upstream result deriv_Jcost_one supplies the explicit differentiation: it applies hasDerivAt_Jcost at 1 followed by simplification to obtain the zero derivative.
proof idea
One-line wrapper that applies deriv_Jcost_one after the identification of J with Jcost.
why it matters
This supplies the core stationarity lemma for local sections of the recognition sheaf, feeding section_stationarity_thm and related gluing results in the same module. It realizes the physical claim that the recognition ratio equal to 1 is the stable ledger equilibrium, consistent with the J-uniqueness step in the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.