comparison_exists
plain-language theorem explainer
For any observable on a state space, a reflexive Boolean comparison of states exists constructively: decide equality of the extracted real values. Cited in the necessity chain that turns measurable extraction into distinction and then into recognition. The proof is a direct witness plus reflexivity by simplification.
Claim. Let $S$ be any type of states and let $O:S\to\mathbb{R}$ be an observable (a real-valued extraction map). Then there exists a comparison $\mathrm{cmp}:S\to S\to\{\mathrm{true},\mathrm{false}\}$ such that $\mathrm{cmp}(s,s)=\mathrm{true}$ for every $s\in S$.
background
This module shows that any framework extracting observables must carry a recognition structure: the ability to distinguish and identify states. The strategy is three-step: measurable extraction implies distinguishability; distinction requires comparison; comparison without external reference is self-recognition. The Meta Principle then rules out empty recognition.
An Observable on a state space $S$ is just a map $\mathrm{value}:S\to\mathbb{R}$. Downstream siblings package comparison mechanisms and the claim that distinction without external reference is recognition. The present lemma is the constructive existence half of that packaging: given any such value map, a reflexive Boolean comparator can be written down explicitly.
Upstream calculus material (registry evaluation to reals, one-step trace extension) supplies the ambient language of certified real values, but is not invoked in the body of this particular proof.
proof idea
Term/tactic hybrid, fully constructive. Witness the existential with the function that, on a pair of states, runs decide on equality of their observable values. Reflexivity is immediate: for fixed $s$, the two arguments are identical, so the decided equality is true; simp closes the goal. No external lemmas are required beyond decidable equality on $\mathbb{R}$ as used by decide.
why it matters
Fills the constructive existence step in the Recognition Necessity chain (module main results: observables require distinction; distinction is recognition; observables require recognition). Without an explicit comparator, later claims that distinction requires comparison and that internal comparison is recognition would be non-constructive. It supports the Step-2 slogan "distinction requires comparison" and the packaging of comparison mechanisms as recognition events.
No tracked downstream theorems yet (used_by empty), so its role is local scaffolding inside the necessity module rather than a cited leaf of the T0–T8 forcing chain. It does not itself invoke J-cost, $\varphi$, or the eight-tick octave; it only secures that observables come with a reflexive comparison, which the Meta Principle later forces to be non-empty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.