  29/-! ## §1. Carrier frequency and pulse spacing -/
  30
  31/-- Cortical-column carrier frequency = `5 · φ Hz`. -/
  32def carrier : ℝ := 5 * phi
  33
  34theorem carrier_pos : 0 < carrier := by
  35  unfold carrier; exact mul_pos (by norm_num) phi_pos
  36
  37theorem carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10 := by
  38  unfold carrier
  39  have h1 := phi_gt_onePointSixOne
  40  have h2 := phi_lt_onePointSixTwo
  41  refine ⟨by linarith, by linarith⟩
  42
  43/-- Optimal pulse spacing in seconds (= 1 / carrier). -/
  44def pulseSpacing : ℝ := 1 / carrier
  45
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.