classical_acomega
plain-language theorem explainer
Countable choice (ACω) holds in the classical display layer: full choice specializes to a simultaneous witness along any ℕ-indexed inhabited family. Foundation auditors and constructive-real completeness work cite it as the calibration point that ACω is strictly weaker than Classical.choice. The proof is a short term that applies Classical.choose pointwise and packages the specs.
Claim. Classically, for every type $X$ and every family of relations $R:\mathbb{N}\to X\to\mathrm{Prop}$, if $\forall n\,\exists x\, R(n,x)$, then there exists $f:\mathbb{N}\to X$ with $\forall n\, R(n,f(n))$.
background
ACω is countable choice over Type-valued carriers: given an ℕ-indexed family of relations on a type $X$, each inhabited by some witness, there is one function $f:\mathbb{N}\to X$ that hits a witness at every index. The statement itself is choice-free to write down; what matters is its proof cost.
In the Primitive Recognition Calculus choice module this is the exact choice strength expected of Bishop/Bridges constructive-real completeness rungs. It sits in the audit registry as a NAMED hypothesis class: theorems that assume ACω cleanly, without smuggling full classical choice, earn a verdict strictly between CONDITIONAL and BRIDGE.
The classical display layer is allowed to use Mathlib's Classical.choice. This declaration records that full choice immediately yields ACω, and is deliberately kept classical as a bridge-tier calibration marker.
proof idea
Term-mode proof. Fix carrier $X$, relation family $R$, and the hypothesis $h$ that every index is inhabited. Build the choice function by $n \mapsto \mathrm{Classical.choose}(h, n)$ and discharge the pointwise specs with $\mathrm{Classical.choose_spec}(h, n)$. Package the pair as the existential witness required by ACω. No intermediate lemmas; pure specialization of full choice to the countable case.
why it matters
This is the deliberate classical calibration point "ACω < Classical.choice" in the Recognition foundation audit. It must not be purified: its job is to show that the classical display layer satisfies countable choice, while the δ-base does not prove ACω on its own.
Downstream, clean-footprint theorems that carry ACω only as a named hypothesis (for example Bool-valued or rational-sequence specializations in the same module) are scored NAMED rather than BRIDGE. That separation keeps constructive-real completeness rungs honest about their choice cost without collapsing them into full classical choice.
No parent theorem currently depends on this declaration in the graph; it is infrastructure for the choice-audit ladder rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.