acomega_rat_seq
plain-language theorem explainer
Countable choice (ACω) specializes to rational-valued witness sequences: if every natural number n has some rational q with R(n,q), then a single map f : ℕ → ℚ picks witnesses for all n at once. Anyone building constructive-real completeness (Bishop/Bridges style) cites this for the modulus-of-approximation step. The proof is a one-line instantiation of ACω at X = ℚ.
Claim. Assume countable choice over Type-valued carriers (ACω). Let $R : \mathbb{N} \to \mathbb{Q} \to \mathrm{Prop}$ be any relation such that for every $n$ there exists a rational $q$ with $R(n,q)$. Then there exists a function $f : \mathbb{N} \to \mathbb{Q}$ with $R(n, f(n))$ for all $n$.
background
This module isolates the exact choice principles needed by the primitive recognition calculus, especially the constructive-real completeness rungs. The central object is ACω: for every Type-valued carrier X and every ℕ-indexed family of relations R that is pointwise inhabited, there is a simultaneous witness function f : ℕ → X. Stating ACω is choice-free; proving it from the δ base is not. Classical choice proves it immediately (the sibling classical_acomega), which calibrates ACω as strictly weaker than full Classical.choice.
The present theorem fixes the carrier to the rationals. That is the shape consumed by CRealPre completeness: one starts from "every precision level has a rational witness" and needs a single approximation sequence. No extra structure on ℚ is used beyond it being a Type.
proof idea
One-line term proof: apply the ACω hypothesis at carrier X = ℚ, relation R, and the pointwise existence hypothesis hR. Nothing else is unfolded or rewritten.
why it matters
In the Recognition Science foundation layer this is a named-footprint specialization: theorems that carry ACω as an explicit hypothesis earn the NAMED audit verdict (between CONDITIONAL and BRIDGE). The doc-comment ties it directly to the CRealPre completeness rung, which needs a modulus-of-witness map from pointwise rational approximations to a single sequence. No downstream consumers are registered yet in the graph, so its role is interface hygiene: keep the rational case as a clean, reusable application of ACω rather than inlining the specialization at each completeness proof. It does not touch the forcing chain T0–T8, RCL, or physical constants; it is pure choice bookkeeping for constructive analysis inside the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.