TransferOperator

formal source

  22  ⟨{ T := ContinuousLinearMap.id ℂ (LatticeMeasure → ℂ) }⟩
  23
  24/-- The transfer operator associated with a kernel. -/
  25noncomputable def TransferOperator (K : Kernel) : (LatticeMeasure → ℂ) →L[ℂ] (LatticeMeasure → ℂ) :=
  26  K.T
  27
  28/-- OS reflection positivity surrogate: existence of a transfer kernel with a
  29    uniform overlap lower bound β ∈ (0,1]. This encodes a spectral positivity
  30    guard compatible with Dobrushin-type contraction. -/
  31def OSPositivity (_μ : LatticeMeasure) : Prop := ∃ K : Kernel, ∃ β : ℝ, OverlapLowerBoundOS K β
  32
  33lemma OSPositivity_default (_μ : LatticeMeasure) : OSPositivity _μ := by
  34  refine ⟨default, 1, ?_⟩
  35  dsimp [OverlapLowerBoundOS]
  36  constructor <;> norm_num
  37
  38/-- Overlap lower bound for a kernel (β ∈ (0,1]). -/
  39def OverlapLowerBoundOS (_K : Kernel) (β : ℝ) : Prop := 0 < β ∧ β ≤ 1
  40
  41/-- Perron–Frobenius transfer spectral gap property. -/
  42def TransferPFGap (_μ : LatticeMeasure) (_K : Kernel) (γ : ℝ) : Prop := 0 < γ
  43
  44/-- Gap persistence hypothesis (continuum stability). -/
  45def GapPersists (γ : ℝ) : Prop := 0 < γ
  46
  47/-- Lattice mass gap: existence of a kernel with PF gap γ. -/
  48def MassGap (_μ : LatticeMeasure) (γ : ℝ) : Prop := ∃ K : Kernel, TransferPFGap (μ:=default) K γ
  49
  50/-- Continuum mass gap: lattice gap persists via stability hypothesis. -/
  51def MassGapCont (γ : ℝ) : Prop := ∃ μ : LatticeMeasure, MassGap μ γ ∧ GapPersists γ
  52
  53/-- OS positivity + PF transfer gap yields a lattice mass gap. -/
  54theorem mass_gap_of_OS_PF {μ : LatticeMeasure} {K : Kernel} {γ : ℝ}
  55    (hOS : OSPositivity μ) (hPF : TransferPFGap μ K γ) : MassGap μ γ := by