zero_params_forces_internal_comparison
plain-language theorem explainer
Any comparison mechanism on a state space with an observable can be re-packaged as an internal comparison (no external reference). Closes Step 3 of the recognition-necessity chain: comparison without external data is self-recognition. The proof rebuilds the internal structure from the given fields and witnesses the no-external-ref clause by the comparison map itself.
Claim. Let $S$ be a state space and $\mathrm{obs}: S \to \mathbb{R}$ an observable. For every comparison mechanism $C$ on $(S,\mathrm{obs})$ (a reflexive, symmetric Boolean comparison that returns false whenever $\mathrm{obs}$ takes distinct values), there exists an internal comparison $I$ on $(S,\mathrm{obs})$ whose underlying comparison mechanism equals $C$.
background
The module proves that any framework extracting observables must carry recognition structure: the ability to distinguish and identify states. Strategy is three steps: (1) observables force distinction of states with different values; (2) distinction requires a comparison mechanism; (3) comparison with no external reference is internal self-recognition. The Meta Principle then rules out empty recognition.
An Observable is a real-valued map on states. A ComparisonMechanism supplies a Boolean compare map that is reflexive and symmetric and separates states with unequal observable values. An InternalComparison extends that structure by a no-external-ref clause: for every pair of states the comparison equals some pure function of those two states alone. In a zero-parameter setting that clause is the mathematical stand-in for "comparison cannot consult an outside reference," forcing self-recognition.
proof idea
Term-mode construction, not a deep lemma chase. Build an InternalComparison whose compare, reflexivity, symmetry, and distinction fields are copied verbatim from the given mechanism, then close equality of the underlying mechanism by rfl.
The only obligation is no_external_ref. For arbitrary states $s_1,s_2$, exhibit the mechanism's own compare map as the witnessing pure function $f$, and discharge the equality by reflexivity. So every comparison mechanism is already internal: the external-reference ban is automatic once compare is a function of the two states.
why it matters
Fills Step 3 of the module strategy ("Comparison without external reference = self-recognition"). Together with the upstream distinction and comparison steps it underwrites the main claim that observable extraction requires recognition structure, and that internal comparison is mathematically equivalent to a recognition event (recognizer vs recognized).
In Recognition Science this is the zero-parameter hinge: a framework that cannot smuggle external calibration constants must compare states to themselves, which is recognition. Downstream the Meta Principle forbids the empty case, so the forced internal comparison is non-trivial. No used_by edges are recorded yet; the natural parents are the module's main combination theorems (observables_require_recognition and the distinction-is-recognition bridge).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.