evolve_changes_observable_implies_distinct
plain-language theorem explainer
If some state's observable value changes under one evolution step of a physics framework, then that observable takes at least two distinct values on the state space. Verification and necessity arguments cite it to turn dynamical non-constancy into static distinguishability. The proof is a two-line existential unpack: witness the pair (evolve s, s).
Claim. Let $F$ be a physics framework with state space $S$ and evolution map $\mathrm{evolve}: S\to S$. Let $\mathrm{obs}: S\to\mathbb{R}$ be an observable. If there exists $s\in S$ with $\mathrm{obs}(\mathrm{evolve}(s))\neq\mathrm{obs}(s)$, then there exist $s_1,s_2\in S$ with $\mathrm{obs}(s_1)\neq\mathrm{obs}(s_2)$.
background
This module shows that any framework extracting observables must carry a recognition structure: the capacity to distinguish and identify states. The strategy is that measurable quantities force distinction, distinction forces comparison, and comparison without external reference is self-recognition; the Meta Principle then rules out empty recognition.
An Observable on a state space is a map value : StateSpace → ℝ, i.e. a real-valued quantity extractable from a state. The local claim sits one step before the main necessity chain: if evolution ever moves that real value, the image of value is non-constant, so two states are already distinguished by the observable alone.
Upstream, distinction is the primitive binary predicate on a carrier (canonical case: inequality). Framework-level observables are the same real-valued extraction pattern used in recognition forcing. Evolution here is the framework's one-step dynamics on states, not a specific ledger kernel.
proof idea
Term-mode existential proof. Destructure the hypothesis to a witness state $s$ with $\mathrm{obs}(\mathrm{evolve}, s)\neq\mathrm{obs}, s$. Supply the pair $(\mathrm{evolve}, s,, s)$ as the two states with unequal observable values, flipping inequality with ne_comm via simpa. No lemmas beyond existential introduction and commutativity of $\neq$.
why it matters
In the Recognition Structure Necessity module this is a bridge lemma: dynamical change of an observable is converted into static distinguishability of states, which is the first step toward observables_require_distinction and the main observables_require_recognition chain. Without non-constant values there is nothing to compare, so recognition never starts.
The module's larger claim is that any framework deriving observables must admit recognition structure (distinction plus internal comparison), with MP forbidding the empty case. This lemma is elementary bookkeeping on that path: evolution that moves a measured quantity already supplies a distinction event. No downstream uses are recorded yet; it is local scaffolding for the necessity argument rather than a forcing-chain (T0–T8) landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.