InternalComparison
plain-language theorem explainer
Internal comparison is a comparison mechanism that uses only the states themselves: no external reference scale or oracle. In a zero-parameter framework this is forced, and it is the precise notion of self-recognition used later in the necessity chain. Anyone citing the step from observables to recognition will need this structure. It is a pure structure extension of the base comparison mechanism by a no-external-reference axiom.
Claim. Fix a state space $S$ and an observable $\mathrm{obs}: S \to \mathbb{R}$. An internal comparison on $(S,\mathrm{obs})$ is a comparison mechanism (a Boolean map $\mathrm{compare}: S\times S\to\{\mathrm{true},\mathrm{false}\}$ that is reflexive, symmetric, and separates states with unequal observable values) together with the requirement that for every pair of states $s_1,s_2$ the value $\mathrm{compare}(s_1,s_2)$ equals $f(s_1,s_2)$ for some function $f:S\times S\to\{\mathrm{true},\mathrm{false}\}$ built only from the states (no external reference).
background
The module proves that any framework extracting observables must carry a recognition structure: the capacity to distinguish and identify states. The strategy is three-step: observables imply distinction, distinction requires comparison, and comparison without external reference is self-recognition. The Meta Principle then rules out empty recognition.
An observable on a state space $S$ is simply a real-valued map $\mathrm{value}:S\to\mathbb{R}$. A comparison mechanism supplies a Boolean $\mathrm{compare}$ that is reflexive and symmetric and that returns false whenever two states carry different observable values. That is the minimal algebraic content needed to say "these two states are distinguishable by measurement."
Internal comparison tightens the base mechanism by forbidding an external yardstick. In a zero-parameter setting there is nothing outside the states to compare against, so the comparison map must be realized by a pure function of the two states alone. That is exactly the content of the no_external_ref field.
proof idea
No proof body: this is a structure definition. It extends the base comparison mechanism by a single propositional field asserting that for every pair of states the comparison outcome equals the application of some pure binary Boolean function of those states. Downstream theorems treat an inhabitant of this structure as data plus that axiom; they do not discharge it here.
why it matters
This structure is the formal stand-in for Step 3 of the module strategy: comparison without external reference equals self-recognition. The companion definition ComparisonIsRecognition takes an internal comparison and packages it as a recognition event (comparing state as recognizer, compared state as recognized, comparison as the act). The theorem zero_params_forces_internal_comparison then shows every comparison mechanism can be re-viewed as internal, so the zero-parameter hypothesis collapses the distinction.
In the broader Recognition Science forcing picture this is the verification-side necessity claim that observables already force a recognition structure, before cost, $J$-uniqueness, or the eight-tick octave enter. It sits upstream of the main necessity theorem that observables require recognition, and it is the precise interface those later results consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.