IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.ChoicePrinciples

   1/-
   2  PrimitiveRecognitionCalculus/ChoicePrinciples.lean
   3
   4  The NAMED choice principles: the second registry class of the Delta Forcing
   5  Spectrum audit, alongside the omniscience posits (`Omniscience.lean`).
   6
   7  The omniscience principles (LPO, WLPO, LLPO, MP) are DECISION principles:
   8  they decide Sigma-0-1 data that no finite distinction certificate can decide.
   9  Countable choice is a different kind of commitment: a FUNCTION-EXISTENCE
  10  principle. From "every index has a witness" it manufactures a single
  11  simultaneous witness function. The delta base cannot force it (there is no
  12  finite certificate for an infinite simultaneous selection), but it is far
  13  weaker than full `Classical.choice`: it neither decides anything (no excluded
  14  middle) nor chooses over uncountable families.
  15
  16  Why it gets its own registry class instead of joining the posits: the audit's
  17  CONDITIONAL verdict means "constructive modulo a named omniscience decision".
  18  The NAMED verdict means "constructive modulo a named choice principle". The
  19  constructive-real ladder (M0a: eta : Q_delta -> R_delta over Bishop-regular
  20  sequences) is expected to cost exactly AC_omega at the completeness rungs, and
  21  the ledger must be able to say that precisely, not launder it as BRIDGE
  22  (full classical) or overclaim it as FORCED.
  23
  24  Everything here except `classical_acomega` is choice-free. `classical_acomega`
  25  is DELIBERATELY classical (it is the statement that the display layer
  26  satisfies AC_omega); it is bridge-tier by design and must not be "purified".
  27
  28  No project-local axioms. No sorry.
  29-/
  30
  31import Mathlib
  32
  33namespace IndisputableMonolith
  34namespace Foundation
  35namespace PrimitiveRecognitionCalculus
  36namespace ChoicePrinciples
  37
  38/-- **ACω**, countable choice over `Type`-valued carriers. For every ℕ-indexed
  39family of inhabited-by-witness relations there is a simultaneous witness
  40function. This is the exact choice cost expected of the constructive-real
  41completeness rungs (Bishop/Bridges). As a `Prop` it is choice-free to STATE;
  42the point is that it is not provable from the δ base, while `Classical.choice`
  43proves it trivially (`classical_acomega`). Registered in the audit manifest's
  44`[registry].named` class: a clean-footprint theorem carrying `ACOmega` as a
  45hypothesis earns the NAMED verdict, strictly between CONDITIONAL and BRIDGE. -/
  46def ACOmega : Prop :=
  47  ∀ (X : Type) (R : ℕ → X → Prop), (∀ n, ∃ x, R n x) → ∃ f : ℕ → X, ∀ n, R n (f n)
  48
  49/-- The classical display layer satisfies ACω: full choice specializes to
  50countable choice. DELIBERATELY classical (bridge tier); this theorem is the
  51calibration point "ACω < Classical.choice" and must not be purified. -/
  52theorem classical_acomega : ACOmega := fun _X _R h =>
  53  ⟨fun n => Classical.choose (h n), fun n => Classical.choose_spec (h n)⟩
  54
  55/-- NAMED-class canary: ACω specializes, choice-free, to `Bool`-valued
  56relations. The proof is pure application, so the measured axiom footprint is
  57empty while the statement carries `ACOmega` as a hypothesis: the audit must
  58report exactly the NAMED verdict on this rung. If this rung ever measures
  59FORCED or BRIDGE, the tag-class plumbing is broken. -/
  60theorem acomega_bool (h : ACOmega) :
  61    ∀ R : ℕ → Bool → Prop, (∀ n, ∃ b, R n b) → ∃ f : ℕ → Bool, ∀ n, R n (f n) :=
  62  fun R hR => h Bool R hR
  63
  64/-- ACω yields a modulus-of-witness function for rational approximation
  65families: the exact shape the CRealPre completeness rung consumes (from
  66"every precision level has a rational witness" to a single approximation
  67sequence). Choice-free given the hypothesis; pure application. -/
  68theorem acomega_rat_seq (h : ACOmega) (R : ℕ → ℚ → Prop) (hR : ∀ n, ∃ q, R n q) :
  69    ∃ f : ℕ → ℚ, ∀ n, R n (f n) :=
  70  h ℚ R hR
  71
  72end ChoicePrinciples
  73end PrimitiveRecognitionCalculus
  74end Foundation
  75end IndisputableMonolith
  76