section_stationarity
plain-language theorem explainer
Local sections of a recognition sheaf S over a topological space M evaluate to the J-cost minimum at every point. Researchers modeling recognition dynamics in spacetime would cite this to confirm local potentials sit at equilibrium. The proof is a one-line wrapper that rewrites the ratio to unity via the companion theorem and applies the known Jcost(1)=0 lemma.
Claim. Let $M$ be a topological space, $S$ a recognition sheaf on $M$ with continuous positive potential function $phi$, $U subset M$ open, $x in U$, and $f$ a local section of $S$ over $U$. Then $J(f(x)/phi(x)) = 0$.
background
The RecognitionSheaf is a structure on a topological space M consisting of a continuous positive potential function phi : M to R. A LocalSection over an open U is a function f : U to R that coincides exactly with phi on U, so the ratio f(x)/phi(x) is identically 1. The J-cost is the abbrev for the Cost.Jcost functional, whose minimum value of zero at argument 1 is recorded in the upstream lemma Jcost_unit0.
proof idea
The term proof introduces the local section f, rewrites the goal using the sibling theorem section_stationarity_thm that forces the ratio to one, and concludes by applying the lemma Jcost_unit0.
why it matters
This anchors the local equilibrium property inside the recognition sheaf construction, directly supporting the J-cost minimum as the stable point of ledger dynamics. It fills the stationarity step required by the module objective of proving local sections obey the J-cost principle, linking to the Recognition Science framework where J-uniqueness forces the fixed point at unity. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.