DistinguishabilityOn
plain-language theorem explainer
DistinguishabilityOn encodes the non-degeneracy requirement for a comparison operator C on an ordered field K: there must exist positive x and y with C x y nonzero. Researchers working on the Recognition Science bootstrap from logic to reals cite this as the minimal condition ensuring the operator is not trivial on the positive cone. The definition is a direct existential predicate with no additional proof obligations.
Claim. Let $K$ be a field with zero element and strict order. A comparison operator $C: K → K → K$ is distinguishable when there exist $x, y ∈ K$ such that $0 < x$, $0 < y$, and $C(x, y) ≠ 0$.
background
The module DomainBootstrap addresses the bootstrap theorem for the comparison-operator domain. A comparison operator is defined as a map $C: K → K → K$ on a linearly ordered field $K$. The local setting requires that the Law of Logic can be stated on $K$, leading to an isomorphism with the reals under Archimedean and Dedekind completeness hypotheses. The completeness hypothesis is the standard analytic input that makes continuous comparison non-vacuous; without it, the comparison operator could live on $ℚ$ or any incomplete subfield.
proof idea
The definition is the direct statement of the existential condition for distinguishability.
why it matters
This definition is a component of the LogicSupported structure, which collects the conditions under which a linearly ordered field supports the Law of Logic. It contributes to the uniqueness theorem that any such field is isomorphic to the reals, closing the loop between the Law of Logic on $ℝ$ and the recovered LogicReal. In the Recognition framework this resolves the chicken-and-egg issue by showing that the ambient field must be $ℝ$ when the comparison operator satisfies these properties together with completeness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.