IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ChoicePrinciples
Isolates countable choice (ACω) as a named Prop for Type-valued ℕ-families of inhabited relations, the exact choice cost of constructive-real completeness (Bishop/Bridges). Foundation auditors cite it when scoring δ-base theorems: carrying ACω as a hypothesis earns the NAMED audit verdict. The module states the Prop choice-free, proves Classical.choice implies it, and records elementary instances on Bool and rational sequences.
claimCountable choice $\mathrm{AC}_\omega$: for every $\mathbb{N}$-indexed family of inhabited-by-witness relations on $\mathrm{Type}$-valued carriers, there is a simultaneous witness function. As a proposition it is choice-free to state; classical choice proves it. Elementary instances hold for $\mathrm{Bool}$ and for sequences of rationals.
background
In constructive analysis (Bishop/Bridges), completeness of the reals and related rungs require a controlled fragment of choice: countable choice over inhabited sets, not full AC. This module packages that fragment as a first-class Prop so Recognition foundation proofs can name their choice cost instead of smuggling it through classical axioms.
The ambient setting is the Primitive Recognition Calculus layer of the Foundation domain. The δ base is intended to stay choice-light; ACω is therefore registered as a named hypothesis class in the audit manifest. Stating ACω costs nothing constructively; proving it from the δ base is not expected, while Classical.choice discharges it immediately.
Sibling objects in the module are the Prop itself, the classical implication, and two elementary specializations (boolean carriers and rational sequences) that pin the intended strength without opening full dependent choice.
proof idea
Definition-and-interface module, not a deep proof development. The core object is a Prop asserting simultaneous witnesses for ℕ-indexed inhabited Type-relations. One theorem is a one-line classical discharge: full classical choice implies the countable fragment. Two further results instantiate the principle on Bool and on rational sequences, confirming the Prop has the expected elementary models. No forcing-chain or J-cost reasoning appears here.
why it matters in Recognition Science
Gives the Foundation audit a clean middle rung between CONDITIONAL (open hypotheses) and BRIDGE (heavier classical or analytic glue). A theorem whose only non-δ assumption is ACω earns the NAMED verdict: choice cost is explicit, localized, and the exact fragment constructive-real completeness needs. Downstream completeness and constructive-real rungs in Primitive Recognition Calculus can therefore cite ACω rather than silent classical choice, keeping the Recognition forcing chain's constructive footprint auditable. The module does not itself advance T5–T8; it polices the logical budget of proofs that will.
scope and limits
- Does not prove ACω from the δ base or any choice-free fragment.
- Does not assert full AC, dependent choice, or unique choice.
- Does not derive real-completeness or analysis theorems; only names the choice cost.
- Does not connect to J-cost, phi-ladder, or T5–T8 forcing steps.
- Does not claim the elementary Bool/rat instances exhaust all needed carriers.