IndisputableMonolith.Verification.CPT.Core

   1import Mathlib
   2import IndisputableMonolith.CPM.LawOfExistence
   3
   4/-!
   5# CPT Verification Core
   6
   7This module provides small reusable interfaces for the CPT formalization:
   8
   9- decision tags (`zero/nonzero/inconclusive`),
  10- procedure and resolved-set utilities,
  11- class-restricted domination relation,
  12- lightweight wrappers around the CPM A/B/C closure theorems.
  13
  14The intent is to keep theorem statements claim-honest and composable across:
  15`WindowIdentifiability`, `Pipeline`, `Optimality`, and `ForcedFactorization`.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace Verification
  20namespace CPT
  21
  22open scoped Classical
  23
  24/-- Ternary decision output used by CPT-style procedures. -/
  25inductive DecisionTag
  26  | zero
  27  | nonzero
  28  | inconclusive
  29  deriving DecidableEq, Repr
  30
  31/-- A CPT procedure on inputs of type `X`. -/
  32abbrev Procedure (X : Type) : Type := X → DecisionTag
  33
  34/-- Inputs resolved by a procedure (i.e., not `inconclusive`). -/
  35def resolvedSet {X : Type} (Φ : Procedure X) : Set X :=
  36  {x | Φ x ≠ DecisionTag.inconclusive}
  37
  38/-- Resolved inputs inside a class `C`. -/
  39def resolvedSetOn {X : Type} (C : Set X) (Φ : Procedure X) : Set X :=
  40  {x | x ∈ C ∧ x ∈ resolvedSet Φ}
  41
  42/-- Domination on a restricted class: `Φ` resolves at least what `Ψ` resolves on `C`,
  43and agrees with `Ψ` wherever `Ψ` resolves on `C`. -/
  44def dominatesOn {X : Type} (C : Set X) (Φ Ψ : Procedure X) : Prop :=
  45  resolvedSetOn C Ψ ⊆ resolvedSetOn C Φ
  46  ∧
  47  ∀ ⦃x : X⦄, x ∈ resolvedSetOn C Ψ → Φ x = Ψ x
  48
  49/-- Soundness specification for ternary procedures:
  50`zero` certifies `isZero`; `nonzero` certifies `isNonzero`. -/
  51structure SoundProcedure {X : Type}
  52    (isZero isNonzero : X → Prop) (Φ : Procedure X) : Prop where
  53  zero_sound : ∀ {x : X}, Φ x = DecisionTag.zero → isZero x
  54  nonzero_sound : ∀ {x : X}, Φ x = DecisionTag.nonzero → isNonzero x
  55
  56/-- A procedure-space package used in optimality theorems:
  57soundness plus an abstract finite-data predicate. -/
  58structure ProcedureSpace {X : Type}
  59    (isZero isNonzero : X → Prop) (finiteData : Procedure X → Prop)
  60    (Φ : Procedure X) : Prop where
  61  sound : SoundProcedure isZero isNonzero Φ
  62  finite_data : finiteData Φ
  63
  64namespace CPMBridge
  65
  66open IndisputableMonolith.CPM.LawOfExistence
  67
  68variable {β : Type}
  69
  70/-- CPT `B`-stage wrapper for AB-forward coercivity. -/
  71theorem b_stage_forward_coercivity
  72    (M : Model β) (a : β) :
  73    M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Ceng) * M.energyGap a :=
  74  M.defect_le_constants_mul_energyGap a
  75
  76/-- CPT `B`-stage wrapper for AB-reverse coercivity. -/
  77theorem b_stage_reverse_coercivity
  78    (M : Model β)
  79    (hpos : 0 < M.C.Knet ∧ 0 < M.C.Cproj ∧ 0 < M.C.Ceng)
  80    (a : β) :
  81    M.energyGap a ≥ cmin M.C * M.defectMass a :=
  82  M.energyGap_ge_cmin_mul_defect hpos a
  83
  84/-- CPT `A`-stage wrapper for AC aggregation. -/
  85theorem a_stage_aggregation
  86    (M : Model β) (a : β) :
  87    M.defectMass a ≤ (M.C.Knet * M.C.Cproj * M.C.Cdisp) * M.tests a :=
  88  M.defect_le_constants_mul_tests a
  89
  90end CPMBridge
  91
  92end CPT
  93end Verification
  94end IndisputableMonolith
  95