IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.FiniteCertificateTransfer

   1/-
   2  PrimitiveRecognitionCalculus/FiniteCertificateTransfer.lean
   3
   4  The finite-certificate transfer theorem.
   5
   6  This is the hinge requested by the Delta-native analysis plan. A continuum
   7  display statement is legitimate only when it is certificate-covered by typed
   8  finite distinction data. If the completion is conservative, continuum
   9  obstructions descend to finite certificates.
  10
  11  HONEST-LAYER UPGRADE (2026-06-01). The original `ConservativeFor` /
  12  `finite_certificate_transfer` notion below is a WEAK baseline: its `certifies`
  13  relation is prover-chosen with no soundness, so `identity_conservative` makes
  14  every predicate "conservative" and `finite_certificate_transfer` is the
  15  identity on its hypotheses. That layer cannot witness that the continuum
  16  carries non-native surplus. We retain it for downstream compatibility but add
  17  the honest notion `SoundFaithfulCover`, which requires:
  18
  19    * coverage   : every witness of `P` carries a certificate;
  20    * soundness  : `certifies c d → P d` (no certificate is issued to a non-witness);
  21    * faithfulness: a certificate determines its datum.
  22
  23  Faithfulness is exactly the condition the weak layer drops, and it blocks the
  24  vacuity trick (`everything_certified_not_faithful`). With it, a sound faithful
  25  cover injects the witness set into the certificate type, so a countable
  26  certificate system cannot cover an uncountable witness family
  27  (`no_soundFaithfulCover_of_uncountable_witnesses`), with the real line as the
  28  named instance (`no_sound_faithful_certification_of_reals`). The cardinality
  29  obstruction is not prover-defeatable.
  30
  31  No project-local axioms. No sorry.
  32-/
  33
  34import Mathlib
  35import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity
  36
  37namespace IndisputableMonolith
  38namespace Foundation
  39namespace PrimitiveRecognitionCalculus
  40namespace FiniteCertificateTransfer
  41
  42open CompletionConservativity
  43
  44/-- A typed finite distinction certificate: finite data together with a tag
  45describing which distinction regime produced it. -/
  46structure TypedFiniteDistinction (Tag : Type*) where
  47  size : ℕ
  48  tag : Tag
  49
  50/-- A certificate map for a display predicate. -/
  51structure CertificateMap (Tag D : Type*) (P : D → Prop) where
  52  cert : D → TypedFiniteDistinction Tag
  53  sound : ∀ d : D, P d → True
  54
  55/-- Continuum statement legitimacy: every display witness of `P` has a finite
  56typed distinction certificate. -/
  57def LegitimateContinuumStatement (Tag D : Type*) (P : D → Prop) : Prop :=
  58  ∀ d : D, P d → Nonempty (TypedFiniteDistinction Tag)
  59
  60theorem certificateMap_legitimate {Tag D : Type*} {P : D → Prop}
  61    (M : CertificateMap Tag D P) : LegitimateContinuumStatement Tag D P := by
  62  intro d hP
  63  exact ⟨M.cert d⟩
  64
  65/-- If a completion is conservative for a display predicate, every display
  66predicate witness descends to a finite certificate. -/
  67theorem conservative_completion_transfers
  68    {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop)
  69    (hC : ConservativeFor C P) :
  70    ∀ d : D, P d → ∃ c : Cert, C.certifies c d :=
  71  hC
  72
  73/-- If an obstruction predicate is conservative, then every continuum obstruction
  74has a finite certificate. -/
  75theorem obstruction_descends
  76    {N D Cert : Type*} (C : Completion N D Cert) (Obstruction : D → Prop)
  77    (hC : ConservativeFor C Obstruction) :
  78    ∀ d : D, Obstruction d → ∃ c : Cert, C.certifies c d :=
  79  hC
  80
  81/-- **Finite-certificate transfer headline.** For a conservative completion,
  82valid continuum witnesses and valid continuum obstructions both descend to finite
  83certificates. This is the formal hinge behind the quantized-proof method. -/
  84theorem finite_certificate_transfer
  85    {N D Cert : Type*} (C : Completion N D Cert) (P Obstruction : D → Prop)
  86    (hP : ConservativeFor C P) (hO : ConservativeFor C Obstruction) :
  87    (∀ d : D, P d → ∃ c : Cert, C.certifies c d)
  88      ∧ (∀ d : D, Obstruction d → ∃ c : Cert, C.certifies c d) :=
  89  ⟨conservative_completion_transfers C P hP, obstruction_descends C Obstruction hO⟩
  90
  91/-! ## The honest layer: sound, faithful certificate covers
  92
  93The weak notion above is prover-defeatable. The notion below is not. -/
  94
  95/-- A **sound, faithful** certificate cover for a display predicate `P` over a
  96completion `C`. Three conditions, the third of which the weak layer drops:
  97* `complete`  : every witness of `P` carries a certificate;
  98* `sound`     : a certificate is issued only to genuine witnesses (`certifies c d → P d`);
  99* `faithful`  : a certificate determines the datum it certifies. -/
 100structure SoundFaithfulCover {N D Cert : Type} (C : Completion N D Cert) (P : D → Prop) : Prop where
 101  complete : ∀ d, P d → ∃ c, C.certifies c d
 102  sound : ∀ c d, C.certifies c d → P d
 103  faithful : ∀ c d₁ d₂, C.certifies c d₁ → C.certifies c d₂ → d₁ = d₂
 104
 105/-- The vacuity-defeating fact. A completion that "certifies everything" (the
 106trick that made the weak layer vacuous) cannot be faithful as soon as the
 107display type has two distinct points. So a `SoundFaithfulCover` is genuinely
 108constrained. -/
 109theorem everything_certified_not_faithful
 110    {N D Cert : Type} (C : Completion N D Cert)
 111    (htriv : ∀ c d, C.certifies c d) (c0 : Cert)
 112    {d₁ d₂ : D} (hne : d₁ ≠ d₂) :
 113    ¬ (∀ c d₁ d₂, C.certifies c d₁ → C.certifies c d₂ → d₁ = d₂) :=
 114  fun hfaith => hne (hfaith c0 d₁ d₂ (htriv c0 d₁) (htriv c0 d₂))
 115
 116/-- A sound, faithful cover injects the witness set into the certificate type. -/
 117theorem soundFaithfulCover_injects
 118    {N D Cert : Type} {C : Completion N D Cert} {P : D → Prop}
 119    (cover : SoundFaithfulCover C P) :
 120    ∃ f : {d // P d} → Cert, Function.Injective f := by
 121  classical
 122  refine ⟨fun w => Classical.choose (cover.complete w.1 w.2), ?_⟩
 123  intro w₁ w₂ hfeq
 124  have h1 : C.certifies (Classical.choose (cover.complete w₁.1 w₁.2)) w₁.1 :=
 125    Classical.choose_spec (cover.complete w₁.1 w₁.2)
 126  have h2 : C.certifies (Classical.choose (cover.complete w₂.1 w₂.2)) w₂.1 :=
 127    Classical.choose_spec (cover.complete w₂.1 w₂.2)
 128  have hc : Classical.choose (cover.complete w₁.1 w₁.2)
 129            = Classical.choose (cover.complete w₂.1 w₂.2) := hfeq
 130  rw [hc] at h1
 131  exact Subtype.ext (cover.faithful _ _ _ h1 h2)
 132
 133/-- **Honest hinge.** A sound, faithful certificate cover by a countable
 134certificate system forces the witness set to be countable. -/
 135theorem soundFaithfulCover_countable_witnesses
 136    {N D Cert : Type} [Countable Cert] {C : Completion N D Cert} {P : D → Prop}
 137    (cover : SoundFaithfulCover C P) :
 138    Countable {d // P d} := by
 139  obtain ⟨f, hf⟩ := soundFaithfulCover_injects cover
 140  rw [← Cardinal.mk_le_aleph0_iff]
 141  exact le_trans (Cardinal.mk_le_of_injective hf) Cardinal.mk_le_aleph0
 142
 143/-- **Cardinality obstruction.** No sound, faithful certificate cover by a
 144countable certificate system exists for a predicate with uncountably many
 145witnesses. This is the honest content the weak layer could not deliver. -/
 146theorem no_soundFaithfulCover_of_uncountable_witnesses
 147    {N D Cert : Type} [Countable Cert] {C : Completion N D Cert} {P : D → Prop}
 148    (hunc : ¬ Countable {d // P d}) (cover : SoundFaithfulCover C P) : False :=
 149  hunc (soundFaithfulCover_countable_witnesses cover)
 150
 151/-- The witnesses of the always-true predicate on ℝ are uncountable. -/
 152theorem reals_uncountable_witnesses : ¬ Countable {_x : ℝ // True} := by
 153  intro h
 154  haveI := h
 155  have hinj : Function.Injective (fun x : ℝ => (⟨x, trivial⟩ : {_x : ℝ // True})) :=
 156    fun a b hab => congrArg Subtype.val hab
 157  have hRcount : Countable ℝ := by
 158    rw [← Cardinal.mk_le_aleph0_iff]
 159    exact le_trans (Cardinal.mk_le_of_injective hinj) Cardinal.mk_le_aleph0
 160  rw [← Cardinal.mk_le_aleph0_iff, Cardinal.mk_real] at hRcount
 161  exact (not_le.mpr Cardinal.aleph0_lt_continuum) hRcount
 162
 163/-- **Named instance: the real line.** No sound, faithful certificate cover by a
 164countable certificate system exists for the real line. Finite distinction data
 165cannot soundly and faithfully certify the continuum. -/
 166theorem no_sound_faithful_certification_of_reals
 167    {N Cert : Type} [Countable Cert] (C : Completion N ℝ Cert)
 168    (cover : SoundFaithfulCover C (fun _ : ℝ => True)) : False :=
 169  no_soundFaithfulCover_of_uncountable_witnesses reals_uncountable_witnesses cover
 170
 171end FiniteCertificateTransfer
 172end PrimitiveRecognitionCalculus
 173end Foundation
 174end IndisputableMonolith
 175