Foundation Primitive Recognition Calculus Choice Principles Acomega

Countable choice as a named axiom

Countable choice is a principle of mathematics that answers a practical question: if you have an infinite, numbered list of tasks, and for each task you know at least one way to complete it, can you choose a completion for every task at once? The principle says yes, provided the list is countable, meaning it can be matched one-to-one with the natural numbers 0, 1, 2, and so on. It is weaker than the full axiom of choice, which makes the same promise for any collection of tasks, no matter how large. Countable choice appears throughout analysis, for example when building a sequence of approximations that get closer and closer to a real number.

The Recognition Science framework, a system that derives physical and mathematical structure from a ledger of recognition events, states this principle as a formal declaration named ACOmega. The declaration says: for every family of relations indexed by natural numbers, if each relation has at least one witness, then there exists a function that picks a witness for every index. In plain words, it is the countable choice principle, written as a single proposition. The framework does not prove ACOmega from its basic assumptions; it treats ACOmega as an explicit hypothesis that some theorems require. This matters because the framework audits which of its results depend on choice principles, and ACOmega is a clean way to mark that dependence.

One theorem in the framework's machine-checked library of formal theorems shows that the full classical axiom of choice, called Classical.choice, proves ACOmega trivially. That is, if you assume the full axiom, countable choice follows for free. The framework keeps this theorem deliberately classical, as a calibration point: it shows that ACOmega sits strictly below full choice in strength. Another theorem shows that ACOmega, when assumed, specializes to relations whose witnesses are just true or false, a simple case that still requires the hypothesis. A third theorem applies ACOmega to rational numbers, turning the statement "for every precision level there exists a rational approximation" into a single sequence of rational approximations, the exact shape needed for constructing real numbers constructively.

In the framework's audit system, a theorem that carries ACOmega as a hypothesis receives a verdict called NAMED, meaning its statement depends on a named choice principle but its proof itself uses no choice axioms. The point is precision: the framework can say exactly which results need countable choice and which do not. ACOmega does not claim that countable choice is provable from the framework's base assumptions, nor that it is false. It only names the principle so that dependence can be tracked honestly.

/-- **ACω**, countable choice over `Type`-valued carriers. For every ℕ-indexed
family of inhabited-by-witness relations there is a simultaneous witness
function. This is the exact choice cost expected of the constructive-real
completeness rungs (Bishop/Bridges). As a `Prop` it is choice-free to STATE;
the point is that it is not provable from the δ base, while `Classical.choice`
proves it trivially (`classical_acomega`). Registered in the audit manifest's
`[registry].named` class: a clean-footprint theorem carrying `ACOmega` as a
hypothesis earns the NAMED verdict, strictly between CONDITIONAL and BRIDGE. -/
def ACOmega : Prop :=
  ∀ (X : Type) (R : ℕ → X → Prop), (∀ n, ∃ x, R n x) → ∃ f : ℕ → X, ∀ n, R n (f n)

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

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

What this page does not claim

ACOmega is not proved from the framework's base assumptions. ACOmega is not the full axiom of choice. The framework does not claim that countable choice is false or unnecessary.

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: