Foundation Primitive Recognition Calculus Choice Principles Acomega Bool

A choice principle for two-valued questions

In mathematics, a choice principle says when you can pick one element from each of a collection of sets. The principle called countable choice, written ACω, applies to a list of sets indexed by the natural numbers 0, 1, 2, and so on. If each set in the list is known to contain at least one element, ACω guarantees a single function that picks one element from every set at once. The declaration acomega_bool is a formal theorem in the framework's machine-checked library of formal theorems. It shows that ACω, when it is assumed, also covers the special case where every set has exactly two possible answers, like yes or no, true or false.

The theorem states the matter precisely. Suppose for each natural number n there is a relation R that pairs n with either of the two boolean values, and suppose for every n at least one boolean value satisfies R. Then ACω produces a function f that assigns to each n a boolean value such that R n (f n) holds. The proof is a single line: it applies the full countable choice principle to the boolean type. The declaration is a theorem with a hypothesis, not an unconditional result. It does not prove that countable choice itself is true. It only proves that the boolean case follows from the general case.

The framework's library uses this theorem as a calibration point. Its audit system classifies theorems by how much they assume. A theorem that carries ACω as a hypothesis and adds nothing else earns the NAMED verdict, which sits between a conditional result and a bridge between theories. The boolean theorem is a canary: if the audit ever reported it as something stronger, the classification machinery would be broken. The theorem also matters for the framework's treatment of real numbers. A companion result, acomega_rat_seq, converts the statement "every precision level has a rational witness" into a single sequence of rational approximations, the exact shape a completeness construction consumes.

The theorem does not claim that ACω is provable from the framework's base assumptions. The library states plainly that full classical choice proves ACω trivially, and that ACω itself is not provable from the δ base. The boolean theorem inherits that status: it is a conditional statement, useful for measuring what a construction needs, not a proof that the needed choice exists. What the declaration establishes is a precise logical bridge: two-valued choice follows from countable choice, nothing more and nothing less.

/-- 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

/-- 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

/-- 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

What this page does not claim

The theorem does not prove that countable choice itself is true. The theorem does not show that the boolean case holds without assuming ACω.

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: