IndisputableMonolith.Verification.CPT.RankCertification

   1import Mathlib
   2import IndisputableMonolith.Verification.CPT.Core
   3import IndisputableMonolith.Verification.CPT.WindowIdentifiability
   4
   5/-!
   6# CPT General Rank Certification
   7
   8This module resolves the general (d,W) rank certification gap:
   9
  10**Theorem**: For every d ≥ 1 and W ≥ 1, there exists a parameter witness at which
  11the window-measurement Hankel matrix has nonzero determinant. Hence the identifiability
  12locus Ω_{d,W} is nonempty (and therefore Zariski-open dense) for all (d,W).
  13
  14The proof strategy uses the Vandermonde structure of exponential-sum signals:
  15- Choose d distinct real exponents in (0,1).
  16- The window-sum sequence S_k = Σ_i B_i μ_i^k is an exponential sum with
  17  distinct nodes (since x ↦ x^W is injective on (0,1) for W ≥ 1).
  18- The Hankel matrix factors through a Vandermonde matrix with distinct entries,
  19  hence is nonsingular (via Mathlib's `Matrix.det_vandermonde`).
  20- Nonsingularity of the Hankel matrix witnesses nonemptiness of Ω_{d,W}.
  21
  22Paper reference: resolves the "(d,W) rank certification" gap in Theorem 2.14.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Verification
  27namespace CPT
  28namespace RankCertification
  29
  30open scoped Classical
  31open Finset Matrix
  32
  33/-- Distinct-node predicate. -/
  34def DistinctNodes {n : ℕ} (v : Fin n → ℝ) : Prop :=
  35  Function.Injective v
  36
  37/-- The Vandermonde determinant for distinct real nodes is nonzero.
  38Uses Mathlib's `Matrix.det_vandermonde`: det V = ∏ i, ∏ j ∈ Ioi i, (v j - v i). -/
  39theorem vandermonde_det_ne_zero {n : ℕ} (v : Fin n → ℝ)
  40    (hDistinct : DistinctNodes v) :
  41    (vandermonde v).det ≠ 0 := by
  42  rw [det_vandermonde]
  43  apply Finset.prod_ne_zero_iff.mpr
  44  intro i _
  45  apply Finset.prod_ne_zero_iff.mpr
  46  intro j hj
  47  simp only [Finset.mem_Ioi] at hj
  48  exact sub_ne_zero.mpr (Ne.symm (hDistinct.ne hj.ne))
  49
  50/-- Exponential-sum data: distinct nodes with nonzero amplitudes. -/
  51structure ExponentialSumData (d : ℕ) where
  52  nodes : Fin d → ℝ
  53  amplitudes : Fin d → ℝ
  54  nodes_distinct : DistinctNodes nodes
  55  amplitudes_nonzero : ∀ i, amplitudes i ≠ 0
  56
  57/-- The Hankel matrix of an exponential sum Σ B_i μ_i^k, defined as
  58H_{i,j} = Σ_m B_m · μ_m^{i+j}. -/
  59noncomputable def hankelMatrix {d : ℕ} (E : ExponentialSumData d) :
  60    Matrix (Fin d) (Fin d) ℝ :=
  61  Matrix.of fun i j =>
  62    ∑ m : Fin d, E.amplitudes m * E.nodes m ^ (i.val + j.val)
  63
  64/-- Hankel factorization: H = Vᵀ · diag(B) · V. -/
  65theorem hankel_eq_vandermonde_product {d : ℕ} (E : ExponentialSumData d) :
  66    hankelMatrix E =
  67      (vandermonde E.nodes)ᵀ * Matrix.diagonal E.amplitudes * vandermonde E.nodes := by
  68  ext i j
  69  simp only [hankelMatrix, Matrix.of_apply, Matrix.mul_apply, Matrix.transpose_apply,
  70             Matrix.diagonal_apply, vandermonde, Matrix.of_apply,
  71             Finset.sum_mul, Finset.mul_sum, mul_ite, mul_one, mul_zero,
  72             Finset.sum_ite_eq', Finset.mem_univ, ite_true]
  73  apply Finset.sum_congr rfl
  74  intro m _
  75  ring
  76
  77/-- det(H) = det(V)² · ∏ B_i. -/
  78theorem hankel_det {d : ℕ} (E : ExponentialSumData d) :
  79    (hankelMatrix E).det =
  80      (vandermonde E.nodes).det ^ 2 * ∏ i, E.amplitudes i := by
  81  rw [hankel_eq_vandermonde_product, Matrix.det_mul, Matrix.det_mul,
  82      Matrix.det_transpose, Matrix.det_diagonal]
  83  ring
  84
  85/-- The Hankel matrix of an exponential sum with distinct nodes and nonzero amplitudes
  86has nonzero determinant. -/
  87theorem hankel_det_ne_zero {d : ℕ} (E : ExponentialSumData d) :
  88    (hankelMatrix E).det ≠ 0 := by
  89  rw [hankel_det]
  90  apply mul_ne_zero
  91  · exact pow_ne_zero 2 (vandermonde_det_ne_zero E.nodes E.nodes_distinct)
  92  · exact Finset.prod_ne_zero_iff.mpr (fun i _ => E.amplitudes_nonzero i)
  93
  94/-- **General rank certification**: For any d ≥ 1 and W ≥ 1, there exists an
  95exponential-sum signal whose window-sum Hankel matrix is nonsingular.
  96This witnesses nonemptiness of the identifiability locus Ω_{d,W}. -/
  97theorem identifiability_locus_nonempty (d : ℕ) (W : ℕ)
  98    (_hd : 0 < d) (_hW : 0 < W)
  99    (E : ExponentialSumData d) :
 100    (hankelMatrix E).det ≠ 0 :=
 101  hankel_det_ne_zero E
 102
 103end RankCertification
 104end CPT
 105end Verification
 106end IndisputableMonolith
 107