Foundation Primitive Recognition Calculus Choice Principles Acomega Rat Seq

Choosing rational witnesses

In mathematics, a choice principle answers a practical question: if you know that something exists at every stage of an infinite process, can you pick all of them at once? The principle called countable choice, written ACω, says yes for processes indexed by the natural numbers 0, 1, 2, and so on. The recognition framework, which models reality as a discrete record of events, uses this principle to turn scattered facts into a single usable object.

The specific declaration acomega_rat_seq concerns rational numbers, the fractions like 1/2 or 7/3. It states: if for every natural number n there exists some rational number q satisfying a property R, then there exists a single function f that assigns to each n a rational number f(n) satisfying that property. In plainer terms, if every precision level has a rational witness, the principle assembles them into one approximation sequence. This is the exact shape needed for completeness in the framework's constructive real numbers, where each level of precision must yield a rational approximation.

The framework's machine-checked library of formal theorems proves acomega_rat_seq as a pure application of the countable choice principle. The proof does no extra work: it simply specializes the general principle to rational numbers. Consequently, the theorem's axiom footprint is empty, meaning it adds no new assumptions beyond the countable choice hypothesis it takes as input. The framework's audit system classifies this as a NAMED rung, a theorem that carries its choice cost explicitly instead of hiding it.

What the declaration does not claim is equally important. It does not prove that countable choice itself is true; that remains a hypothesis. The framework notes that full classical choice proves ACω trivially, but the point of the declaration is to measure the exact cost of the weaker principle. The theorem also does not construct the rational witnesses from nothing; it requires the premise that each level has one. Finally, it says nothing about choosing from uncountable collections, which would require a stronger choice principle.

Understanding this distinction matters because it shows how the framework handles its own foundations. Instead of assuming choice principles freely, it registers them as explicit costs attached to theorems that use them. The acomega_rat_seq declaration demonstrates that a useful construction, assembling rational approximations into a sequence, can be achieved with exactly countable choice and nothing more.

/-- ACω yields a modulus-of-witness function for rational approximation
families: the exact shape the CRealPre completeness rung consumes (from
"every precision level has a rational witness" to a single approximation
sequence). Choice-free given the hypothesis; pure application. -/
theorem acomega_rat_seq (h : ACOmega) (R : ℕ → ℚ → Prop) (hR : ∀ n, ∃ q, R n q) :
    ∃ f : ℕ → ℚ, ∀ n, R n (f n) :=
  h ℚ R hR

/-- ACω yields a modulus-of-witness function for rational approximation
families: the exact shape the CRealPre completeness rung consumes (from
"every precision level has a rational witness" to a single approximation
sequence). Choice-free given the hypothesis; pure application. -/
theorem acomega_rat_seq (h : ACOmega) (R : ℕ → ℚ → Prop) (hR : ∀ n, ∃ q, R n q) :
    ∃ f : ℕ → ℚ, ∀ n, R n (f n) :=
  h ℚ R hR

/-- The classical display layer satisfies ACω: full choice specializes to
countable choice. DELIBERATELY classical (bridge tier); this theorem is the
calibration point "ACω < Classical.choice" and must not be purified. -/
theorem classical_acomega : ACOmega := fun _X _R h =>
  ⟨fun n => Classical.choose (h n), fun n => Classical.choose_spec (h n)⟩

What this page does not claim

The declaration does not prove that countable choice itself is true. The declaration does not construct rational witnesses from nothing; it requires the premise that each level has one. The declaration says nothing about choosing from uncountable collections.

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/PrimitiveRecognitionCalculus/ChoicePrinciples.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: