IndisputableMonolith.Verification.CPT.Optimality

   1import Mathlib
   2import IndisputableMonolith.Verification.CPT.Core
   3import IndisputableMonolith.Verification.CPT.Pipeline
   4
   5/-!
   6# CPT Optimality (Domination on a Class)
   7
   8This module formalizes a class-restricted domination relation for CPT procedures and
   9proves a clean domination theorem for `PhiStar` under explicit assumptions:
  10
  11- `Psi` resolves every input in the target class,
  12- `PhiStar` and `Psi` agree on that class.
  13
  14The theorem intentionally keeps hypotheses explicit, matching claim-hygiene requirements.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Verification
  19namespace CPT
  20namespace Optimality
  21
  22open scoped Classical
  23
  24variable {X Y Z : Type}
  25
  26abbrev PhiStar
  27    (P : Pipeline.ProjectionStage X Y)
  28    (B : Pipeline.CoercivityStage Y Z)
  29    (A : Pipeline.AggregationStage Z) : Procedure X :=
  30  Pipeline.PhiStar P B A
  31
  32/-- A procedure resolves every point in class `C` if it never returns `inconclusive` on `C`. -/
  33def ResolvesClass (C : Set X) (Φ : Procedure X) : Prop :=
  34  ∀ ⦃x : X⦄, x ∈ C → Φ x ≠ DecisionTag.inconclusive
  35
  36theorem procedure_resolves_class
  37    (C : Set X) (Φ : Procedure X)
  38    (hResolve : ResolvesClass C Φ) :
  39    C ⊆ resolvedSet Φ := by
  40  intro x hxC
  41  exact hResolve hxC
  42
  43theorem phiStar_in_procedureSpace
  44    (P : Pipeline.ProjectionStage X Y)
  45    (B : Pipeline.CoercivityStage Y Z)
  46    (A : Pipeline.AggregationStage Z)
  47    (isZero isNonzero : X → Prop)
  48    (finiteData : Procedure X → Prop)
  49    (hzero : ∀ {x : X}, PhiStar P B A x = DecisionTag.zero → isZero x)
  50    (hnonzero : ∀ {x : X}, PhiStar P B A x = DecisionTag.nonzero → isNonzero x)
  51    (hfinite : finiteData (PhiStar P B A)) :
  52    ProcedureSpace isZero isNonzero finiteData (PhiStar P B A) :=
  53  Pipeline.phiStar_in_procedureSpace P B A isZero isNonzero finiteData hzero hnonzero hfinite
  54
  55theorem phiStar_resolves_nondegenerate
  56    (P : Pipeline.ProjectionStage X Y)
  57    (B : Pipeline.CoercivityStage Y Z)
  58    (A : Pipeline.AggregationStage Z)
  59    (C : Set X)
  60    (hResolve : ResolvesClass C (PhiStar P B A)) :
  61    C ⊆ resolvedSet (PhiStar P B A) :=
  62  procedure_resolves_class C (PhiStar P B A) hResolve
  63
  64/-- Domination/optimality on a class:
  65if `Psi` resolves the class and agrees with `PhiStar` on that class, then `PhiStar`
  66dominates `Psi` on that class. -/
  67theorem phiStar_dominates
  68    (P : Pipeline.ProjectionStage X Y)
  69    (B : Pipeline.CoercivityStage Y Z)
  70    (A : Pipeline.AggregationStage Z)
  71    (C : Set X)
  72    (Ψ : Procedure X)
  73    (hPsiResolve : ResolvesClass C Ψ)
  74    (hAgreeOnClass : ∀ ⦃x : X⦄, x ∈ C → PhiStar P B A x = Ψ x) :
  75    dominatesOn C (PhiStar P B A) Ψ := by
  76  constructor
  77  · intro x hx
  78    rcases hx with ⟨hxC, _hxResPsi⟩
  79    have hΨ_on_class : x ∈ resolvedSet Ψ :=
  80      (procedure_resolves_class C Ψ hPsiResolve) hxC
  81    have hEq : PhiStar P B A x = Ψ x := hAgreeOnClass hxC
  82    have hΦ_on_class : x ∈ resolvedSet (PhiStar P B A) := by
  83      simpa [resolvedSet, hEq] using hΨ_on_class
  84    exact ⟨hxC, hΦ_on_class⟩
  85  · intro x hx
  86    exact hAgreeOnClass hx.1
  87
  88/-- Global-class specialization of domination (`C = Set.univ`). -/
  89theorem phiStar_dominates_global
  90    (P : Pipeline.ProjectionStage X Y)
  91    (B : Pipeline.CoercivityStage Y Z)
  92    (A : Pipeline.AggregationStage Z)
  93    (Ψ : Procedure X)
  94    (hPsiResolve : ResolvesClass (Set.univ : Set X) Ψ)
  95    (hAgreeGlobal : ∀ x : X, PhiStar P B A x = Ψ x) :
  96    dominatesOn (Set.univ : Set X) (PhiStar P B A) Ψ := by
  97  exact phiStar_dominates P B A (Set.univ : Set X) Ψ hPsiResolve (by
  98    intro x _hx
  99    exact hAgreeGlobal x)
 100
 101end Optimality
 102end CPT
 103end Verification
 104end IndisputableMonolith
 105