Foundation Domain Bootstrap Real Supports Logic

The bootstrap theorem

The real numbers are the unique ordered number system that is both Archimedean and Dedekind-complete: every bounded set has a least upper bound, and no infinitely large or infinitesimally small elements exist. This classical characterization, a standard result in analysis, is the backdrop for a theorem in the Recognition Science framework's machine-checked library of formal theorems. The theorem, called real_supports_logic, establishes that the real numbers themselves can serve as the domain for the framework's fundamental comparison operator, the basic two-input operation from which the framework derives its cost function.

The framework's central law of logic is stated using a comparison operator that takes two positive real numbers and returns a third. The framework also derives its own copy of the real numbers, called LogicReal, from that same law. This creates a potential circularity: the law is stated over the real numbers, but the real numbers are supposed to be derived from the law. The declaration real_supports_logic resolves this by showing that the real numbers satisfy the conditions needed to support the law, namely the four Aristotelian conditions of identity, non-contradiction, scale invariance, and distinguishability, along with the order-theoretic property that 0 is less than 1.

The significance is a uniqueness result. A separate theorem in the same module, bootstrap_to_real, proves that any linearly ordered field on which the law of logic is supported, and which is also Archimedean and conditionally complete, is canonically isomorphic to the real numbers. This means the choice of the real numbers as the domain for the comparison operator is not arbitrary; it is forced up to isomorphism by the law itself, provided the ambient field has the standard analytic completeness properties. The framework's own recovered real line, LogicReal, is then isomorphic to the ambient real numbers, closing the loop.

In Recognition Science, this bootstrap closure is what makes the framework's starting point coherent: the law of logic does not float free of a number system; it requires a specific one, and that one is the real numbers. The declaration real_supports_logic is the concrete witness that the real numbers do indeed support the law, making the entire edifice self-consistent rather than circular.

/-- **Idempotence**: `ℝ` itself is a Logic-supported domain (witnessed
by any of the comparison operators we already have over `ℝ`). The
bootstrap theorem then says nothing new on `ℝ`, but on any other
candidate ordered field it forces an isomorphism to `ℝ`. -/
def real_supports_logic
    (C : LogicAsFunctionalEquation.ComparisonOperator)
    (h : LogicAsFunctionalEquation.SatisfiesLawsOfLogic C) :
    LogicSupported ℝ where
  zero_lt_one_in_K := by norm_num
  C := C
  identity := h.identity
  non_contradiction := h.non_contradiction
  scale_invariant := h.scale_invariant
  distinguishability :=
    LogicAsFunctionalEquation.distinguishability_of_nonTrivial C h.non_trivial

/-- **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 ℝ⟩

/-- **Bootstrap closure**: the Law of Logic plus Archimedean
completeness uniquely picks out `ℝ` as the ambient ordered field, up
to canonical isomorphism. -/
theorem bootstrap_closure
    (K : Type*) [ConditionallyCompleteLinearOrderedField K]
    (h : LogicSupported K) :
    Nonempty (K ≃+*o ℝ) :=
  bootstrap_to_real K h

What this page does not claim

The declaration does not prove that the real numbers are the only possible domain for the law of logic without the Archimedean and completeness hypotheses. The declaration does not derive the Archimedean or Dedekind-completeness properties from the law of logic itself; these are named as residual analytic inputs. The declaration does not establish that the framework's cost function or other derived structures are unique or physically realized.

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: