Foundation Domain Bootstrap

The bootstrap theorem

The real numbers, ℝ, are the complete ordered number line used throughout mathematics. A key classical fact is that they are essentially the only such structure: any ordered field that is both Archimedean (no infinitely large or small elements) and Dedekind-complete (every bounded set has a least upper bound) is isomorphic to the reals. This characterization, part of standard analysis, is the foundation for what follows.

In Recognition Science, the framework begins with a comparison operator, a function that takes two positive numbers and returns a third, used to measure the cost of distinguishing them. The framework's core law, the Law of Logic, states that any such operator satisfying four plain conditions must equal a specific formula. However, this law is stated over an ambient field, and the framework does not simply assume that field is ℝ. This creates a chicken-and-egg problem: the framework derives the real line from its own logic, but it needs the real line to state that logic in the first place.

The bootstrap theorem resolves this circularity. It proves that if any linearly ordered field supports a comparison operator satisfying the Law of Logic, and if that field is also Archimedean and Dedekind-complete, then it is canonically isomorphic to ℝ. In plain terms, the framework's logic cannot live on the rationals or any other incomplete number system; the very act of stating its fundamental law, combined with the standard analytic completeness, forces the ambient field to be the real numbers. This is a theorem in the framework's machine-checked library of formal theorems, not an assumption.

The theorem also shows the process is idempotent. Starting from ℝ as the ambient field, the framework recovers an isomorphic copy of ℝ from within. Conversely, any other field that could support the logic is shown to be ℝ in disguise. The choice of ℝ as the domain for the comparison operator is therefore a canonical choice, up to isomorphism, not a contingent one. The single residual classical input is the Archimedean completeness of the field, which the Law of Logic on its own does not provide; this input is named explicitly rather than hidden.

What this establishes is that the framework's foundation is not circular in a problematic way. The framework does not need to invent its own number system from nothing; it shows that its logic, plus a standard analytic hypothesis, uniquely picks out the familiar real numbers. This closes the loop and allows the rest of the framework, including the derivation of the golden ratio and the eight-tick cycle, to proceed on solid ground.

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

/-- **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 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 bootstrap theorem does not prove that the Law of Logic alone, without the Archimedean and completeness hypotheses, forces the field to be ℝ. This module does not derive the specific form of the cost function J(x); that is established elsewhere. The theorem does not claim that the framework's logic is independent of classical analysis, as it explicitly relies on the standard characterization of ℝ.

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: