Foundation Primitive Recognition Calculus Choice Principles

Choice principles

In mathematics, a choice principle is a rule that lets you pick an element from each of a collection of nonempty sets, all at once. The countable version, called ACω, applies when the collection is indexed by the natural numbers 0, 1, 2, and so on. It says: if for every natural number n there exists some x satisfying a relation R, then there is a single function f that, for each n, picks such an x. This is a classical idea, studied since the early 20th century, and it sits between weaker and stronger choice axioms.

The framework's machine-checked library of formal theorems, called the ledger (a discrete record of mathematical facts), uses ACω in a specific place. Its constructive-real completeness rungs, following the Bishop/Bridges tradition, need to convert the statement "for every precision level there is a rational witness" into a single sequence of rational approximations. The module ChoicePrinciples proves that ACω is exactly the right tool for this conversion. It shows that ACω specializes to Bool-valued relations and to rational-valued relations, producing the modulus-of-witness functions that the completeness rung consumes. These are pure applications: given the hypothesis ACω, the conclusions follow by direct instantiation.

The module also calibrates ACω against full classical choice. It proves that classical choice implies ACω, so ACω is the weaker principle. The framework's audit manifest registers this as a named class: a theorem that carries ACω as a hypothesis earns the NAMED verdict, strictly between CONDITIONAL and BRIDGE. This matters because the framework wants to know exactly which choice cost each constructive-real rung requires. The point is not that ACω is unprovable from the base; it is that ACω is not provable from the base without an explicit choice assumption, while classical choice proves it trivially.

The practical consequence is a precise accounting. When the framework builds real numbers from rational approximations, it does not silently assume full classical choice. It names the countable choice principle as a hypothesis, uses it where needed, and records the footprint. A reader can see, in the audit, that the completeness rung depends on ACω and nothing stronger. This is the kind of exact provenance the framework aims for: every constructive step carries its choice cost on its sleeve.

/-- NAMED-class canary: ACω specializes, choice-free, to `Bool`-valued
relations. The proof is pure application, so the measured axiom footprint is
empty while the statement carries `ACOmega` as a hypothesis: the audit must
report exactly the NAMED verdict on this rung. If this rung ever measures
FORCED or BRIDGE, the tag-class plumbing is broken. -/
theorem acomega_bool (h : ACOmega) :
    ∀ R : ℕ → Bool → Prop, (∀ n, ∃ b, R n b) → ∃ f : ℕ → Bool, ∀ n, R n (f n) :=
  fun R hR => h Bool 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

ACω is not provable from the base without an explicit choice assumption. The module does not prove that ACω is independent of the base; it only records that classical choice proves it trivially. The framework's real-number construction is not fully classical; it carries ACω as a named hypothesis.

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: