IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.CompletionConservativity

   1/-
   2  PrimitiveRecognitionCalculus/CompletionConservativity.lean
   3
   4  Completion as interface, not ontology.
   5
   6  A completion is conservative when every true display predicate descends to a
   7  native certificate. A completion creates artifacts when a display predicate has
   8  no native certificate.
   9
  10  This is the formal control layer behind the slogan: continuity is completed
  11  distinction.
  12
  13  No project-local axioms. No sorry.
  14-/
  15
  16import Mathlib
  17
  18namespace IndisputableMonolith
  19namespace Foundation
  20namespace PrimitiveRecognitionCalculus
  21namespace CompletionConservativity
  22
  23/-- A completion interface from native data `N` to display data `D`, with
  24certificates `Cert` for display predicates `P`. -/
  25structure Completion (N D Cert : Type*) where
  26  display : N → D
  27  certifies : Cert → D → Prop
  28
  29/-- A display predicate is certificate-covered when every display datum satisfying
  30it carries a finite/native certificate. -/
  31def CertificateCovered {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) : Prop :=
  32  ∀ d : D, P d → ∃ c : Cert, C.certifies c d
  33
  34/-- A completion is conservative for a predicate when the predicate is certificate-covered. -/
  35def ConservativeFor {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) : Prop :=
  36  CertificateCovered C P
  37
  38/-- A non-native artifact is a display datum satisfying a predicate but carrying no certificate. -/
  39def ArtifactFor {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) : Prop :=
  40  ∃ d : D, P d ∧ ¬ ∃ c : Cert, C.certifies c d
  41
  42theorem conservative_iff_no_artifact {N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) :
  43    ConservativeFor C P ↔ ¬ ArtifactFor C P := by
  44  unfold ConservativeFor CertificateCovered ArtifactFor
  45  constructor
  46  · intro h hc
  47    rcases hc with ⟨d, hP, hno⟩
  48    exact hno (h d hP)
  49  · intro h d hP
  50    by_contra hno
  51    exact h ⟨d, hP, hno⟩
  52
  53/-- Identity completion is conservative whenever the predicate itself supplies a
  54certificate. This is the base case for certificate-preserving completions. -/
  55def identityCompletion (N : Type*) : Completion N N N where
  56  display := id
  57  certifies := fun c d => c = d
  58
  59theorem identity_conservative (N : Type*) (P : N → Prop) :
  60    ConservativeFor (identityCompletion N) P := by
  61  intro d _
  62  exact ⟨d, rfl⟩
  63
  64/-- Product of two completion interfaces. Certificates pair component
  65certificates. -/
  66def productCompletion {N₁ D₁ Cert₁ N₂ D₂ Cert₂ : Type*}
  67    (C₁ : Completion N₁ D₁ Cert₁) (C₂ : Completion N₂ D₂ Cert₂) :
  68    Completion (N₁ × N₂) (D₁ × D₂) (Cert₁ × Cert₂) where
  69  display := fun n => (C₁.display n.1, C₂.display n.2)
  70  certifies := fun c d => C₁.certifies c.1 d.1 ∧ C₂.certifies c.2 d.2
  71
  72/-- Product predicates from component predicates. -/
  73def ProductPredicate {D₁ D₂ : Type*} (P₁ : D₁ → Prop) (P₂ : D₂ → Prop) : D₁ × D₂ → Prop :=
  74  fun d => P₁ d.1 ∧ P₂ d.2
  75
  76/-- Conservative completions compose across products: if each component display
  77predicate descends to a certificate, the product predicate descends to paired
  78certificates. -/
  79theorem product_conservative
  80    {N₁ D₁ Cert₁ N₂ D₂ Cert₂ : Type*}
  81    (C₁ : Completion N₁ D₁ Cert₁) (C₂ : Completion N₂ D₂ Cert₂)
  82    (P₁ : D₁ → Prop) (P₂ : D₂ → Prop)
  83    (h₁ : ConservativeFor C₁ P₁) (h₂ : ConservativeFor C₂ P₂) :
  84    ConservativeFor (productCompletion C₁ C₂) (ProductPredicate P₁ P₂) := by
  85  intro d hd
  86  rcases hd with ⟨hP₁, hP₂⟩
  87  rcases h₁ d.1 hP₁ with ⟨c₁, hc₁⟩
  88  rcases h₂ d.2 hP₂ with ⟨c₂, hc₂⟩
  89  exact ⟨(c₁, c₂), ⟨hc₁, hc₂⟩⟩
  90
  91/-- **Completion conservativity headline.** A completion is conservative exactly
  92when it has no uncertified display artifacts; the identity completion is
  93conservative for every predicate. -/
  94theorem completion_conservativity_headline (N D Cert : Type*) (C : Completion N D Cert) :
  95    (∀ P : D → Prop, ConservativeFor C P ↔ ¬ ArtifactFor C P)
  96      ∧ (∀ P : N → Prop, ConservativeFor (identityCompletion N) P) :=
  97  ⟨fun P => conservative_iff_no_artifact C P, identity_conservative N⟩
  98
  99/-- **Product completion headline.** Certificate-preserving completion is stable
 100under products, so multi-field display objects can be certified componentwise. -/
 101theorem product_completion_headline
 102    {N₁ D₁ Cert₁ N₂ D₂ Cert₂ : Type*}
 103    (C₁ : Completion N₁ D₁ Cert₁) (C₂ : Completion N₂ D₂ Cert₂)
 104    (P₁ : D₁ → Prop) (P₂ : D₂ → Prop) :
 105    ConservativeFor C₁ P₁ → ConservativeFor C₂ P₂ →
 106      ConservativeFor (productCompletion C₁ C₂) (ProductPredicate P₁ P₂) :=
 107  product_conservative C₁ C₂ P₁ P₂
 108
 109/-- Finite function-space completion: complete each coordinate through the same
 110interface. This is the finite-vector/finite-field display pattern. -/
 111def functionCompletion (I N D Cert : Type*) (C : Completion N D Cert) :
 112    Completion (I → N) (I → D) (I → Cert) where
 113  display := fun n i => C.display (n i)
 114  certifies := fun c d => ∀ i : I, C.certifies (c i) (d i)
 115
 116/-- Pointwise predicate on a finite/display function. -/
 117def AllPredicate {I D : Type*} (P : D → Prop) : (I → D) → Prop :=
 118  fun d => ∀ i : I, P (d i)
 119
 120/-- Conservativity lifts pointwise to finite function displays: if each coordinate
 121predicate has a certificate, the whole function has a coordinatewise certificate. -/
 122theorem function_conservative
 123    {I N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop)
 124    (hC : ConservativeFor C P) :
 125    ConservativeFor (functionCompletion I N D Cert C) (AllPredicate P) := by
 126  intro d hd
 127  choose c hc using fun i : I => hC (d i) (hd i)
 128  exact ⟨c, hc⟩
 129
 130/-- **Function-space completion headline.** Certificate-preserving completion is
 131stable under pointwise finite/function displays, so finite vectors and finite
 132fields can be certified coordinatewise. -/
 133theorem function_completion_headline
 134    {I N D Cert : Type*} (C : Completion N D Cert) (P : D → Prop) :
 135    ConservativeFor C P →
 136      ConservativeFor (functionCompletion I N D Cert C) (AllPredicate P) :=
 137  function_conservative C P
 138
 139end CompletionConservativity
 140end PrimitiveRecognitionCalculus
 141end Foundation
 142end IndisputableMonolith
 143