IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.RealLineNonNativity

   1/-
   2  PrimitiveRecognitionCalculus/RealLineNonNativity.lean
   3
   4  The Non-Nativity of the Real Line, with teeth.
   5
   6  Audit context. The certificate layer in `CompletionConservativity.lean` and
   7  `FiniteCertificateTransfer.lean` uses an arbitrary, prover-chosen `certifies`
   8  relation with no soundness link to the predicate it certifies. Consequently
   9  `identity_conservative` makes *every* predicate "conservative," and
  10  `finite_certificate_transfer` is the identity on its hypotheses. That layer is
  11  vacuous: it cannot witness that the continuum carries non-native surplus.
  12
  13  This module supplies the missing content via a cardinality obstruction, which
  14  is *not* prover-defeatable. The doctrine "the real line is non-native" is made
  15  precise and TRUE here as: no countable finite-distinction certificate system
  16  can FAITHFULLY cover ℝ, because faithful (injective) covering forces the
  17  covered type to be countable, and ℝ is uncountable.
  18
  19  Honest scope. This is the crude (cardinality) form of the doctrine. It kills
  20  naive certificate-covering of the continuum itself. It does NOT, by itself,
  21  kill the Millennium targets whose witness sets are countable (algebraic
  22  cycles and rational Hodge classes are both countable). For those, cardinality
  23  gives no obstruction and the genuine obstruction is finer and geometric (for
  24  Hodge, the diffuse zero-Lelong residual; see
  25  `IndisputableMonolith.Mathematics.HodgeDiffuseLocalization`). That separation
  26  is itself a result: it tells you exactly when the doctrine bites by counting
  27  and when it must descend to structure.
  28
  29  No project-local axioms. No sorry.
  30-/
  31
  32import Mathlib
  33
  34namespace IndisputableMonolith
  35namespace Foundation
  36namespace PrimitiveRecognitionCalculus
  37namespace RealLineNonNativity
  38
  39/-- A faithful certificate assignment: distinct certified data receive distinct
  40certificates. This is the minimal soundness a genuine witness must satisfy — a
  41certificate that determines what it certifies. The vacuous layer drops exactly
  42this condition. -/
  43def Faithful {D Cert : Type} (assign : D → Cert) : Prop :=
  44  Function.Injective assign
  45
  46/-- A faithful cover into a countable certificate system forces the covered type
  47to be countable. -/
  48theorem faithful_cover_into_countable_imp_countable
  49    {W Cert : Type} [Countable Cert] (assign : W → Cert) (h : Faithful assign) :
  50    Countable W := by
  51  have hinj : Function.Injective assign := h
  52  rw [← Cardinal.mk_le_aleph0_iff]
  53  have h1 : Cardinal.mk W ≤ Cardinal.mk Cert := Cardinal.mk_le_of_injective hinj
  54  have h2 : Cardinal.mk Cert ≤ Cardinal.aleph0 := Cardinal.mk_le_aleph0
  55  exact le_trans h1 h2
  56
  57/-- **Cardinality obstruction.** A countable certificate system cannot faithfully
  58cover an uncountable display type: faithful covering would force the display type
  59to be countable. -/
  60theorem no_faithful_cover_of_uncountable
  61    {D Cert : Type} [Countable Cert] (hD : ¬ Countable D) (assign : D → Cert) :
  62    ¬ Faithful assign :=
  63  fun hinj => hD (faithful_cover_into_countable_imp_countable assign hinj)
  64
  65/-- ℝ is uncountable (its cardinality is the continuum, strictly above ℵ₀). -/
  66theorem real_uncountable : ¬ Countable ℝ := by
  67  rw [← Cardinal.mk_le_aleph0_iff, Cardinal.mk_real]
  68  exact not_le.mpr Cardinal.aleph0_lt_continuum
  69
  70/-- **The Non-Nativity of the Real Line (cardinality form).** No countable
  71finite-distinction certificate system faithfully covers the real line. The
  72continuum carries surplus that no countable distinction protocol can witness;
  73ℝ enters only through a completion interface, not from distinction alone. -/
  74theorem real_not_faithfully_certifiable
  75    {Cert : Type} [Countable Cert] (assign : ℝ → Cert) :
  76    ¬ Faithful assign :=
  77  no_faithful_cover_of_uncountable real_uncountable assign
  78
  79/-- **Honest refinement: countable witnesses escape the cardinality weapon.** Any
  80countable witness type admits a faithful certificate assignment into ℕ. So when
  81the true witnesses are countable — as for algebraic cycles and rational Hodge
  82classes — cardinality gives no obstruction, and any genuine obstruction must be
  83finer than counting (for Hodge: the geometric diffuse residual). -/
  84theorem countable_witness_has_faithful_cover
  85    {W : Type} [Countable W] : ∃ assign : W → ℕ, Faithful assign := by
  86  obtain ⟨f, hf⟩ := exists_injective_nat W
  87  exact ⟨f, hf⟩
  88
  89/-- The dividing line: a faithful cover into a countable system exists iff the
  90witness type is countable. This is exactly the boundary between where the
  91cardinality form of the doctrine bites (uncountable witnesses) and where it does
  92not (countable witnesses, needing a finer geometric obstruction). -/
  93theorem faithful_cover_into_countable_iff_countable
  94    {W : Type} :
  95    (∃ assign : W → ℕ, Faithful assign) ↔ Countable W := by
  96  constructor
  97  · rintro ⟨assign, h⟩
  98    exact faithful_cover_into_countable_imp_countable assign h
  99  · intro hW
 100    exact countable_witness_has_faithful_cover
 101
 102end RealLineNonNativity
 103end PrimitiveRecognitionCalculus
 104end Foundation
 105end IndisputableMonolith
 106