IndisputableMonolith.NumberTheory.RecognitionTheta.Convergence

   1import IndisputableMonolith.NumberTheory.RecognitionTheta
   2
   3/-!
   4  RecognitionTheta/Convergence.lean
   5
   6  Track C, sub-conjecture A.1.
   7
   8  The current `RecognitionThetaConvergence` statement asks for summability of
   9  the Recognition Theta term for every `t > 0`. This module proves the general
  10  comparison theorem needed to discharge it: if the terms admit a summable
  11  nonnegative majorant for each positive `t`, then A.1 follows.
  12
  13  The remaining mathematical content is not hidden here. It is the construction
  14  of such a majorant from lower bounds on `costSpectrumValue n` and upper
  15  bounds on the phi-rung weight.
  16-/
  17
  18namespace IndisputableMonolith
  19namespace NumberTheory
  20namespace RecognitionTheta
  21namespace Convergence
  22
  23noncomputable section
  24
  25/-- A summable nonnegative majorant for the Recognition Theta terms at each
  26positive time. -/
  27structure RecognitionThetaMajorant where
  28  majorant : ℝ → ℕ → ℝ
  29  summable_majorant :
  30    ∀ t : ℝ, 0 < t → Summable (majorant t)
  31  term_norm_le :
  32    ∀ t : ℝ, 0 < t →
  33      ∀ n : ℕ, ‖recognitionThetaTerm t n‖ ≤ majorant t n
  34
  35/-- A majorant package proves Recognition Theta convergence. -/
  36theorem recognitionThetaConvergence_of_majorant
  37    (maj : RecognitionThetaMajorant) :
  38    RecognitionThetaConvergence where
  39  summable := by
  40    intro t ht
  41    exact (maj.summable_majorant t ht).of_norm_bounded
  42      (maj.term_norm_le t ht)
  43
  44/-- A reusable sufficient condition: domination by a geometric sequence. -/
  45structure RecognitionThetaGeometricMajorant where
  46  C : ℝ
  47  q : ℝ
  48  C_nonneg : 0 ≤ C
  49  q_nonneg : 0 ≤ q
  50  q_lt_one : q < 1
  51  term_norm_le :
  52    ∀ t : ℝ, 0 < t →
  53      ∀ n : ℕ, ‖recognitionThetaTerm t n‖ ≤ C * q ^ n
  54
  55/-- A geometric majorant is a summable majorant. -/
  56def majorant_of_geometric
  57    (geo : RecognitionThetaGeometricMajorant) :
  58    RecognitionThetaMajorant where
  59  majorant := fun _ n => geo.C * geo.q ^ n
  60  summable_majorant := by
  61    intro _t _ht
  62    exact Summable.mul_left geo.C
  63      (summable_geometric_of_lt_one geo.q_nonneg geo.q_lt_one)
  64  term_norm_le := geo.term_norm_le
  65
  66/-- A geometric majorant proves Recognition Theta convergence. -/
  67theorem recognitionThetaConvergence_of_geometricMajorant
  68    (geo : RecognitionThetaGeometricMajorant) :
  69    RecognitionThetaConvergence :=
  70  recognitionThetaConvergence_of_majorant (majorant_of_geometric geo)
  71
  72/-! ## Current A.1 attack surface -/
  73
  74/-- Machine-readable A.1 status: the comparison theorem is proved; the remaining
  75input is a summable majorant, ideally geometric after finitely many terms. -/
  76structure RecognitionThetaConvergenceAttackSurface where
  77  comparison :
  78    RecognitionThetaMajorant → RecognitionThetaConvergence
  79  geometric_comparison :
  80    RecognitionThetaGeometricMajorant → RecognitionThetaConvergence
  81
  82def recognitionThetaConvergenceAttackSurface :
  83    RecognitionThetaConvergenceAttackSurface where
  84  comparison := recognitionThetaConvergence_of_majorant
  85  geometric_comparison := recognitionThetaConvergence_of_geometricMajorant
  86
  87end
  88
  89end Convergence
  90end RecognitionTheta
  91end NumberTheory
  92end IndisputableMonolith
  93