acomega_bool
plain-language theorem explainer
Countable choice ACω specializes, without extra axioms, to Bool-valued relations: any ℕ-indexed family of nonempty Bool-predicates admits a simultaneous choice function once ACω is assumed. Audit authors and constructive-analysis writers cite it as the NAMED-class canary for the choice-principles registry. The proof is pure specialization of the general ACω hypothesis at the carrier Bool.
Claim. Assume countable choice $\mathrm{AC}_\omega$. Then for every relation $R:\mathbb{N}\to\mathrm{Bool}\to\mathrm{Prop}$ such that $\forall n,\,\exists b,\, R\,n\,b$, there exists $f:\mathbb{N}\to\mathrm{Bool}$ with $\forall n,\, R\,n\,(f\,n)$.
background
In this module, $\mathrm{AC}\omega$ is the Prop asserting countable choice over arbitrary Type carriers: for every type $X$ and every $\mathbb{N}$-indexed family of inhabited-by-witness relations $R:n\mapsto X$, there is a simultaneous witness function $f:\mathbb{N}\to X$. Stating $\mathrm{AC}\omega$ costs no choice; proving it does. Classical choice yields it immediately (the sibling calibration theorem), while the $\delta$ base does not.
The local setting is the Primitive Recognition Calculus choice ladder. Bool is the simplest nontrivial discrete carrier, so specializing $\mathrm{AC}\omega$ here is the cleanest probe of how the audit tags a theorem that carries $\mathrm{AC}\omega$ only as a named hypothesis. Downstream, the same pattern is applied to rational approximation families that feed constructive-real completeness rungs.
proof idea
One-line term proof. The hypothesis $h:\mathrm{AC}_\omega$ is already quantified over every Type carrier. Instantiate it at $X=\mathrm{Bool}$, pass the given relation $R$ and the pointwise existence hypothesis, and return the resulting choice function. No lemmas, no classical axioms, no rewriting: pure application.
why it matters
This is the NAMED-class canary for the audit manifest's choice registry. The doc-comment states the contract explicitly: the measured axiom footprint must stay empty while the statement carries $\mathrm{AC}_\omega$ as a hypothesis, so the audit reports exactly NAMED (strictly between CONDITIONAL and BRIDGE). If the rung ever measures FORCED or BRIDGE, the tag-class plumbing is broken.
In the Recognition foundation it anchors the choice cost expected of constructive-real completeness (Bishop/Bridges style). The sibling specialization to rational approximation sequences is the exact shape those completeness rungs consume: from "every precision level has a rational witness" to a single approximation sequence. No downstream consumers are wired yet in the graph, but the declaration exists to keep the choice ledger honest before those rungs close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.