LocalSection
plain-language theorem explainer
The LocalSection definition specifies the type of maps from an open set U to the reals that coincide pointwise with the potential of a given recognition sheaf S. Researchers formalizing sheaf models of recognition costs over spacetime manifolds cite this when reducing local stationarity statements to the global J minimum. The definition is a direct subtype construction that enforces exact matching to the sheaf potential at every point in U.
Claim. Let $M$ be a topological space and $S$ a recognition sheaf on $M$. For an open set $Usubseteq M$, a local section of $S$ over $U$ is a function $f:Utomathbb{R}$ such that $f(x)=S.potential(x)$ for every $x in U$.
background
The RecognitionSheaf structure on a topological space $M$ consists of a potential map $Mtomathbb{R}$ that is continuous and strictly positive at every point. The module sets up the sheaf of recognition potentials over spacetime with the explicit objective of proving that its local sections obey the J-cost stationarity principle. Upstream constants supply the RS-native gauge in which $c=1$, while cost definitions from multiplicative recognizers and observer forcing identify the relevant cost functional as the J-cost on positive ratios.
proof idea
The declaration is a subtype definition: the type of all functions from $U$ to $mathbb{R}$ whose value at each point equals the sheaf potential. No lemmas or tactics are invoked; the construction directly encodes the equality condition that later theorems apply to reach J(1)=0.
why it matters
LocalSection supplies the objects used by local_section_eq_global, recognition_ratio_unity, section_stationarity and section_stationarity_thm to conclude that every local section realizes the J-cost minimum. It therefore realizes the sheaf setting in which the recognition ratio is identically one, directly supporting the module goal of establishing J-cost stationarity for recognition potentials. The construction sits inside the Recognition Science program that derives dynamics from the single functional equation for J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.