IndisputableMonolith.Verification.CPT.WindowIdentifiability

   1import Mathlib
   2import IndisputableMonolith.Verification.CPT.Core
   3
   4/-!
   5# CPT Window Identifiability
   6
   7This module formalizes the matrix-level identifiability core used in the CPT window
   8arguments:
   9
  10- injective reconstruction from finite window measurements,
  11- equivalence with trivial kernel of the measurement map,
  12- equivalence with a "full-column-rank" predicate (defined as injectivity here),
  13- zero-detection under identifiability.
  14
  15The "generic/nondegenerate" layer is represented explicitly by a named hypothesis
  16bundle (`NonvanishingMinorHypothesis`) to keep claim strength explicit.
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Verification
  21namespace CPT
  22namespace WindowIdentifiability
  23
  24open scoped Classical
  25
  26abbrev Vec (ι : Type) := ι → ℝ
  27
  28variable {m n : Type} [Fintype n] [DecidableEq n]
  29
  30/-- Linear measurement map induced by the window matrix. -/
  31noncomputable def measurementLinear (A : Matrix m n ℝ) :
  32    Vec n →ₗ[ℝ] Vec m :=
  33  Matrix.toLin' A
  34
  35/-- Window identifiability: the measurement map is injective. -/
  36def Identifiable (A : Matrix m n ℝ) : Prop :=
  37  Function.Injective (measurementLinear A)
  38
  39/-- Trivial-kernel formulation of identifiability. -/
  40def TrivialKernel (A : Matrix m n ℝ) : Prop :=
  41  LinearMap.ker (measurementLinear A) = ⊥
  42
  43/-- "Full column rank" in the finite-data reconstruction sense:
  44injectivity of the matrix-induced linear map. -/
  45def FullColumnRank (A : Matrix m n ℝ) : Prop :=
  46  Function.Injective (measurementLinear A)
  47
  48theorem identifiable_iff_trivialKernel (A : Matrix m n ℝ) :
  49    Identifiable A ↔ TrivialKernel A := by
  50  simpa [Identifiable, TrivialKernel] using
  51    (LinearMap.ker_eq_bot (f := measurementLinear A)).symm
  52
  53theorem identifiable_iff_fullColumnRank (A : Matrix m n ℝ) :
  54    Identifiable A ↔ FullColumnRank A := by
  55  rfl
  56
  57theorem trivialKernel_iff_fullColumnRank (A : Matrix m n ℝ) :
  58    TrivialKernel A ↔ FullColumnRank A := by
  59  constructor
  60  · intro h
  61    exact (identifiable_iff_fullColumnRank A).mp ((identifiable_iff_trivialKernel A).mpr h)
  62  · intro h
  63    exact (identifiable_iff_trivialKernel A).mp ((identifiable_iff_fullColumnRank A).mpr h)
  64
  65/-- Under identifiability, observing zero output forces the input to be zero. -/
  66theorem zero_detection_of_identifiable (A : Matrix m n ℝ)
  67    (hId : Identifiable A) (x : Vec n) :
  68    measurementLinear A x = 0 → x = 0 := by
  69  intro hx
  70  apply hId
  71  calc
  72    measurementLinear A x = 0 := hx
  73    _ = measurementLinear A 0 := by simp
  74
  75/-- Explicit bridge hypothesis for the paper's generic/nondegenerate regime:
  76we assume the relevant maximal-minor nonvanishing condition has already been
  77verified and expose only its identifiability consequence at this layer. -/
  78structure NonvanishingMinorHypothesis (A : Matrix m n ℝ) : Prop where
  79  fullColumnRank : FullColumnRank A
  80
  81theorem generic_identifiability_assuming_nonvanishing_minor
  82    (A : Matrix m n ℝ)
  83    (hMinor : NonvanishingMinorHypothesis A) :
  84    Identifiable A :=
  85  hMinor.fullColumnRank
  86
  87end WindowIdentifiability
  88end CPT
  89end Verification
  90end IndisputableMonolith
  91