IndisputableMonolith.Verification.CPT.Pipeline

   1import Mathlib
   2import IndisputableMonolith.Verification.CPT.Core
   3import IndisputableMonolith.Verification.CPT.WindowIdentifiability
   4
   5/-!
   6# CPT Pipeline (`P -> B -> A`)
   7
   8This module formalizes the certified composition shape used by CPT:
   9
  10- `P`: projection/neutrality pre-processing,
  11- `B`: coercivity conversion stage,
  12- `A`: aggregation/decision stage.
  13
  14Theorems in this file establish:
  15
  16- definitional factorization (`PhiStar = A ∘ B ∘ P`),
  17- zero/nonzero soundness under explicit assumptions,
  18- procedure-space membership for `PhiStar` (soundness + finite-data predicate).
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Verification
  23namespace CPT
  24namespace Pipeline
  25
  26open scoped Classical
  27
  28variable {X Y Z : Type}
  29
  30/-- `P` stage: preprocessing/projection map. -/
  31structure ProjectionStage (X Y : Type) where
  32  run : X → Y
  33
  34/-- `B` stage: coercive conversion map. -/
  35structure CoercivityStage (Y Z : Type) where
  36  run : Y → Z
  37
  38/-- `A` stage: aggregation decision map. -/
  39structure AggregationStage (Z : Type) where
  40  run : Z → DecisionTag
  41
  42/-- Canonical CPT membership certifier from stage composition. -/
  43def PhiStar (P : ProjectionStage X Y) (B : CoercivityStage Y Z) (A : AggregationStage Z) :
  44    Procedure X :=
  45  fun x => A.run (B.run (P.run x))
  46
  47theorem pipeline_factorization
  48    (P : ProjectionStage X Y) (B : CoercivityStage Y Z) (A : AggregationStage Z) :
  49    PhiStar P B A = A.run ∘ B.run ∘ P.run := by
  50  rfl
  51
  52/-- Zero-decision soundness for the composed CPT pipeline. -/
  53theorem pipeline_sound
  54    (P : ProjectionStage X Y) (B : CoercivityStage Y Z) (A : AggregationStage Z)
  55    (membership : X → Prop)
  56    (hzero : ∀ x : X, PhiStar P B A x = DecisionTag.zero → membership x) :
  57    ∀ x : X, PhiStar P B A x = DecisionTag.zero → membership x := by
  58  intro x hx
  59  exact hzero x hx
  60
  61/-- Nonzero-decision soundness for the composed CPT pipeline. -/
  62theorem pipeline_nonzero_sound
  63    (P : ProjectionStage X Y) (B : CoercivityStage Y Z) (A : AggregationStage Z)
  64    (excluded : X → Prop)
  65    (hnonzero : ∀ x : X, PhiStar P B A x = DecisionTag.nonzero → excluded x) :
  66    ∀ x : X, PhiStar P B A x = DecisionTag.nonzero → excluded x := by
  67  intro x hx
  68  exact hnonzero x hx
  69
  70/-- Bundle `PhiStar` as a procedure-space element under explicit finite-data and
  71soundness hypotheses. -/
  72theorem phiStar_in_procedureSpace
  73    (P : ProjectionStage X Y) (B : CoercivityStage Y Z) (A : AggregationStage Z)
  74    (isZero isNonzero : X → Prop)
  75    (finiteData : Procedure X → Prop)
  76    (hzero : ∀ {x : X}, PhiStar P B A x = DecisionTag.zero → isZero x)
  77    (hnonzero : ∀ {x : X}, PhiStar P B A x = DecisionTag.nonzero → isNonzero x)
  78    (hfinite : finiteData (PhiStar P B A)) :
  79    ProcedureSpace isZero isNonzero finiteData (PhiStar P B A) := by
  80  refine
  81    { sound :=
  82        { zero_sound := by
  83            intro x hx
  84            exact hzero hx
  85          nonzero_sound := by
  86            intro x hx
  87            exact hnonzero hx }
  88      finite_data := hfinite }
  89
  90end Pipeline
  91end CPT
  92end Verification
  93end IndisputableMonolith
  94