Foundation Domain Bootstrap Distinguishability On

The distinguishability condition

Distinguishability is a formal condition on a comparison operator, a two-input function that returns a value. The condition states that there exist two positive inputs for which the operator's output is not zero. In plain terms, it requires that the operator is not trivially constant: it must be able to tell some pair of positive values apart. This is the simplest possible non-triviality requirement, and it is the one that the Recognition Science framework uses.

The declaration DistinguishabilityOn is a definition in the framework's machine-checked library of formal theorems. It is one of several conditions that a comparison operator must satisfy to be considered a valid instance of the framework's core structure. The other conditions are identity, which says comparing a value with itself returns zero; non-contradiction, which says the operator is symmetric; and scale invariance, which says scaling both inputs by the same positive factor leaves the output unchanged. Together, these four conditions are called the Aristotelian conditions.

The role of distinguishability is to rule out degenerate cases. Without it, a comparison operator could return zero for every pair of inputs, which would make the other conditions trivially true but would carry no information. With distinguishability, the operator is guaranteed to produce at least one non-zero output, giving the framework a foothold from which to build a richer structure.

In Recognition Science, the framework models a fundamental ledger, a discrete record of events, where the cost of recognition, the price of telling two events apart, is forced by the structure of comparison. The distinguishability condition ensures that this cost is not always zero, meaning the ledger is not empty of distinctions. This is a necessary step for the framework to derive the real numbers as the unique ambient field on which its laws can operate.

The framework's library shows that a linearly ordered field on which the comparison operator satisfies these conditions, plus the standard analytic assumption of Archimedean completeness, is canonically isomorphic to the real numbers. This is a theorem, not a hypothesis, and it is proved in the library's DomainBootstrap module. Distinguishability is a component of that theorem, but it is not the whole story: the theorem also requires the completeness assumption, which is the residual analytic input the framework does not derive.

What distinguishability does not claim is that the real numbers are the only possible domain for the comparison operator. On its own, the condition is satisfied by any field that has at least two distinct positive elements, including the rational numbers. The uniqueness of the real numbers comes from the additional completeness hypothesis, not from distinguishability alone. The condition also does not specify which pair of inputs must be distinguished, nor does it require that all pairs be distinguished. It is a minimal existence condition, not a strong separation axiom.

/-- Distinguishability, generic field version. -/
def DistinguishabilityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
  ∃ x y : K, 0 < x ∧ 0 < y ∧ C x y ≠ 0

/-- **Bootstrap theorem (named-hypothesis form)**: a linearly ordered
field on which the Law of Logic is supported and which is Archimedean
and conditionally complete is canonically isomorphic to `ℝ` as an
ordered field. The Archimedean and conditional-completeness
hypotheses are the analytic content the Law of Logic does not on its
own provide; they are named here as inputs.

The conclusion is the existence of an order-preserving ring
isomorphism with `ℝ`. -/
theorem bootstrap_to_real
    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
    (_ : LogicSupported K) :
    Nonempty (K ≃+*o ℝ) :=
  ⟨LinearOrderedField.inducedOrderRingIso K ℝ⟩

What this page does not claim

Distinguishability alone forces the domain to be the real numbers. The comparison operator must distinguish all pairs of positive inputs. The framework derives Archimedean completeness from its own axioms.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DomainBootstrap.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: