recognition_ratio_unity
plain-language theorem explainer
Any local section f of a recognition sheaf S over U satisfies f(x) = S.potential(x) at every x in U, so the ratio f(x)/S.potential(x) equals one wherever the potential is nonzero. Researchers modeling spacetime via recognition sheaves would cite this to confirm local-to-global consistency of stationary sections. The proof is a one-line wrapper that rewrites via the local section equality lemma then applies the self-division identity.
Claim. Let $S$ be a recognition sheaf over a topological space $M$, let $U$ be a subset of $M$, let $f$ be a local section of $S$ over $U$, and let $x$ belong to $U$ with $S$.potential$(x) ≠ 0$. Then $f(x) / S$.potential$(x) = 1$.
background
The RecognitionSheaf is a structure on a topological space $M$ that assigns a continuous positive real-valued potential function to each point; the sheaf encodes the recognition potential over spacetime. A LocalSection of $S$ over $U$ is defined as a function $f : U → ℝ$ satisfying $f(x) = S$.potential$(x)$ for every $x$ in $U$ by construction. The module sets the local theoretical setting as the sheaf of recognition potentials whose sections are required to obey J-cost stationarity, where J is the convex cost function with unique minimum at argument one.
proof idea
The term proof first rewrites the left-hand side using the local_section_eq_global lemma, which replaces the local section value by the sheaf potential at $x$. It then applies the exact div_self tactic to the nonzero hypothesis on the potential, yielding the identity 1 = 1.
why it matters
This theorem supplies the elementary consistency step that any local section is identically the restriction of the global potential, thereby supporting the module's objective of gluing local stationary sections into a global configuration. It directly realizes the J-cost minimum at ratio one inside the sheaf setting and aligns with the Recognition Composition Law and phi-forcing chain by enforcing stationarity wherever the potential is defined. No downstream uses are recorded, leaving open whether it will be invoked inside a full sheaf-gluing theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.