`carrier_band`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
domain: Engineering
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.CorticalNeuromodulationDevice on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  63
  64theorem entrainmentConfidence_zero : entrainmentConfidence 0 = 1 := by
  65  unfold entrainmentConfidence; simp
  66
  67theorem entrainmentConfidence_pos (k : ℕ) : 0 < entrainmentConfidence k :=

papers checked against this theorem

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