section_stationarity_thm
plain-language theorem explainer
Local sections of the recognition sheaf over a topological space evaluate the J-cost at the unit ratio. Researchers deriving equilibrium conditions for recognition potentials on spacetime manifolds cite this when establishing local minima of the cost functional. The proof is a direct algebraic reduction that substitutes the local section definition and simplifies the ratio using positivity of the potential.
Claim. Let $S$ be a recognition sheaf on a topological space $M$, $U$ an open subset of $M$, $x$ a point in $U$, and $f$ a local section of $S$ over $U$. Then $J(f(x)/S.potential(x)) = J(1)$, where $J$ is the J-cost functional.
background
A recognition sheaf on a topological space $M$ consists of a continuous positive real-valued potential function on $M$. A local section over an open set $U$ is a map $f: U → ℝ$ satisfying $f(x) = S.potential(x)$ for every $x$ in $U$. The J-cost is the cost functional induced by the multiplicative recognizer, with a global minimum of zero at argument 1.
proof idea
The term-mode proof first invokes the local section property to replace $f.val x$ by $S.potential x$. It then rewrites the ratio inside $J$ to 1 by dividing by the nonzero value guaranteed by the potential_pos field of the sheaf.
why it matters
This theorem supplies the local stationarity step that feeds the parent result section_stationarity, which concludes that the J-cost equals zero. It realizes the J-cost stationarity principle inside the sheaf of recognition potentials, aligning with the J-uniqueness fixed point in the forcing chain where the unit ratio is the equilibrium of the ledger dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.