pulseSpacing_band

formal source

  46theorem pulseSpacing_pos : 0 < pulseSpacing :=
  47  div_pos one_pos carrier_pos
  48
  49theorem pulseSpacing_band :
  50    (0.123 : ℝ) < pulseSpacing ∧ pulseSpacing < 0.125 := by
  51  unfold pulseSpacing carrier
  52  have h1 := phi_gt_onePointSixOne
  53  have h2 := phi_lt_onePointSixTwo
  54  have h_pos : (0 : ℝ) < 5 * phi := by linarith [phi_pos]
  55  refine ⟨?_, ?_⟩
  56  · rw [lt_div_iff₀ h_pos]; linarith
  57  · rw [div_lt_iff₀ h_pos]; linarith
  58
  59/-! ## §2. Entrainment-confidence ladder -/
  60
  61/-- Confidence at φ-rung `k` (relative to baseline 1): `1 / φ^k`. -/
  62def entrainmentConfidence (k : ℕ) : ℝ := 1 / phi ^ k
  63
  64theorem entrainmentConfidence_zero : entrainmentConfidence 0 = 1 := by
  65  unfold entrainmentConfidence; simp
  66
  67theorem entrainmentConfidence_pos (k : ℕ) : 0 < entrainmentConfidence k :=
  68  div_pos one_pos (pow_pos phi_pos _)
  69
  70theorem entrainmentConfidence_le_one (k : ℕ) : entrainmentConfidence k ≤ 1 := by
  71  unfold entrainmentConfidence
  72  rw [div_le_one (pow_pos phi_pos _)]
  73  exact one_le_pow₀ (le_of_lt one_lt_phi)
  74
  75theorem entrainmentConfidence_strict_anti {k₁ k₂ : ℕ} (h : k₁ < k₂) :
  76    entrainmentConfidence k₂ < entrainmentConfidence k₁ := by
  77  unfold entrainmentConfidence
  78  exact one_div_lt_one_div_of_lt (pow_pos phi_pos _)
  79    (pow_lt_pow_right₀ one_lt_phi h)