ACOmega
plain-language theorem explainer
Countable choice (ACω) as a bare proposition: every ℕ-indexed family of inhabited Type-valued relations admits a simultaneous witness sequence. Cited by anyone tracking the exact choice cost of constructive-real completeness rungs (Bishop/Bridges style). The body is a pure Prop abbreviation, not a proof; Classical.choice discharges it, while the δ base does not.
Claim. The proposition $\mathrm{AC}_\omega$ asserts: for every type $X$ and every relation $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
This module isolates choice principles used by the primitive recognition calculus, separating what the constructive δ-layer can state from what only the classical display bridge can prove. $\mathrm{AC}_\omega$ is countable choice over arbitrary Type carriers: from a countable family of existential witnesses one extracts a single selection function.
As a proposition it is choice-free to write down. The Recognition audit treats it as a named hypothesis class: theorems that assume it (and add no further axioms) earn the NAMED verdict, strictly between CONDITIONAL and BRIDGE. The constructive-real completeness path (CRealPre-style rational approximation sequences) is the intended consumer; Bishop/Bridges completeness is the classical reference for this exact strength.
Full classical choice specializes to $\mathrm{AC}_\omega$ immediately. The δ base is not expected to prove it.
proof idea
There is no proof: the declaration is a def equating the name to the universal Prop above. Discharge happens downstream. The classical bridge proves the proposition by applying Classical.choose and Classical.choice_spec pointwise on each $n$. Specializations to Bool and to $\mathbb{Q}$ are pure applications of the hypothesis, adding no axioms.
why it matters
Registers the exact choice cost expected of constructive-real completeness rungs inside the Recognition foundation. Downstream, classical_acomega is the deliberate bridge-tier calibration point "$\mathrm{AC}\omega <$ Classical.choice" and must stay classical. The canaries acomega_bool and acomega_rat_seq are pure applications: empty axiom footprint while carrying $\mathrm{AC}\omega$ as hypothesis, so the audit must report NAMED. The rational-sequence form is the shape CRealPre completeness consumes (from "every precision has a rational witness" to one approximation sequence). In the audit manifest's named class, a clean-footprint theorem with this hypothesis sits strictly between CONDITIONAL and BRIDGE.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.