IndisputableMonolith.Verification.CPT.Exports
IndisputableMonolith/Verification/CPT/Exports.lean · 242 lines · 18 declarations
show as:
view math explainer →
1import IndisputableMonolith.Verification.CPT.Core
2import IndisputableMonolith.Verification.CPT.WindowIdentifiability
3import IndisputableMonolith.Verification.CPT.Pipeline
4import IndisputableMonolith.Verification.CPT.Optimality
5import IndisputableMonolith.Verification.CPT.ForcedFactorization
6import IndisputableMonolith.Verification.CPT.RankCertification
7import IndisputableMonolith.Verification.CPT.EpsilonCertification
8
9/-!
10# CPT Export Surface
11
12Citation-friendly theorem aliases for the CPT formalization layer.
13All items are fully proved (no `sorry`, no new `axiom`).
14
15Paper-to-Lean mapping:
16- `WINDOW_*` ← paper Thm. 4.5 / 6.5 (window identifiability family)
17- `CPT_PIPELINE_*` ← paper P→B→A pipeline (§5 / §6 composition)
18- `CPT_OPT_*` ← paper Thm. 6.11 (domination / optimality)
19- `CPT_FACTOR_*` ← paper Thm. 5.1 (forced factorisation)
20- `CPT_EPS_*` ← paper ε-noise layer (§5 ε-optimal certification)
21-/
22
23namespace IndisputableMonolith
24namespace Verification
25namespace CPT
26namespace Exports
27
28-- ───────────────────────────────────────────────────────────────
29-- Window Identifiability (paper Thm. 4.5 / 6.5)
30-- ───────────────────────────────────────────────────────────────
31
32/-- Identifiability ↔ trivial kernel (paper Thm. 6.5). -/
33theorem WINDOW_identifiable_iff_trivialKernel
34 {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
35 WindowIdentifiability.Identifiable A ↔ WindowIdentifiability.TrivialKernel A :=
36 WindowIdentifiability.identifiable_iff_trivialKernel A
37
38/-- Identifiability ↔ full column rank (paper Thm. 4.5). -/
39theorem WINDOW_identifiable_iff_fullColumnRank
40 {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) :
41 WindowIdentifiability.Identifiable A ↔ WindowIdentifiability.FullColumnRank A :=
42 WindowIdentifiability.identifiable_iff_fullColumnRank A
43
44/-- Zero-detection under identifiability. -/
45theorem WINDOW_zero_detection_of_identifiable
46 {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
47 (hI : WindowIdentifiability.Identifiable A) (v : Fin n → ℝ)
48 (hv : A.mulVec v = 0) : v = 0 :=
49 WindowIdentifiability.zero_detection_of_identifiable A hI v hv
50
51-- ───────────────────────────────────────────────────────────────
52-- Unified P→B→A Pipeline (paper §5/§6)
53-- ───────────────────────────────────────────────────────────────
54
55/-- Pipeline is definitionally equal to A ∘ B ∘ P (paper §5). -/
56theorem CPT_PIPELINE_factorization
57 {X Y Z : Type}
58 (P : Pipeline.ProjectionStage X Y)
59 (B : Pipeline.CoercivityStage Y Z)
60 (A : Pipeline.AggregationStage Z) :
61 Pipeline.PhiStar P B A = A.run ∘ B.run ∘ P.run :=
62 Pipeline.pipeline_factorization P B A
63
64/-- Zero-decision soundness of the composed pipeline. -/
65theorem CPT_PIPELINE_sound
66 {X Y Z : Type}
67 (P : Pipeline.ProjectionStage X Y)
68 (B : Pipeline.CoercivityStage Y Z)
69 (A : Pipeline.AggregationStage Z)
70 (membership : X → Prop)
71 (hzero : ∀ x, Pipeline.PhiStar P B A x = DecisionTag.zero → membership x) :
72 ∀ x, Pipeline.PhiStar P B A x = DecisionTag.zero → membership x :=
73 Pipeline.pipeline_sound P B A membership hzero
74
75/-- Nonzero-decision soundness of the composed pipeline. -/
76theorem CPT_PIPELINE_nonzero_sound
77 {X Y Z : Type}
78 (P : Pipeline.ProjectionStage X Y)
79 (B : Pipeline.CoercivityStage Y Z)
80 (A : Pipeline.AggregationStage Z)
81 (excluded : X → Prop)
82 (hnonzero : ∀ x, Pipeline.PhiStar P B A x = DecisionTag.nonzero → excluded x) :
83 ∀ x, Pipeline.PhiStar P B A x = DecisionTag.nonzero → excluded x :=
84 Pipeline.pipeline_nonzero_sound P B A excluded hnonzero
85
86-- ───────────────────────────────────────────────────────────────
87-- Domination / Optimality (paper Thm. 6.11)
88-- ───────────────────────────────────────────────────────────────
89
90/-- PhiStar dominates any agreeing procedure on the class (paper Thm. 6.11). -/
91theorem CPT_OPT_phiStar_dominates
92 {X Y Z : Type}
93 (P : Pipeline.ProjectionStage X Y)
94 (B : Pipeline.CoercivityStage Y Z)
95 (A : Pipeline.AggregationStage Z)
96 (C : Set X) (Ψ : Procedure X)
97 (hPsiResolve : Optimality.ResolvesClass C Ψ)
98 (hAgree : ∀ ⦃x : X⦄, x ∈ C → Pipeline.PhiStar P B A x = Ψ x) :
99 dominatesOn C (Pipeline.PhiStar P B A) Ψ :=
100 Optimality.phiStar_dominates P B A C Ψ hPsiResolve hAgree
101
102/-- Global class (`Set.univ`) domination specialization. -/
103theorem CPT_OPT_phiStar_dominates_global
104 {X Y Z : Type}
105 (P : Pipeline.ProjectionStage X Y)
106 (B : Pipeline.CoercivityStage Y Z)
107 (A : Pipeline.AggregationStage Z)
108 (Ψ : Procedure X)
109 (hPsiResolve : Optimality.ResolvesClass (Set.univ : Set X) Ψ)
110 (hAgreeGlobal : ∀ x : X, Pipeline.PhiStar P B A x = Ψ x) :
111 dominatesOn (Set.univ : Set X) (Pipeline.PhiStar P B A) Ψ :=
112 Optimality.phiStar_dominates_global P B A Ψ hPsiResolve hAgreeGlobal
113
114-- ───────────────────────────────────────────────────────────────
115-- Forced Factorisation (paper Thm. 5.1)
116-- ───────────────────────────────────────────────────────────────
117
118/-- Monotone reparametrization exists under certificate hypotheses (paper Thm. 5.1 step 1). -/
119theorem CPT_FACTOR_exists_monotone_reparam
120 {S O : Type}
121 (R : ForcedFactorization.RatioCostSpace S O)
122 (C : S → O → ℝ)
123 (h : ForcedFactorization.CertificateHypotheses R C) :
124 ∃ φ : ForcedFactorization.RatioCostSpace.CostCode R → ℝ,
125 (∀ s o, C s o = φ ⟨R.canonicalCost s o, ⟨(s, o), rfl⟩⟩)
126 ∧
127 (∀ s o1 o2,
128 R.canonicalCost s o1 ≤ R.canonicalCost s o2 →
129 φ ⟨R.canonicalCost s o1, ⟨(s, o1), rfl⟩⟩
130 ≤
131 φ ⟨R.canonicalCost s o2, ⟨(s, o2), rfl⟩⟩) :=
132 ForcedFactorization.exists_monotone_reparam R C h
133
134/-- State-independence under explicit rigidity hypothesis (paper Thm. 5.1 rigidity step). -/
135theorem CPT_FACTOR_phi_independent_of_state
136 {S O : Type} [Inhabited S]
137 (R : ForcedFactorization.RatioCostSpace S O)
138 (C : S → O → ℝ)
139 (hRig : ForcedFactorization.RigidityHypotheses R C) :
140 ∃ ψ : O → ℝ, ∀ s o, C s o = ψ o :=
141 ForcedFactorization.phi_independent_of_state R C hRig
142
143/-- Assembled forced-factorization theorem (paper Thm. 5.1). -/
144theorem CPT_FACTOR_forced_factorization
145 {S O : Type} [Inhabited S]
146 (R : ForcedFactorization.RatioCostSpace S O)
147 (C : S → O → ℝ)
148 (h : ForcedFactorization.CertificateHypotheses R C)
149 (hRig : ForcedFactorization.RigidityHypotheses R C) :
150 (∃ φ : ForcedFactorization.RatioCostSpace.CostCode R → ℝ,
151 (∀ s o, C s o = φ ⟨R.canonicalCost s o, ⟨(s, o), rfl⟩⟩))
152 ∧
153 (∃ ψ : O → ℝ, ∀ s o, C s o = ψ o) := by
154 rcases ForcedFactorization.exists_monotone_reparam R C h with ⟨φ, hrepr, _⟩
155 rcases ForcedFactorization.phi_independent_of_state R C hRig with ⟨ψ, hψ⟩
156 exact ⟨⟨φ, hrepr⟩, ⟨ψ, hψ⟩⟩
157
158/-- Strong forced-factorization form with uniqueness on both layers:
159unique cost-image reparametrization + unique state-free profile. -/
160theorem CPT_FACTOR_forced_factorization_unique
161 {S O : Type} [Inhabited S]
162 (R : ForcedFactorization.RatioCostSpace S O)
163 (C : S → O → ℝ)
164 (h : ForcedFactorization.CertificateHypotheses R C)
165 (hRig : ForcedFactorization.RigidityHypotheses R C) :
166 (∃! φ : ForcedFactorization.RatioCostSpace.CostCode R → ℝ,
167 ∀ s o, C s o = φ ⟨R.canonicalCost s o, ⟨(s, o), rfl⟩⟩)
168 ∧
169 (∃! ψ : O → ℝ, ∀ s o, C s o = ψ o) :=
170 ForcedFactorization.forced_factorization_unique R C h hRig
171
172/-- Uniqueness theorem from primitive ratio-level assumptions
173 (derives the H1/H2 bundle internally). -/
174theorem CPT_FACTOR_forced_factorization_unique_of_primitives
175 {S O : Type} [Inhabited S]
176 (R : ForcedFactorization.RatioCostSpace S O)
177 (C : S → O → ℝ)
178 (hPrim : ForcedFactorization.PrimitiveCertificateHypotheses R C)
179 (hRigPrim : ForcedFactorization.PrimitiveRigidityHypotheses R) :
180 (∃! φ : ForcedFactorization.RatioCostSpace.CostCode R → ℝ,
181 ∀ s o, C s o = φ ⟨R.canonicalCost s o, ⟨(s, o), rfl⟩⟩)
182 ∧
183 (∃! ψ : O → ℝ, ∀ s o, C s o = ψ o) :=
184 ForcedFactorization.forced_factorization_unique_of_primitives R C hPrim hRigPrim
185
186-- ───────────────────────────────────────────────────────────────
187-- General (d,W) Rank Certification
188-- ───────────────────────────────────────────────────────────────
189
190/-- Vandermonde determinant is nonzero for distinct nodes. -/
191theorem RANK_vandermonde_det_ne_zero
192 {n : ℕ} (v : Fin n → ℝ)
193 (hDistinct : RankCertification.DistinctNodes v) :
194 (Matrix.vandermonde v).det ≠ 0 :=
195 RankCertification.vandermonde_det_ne_zero v hDistinct
196
197/-- Hankel matrix of an exponential sum with distinct nodes and nonzero amplitudes
198 has nonzero determinant. -/
199theorem RANK_hankel_det_ne_zero
200 {d : ℕ} (E : RankCertification.ExponentialSumData d) :
201 (RankCertification.hankelMatrix E).det ≠ 0 :=
202 RankCertification.hankel_det_ne_zero E
203
204/-- **General (d,W) rank certification**: For any d ≥ 1 and W ≥ 1 with an
205 exponential-sum witness, the Hankel matrix is nonsingular, witnessing
206 nonemptiness of the identifiability locus Ω_{d,W}. -/
207theorem RANK_identifiability_locus_nonempty
208 (d : ℕ) (W : ℕ) (_hd : 0 < d) (_hW : 0 < W)
209 (E : RankCertification.ExponentialSumData d) :
210 (RankCertification.hankelMatrix E).det ≠ 0 :=
211 RankCertification.identifiability_locus_nonempty d W _hd _hW E
212
213-- ───────────────────────────────────────────────────────────────
214-- Epsilon / Noise Layer
215-- ───────────────────────────────────────────────────────────────
216
217/-- Perturbed argmin (`cHat`) is `2ε`-optimal for true cost (`c`)
218under uniform absolute error `|cHat-c| ≤ ε`. -/
219theorem CPT_EPS_approx_argmin_stability
220 {O : Type}
221 (c cHat : O → ℝ) (ε : ℝ)
222 (hErr : ∀ o, |cHat o - c o| ≤ ε)
223 (oHat : O)
224 (hMin : ∀ o, cHat oHat ≤ cHat o) :
225 ∀ o, c oHat ≤ c o + 2 * ε :=
226 EpsilonCertification.approx_argmin_stability c cHat ε hErr oHat hMin
227
228/-- Set-level form: perturbed minimizer lies in `MeanEps c (2ε)`. -/
229theorem CPT_EPS_approx_argmin_mem_meanEps
230 {O : Type}
231 (c cHat : O → ℝ) (ε : ℝ)
232 (hErr : ∀ o, |cHat o - c o| ≤ ε)
233 (oHat : O)
234 (hMin : ∀ o, cHat oHat ≤ cHat o) :
235 oHat ∈ EpsilonCertification.MeanEps c (2 * ε) :=
236 EpsilonCertification.approx_argmin_mem_meanEps c cHat ε hErr oHat hMin
237
238end Exports
239end CPT
240end Verification
241end IndisputableMonolith
242