LocalSection
plain-language theorem explainer
LocalSection defines the subtype of maps from an open set U in a topological space M to the reals that coincide pointwise with the potential of a recognition sheaf S. Researchers modeling recognition dynamics via sheaves over spacetime would cite it to establish local-to-global potential equality. The definition is a direct subtype construction enforcing the equality condition.
Claim. Let $M$ be a topological space and $S$ a recognition sheaf on $M$ with potential function $S.potential : M → ℝ$. For an open set $U ⊆ M$, a local section of $S$ over $U$ is a function $f : U → ℝ$ such that $f(x) = S.potential(x)$ for all $x ∈ U$.
background
The recognition sheaf is a structure over the spacetime manifold M consisting of a continuous positive real-valued potential function at each point. This draws from upstream cost definitions: the J-cost of a recognition event via ObserverForcing.cost and the derived cost from MultiplicativeRecognizerL4.cost, both non-negative by construction. The module sets the local theoretical setting as proving that local sections of this sheaf satisfy the J-cost stationarity principle at unit ratio.
proof idea
The definition is a one-line subtype construction that applies the subtype predicate ∀ x : U, f x = S.potential x directly to the function space U → ℝ.
why it matters
This definition supplies the local objects used by downstream results local_section_eq_global, recognition_ratio_unity, and section_stationarity_thm to prove that any local section yields recognition ratio 1 and J-cost exactly J(1) = 0. It fills the sheaf-theoretic step toward the J-cost stationarity principle in the recognition framework, linking to T5 J-uniqueness and the minimum at unit ratio. No scaffolding or open questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.