`corticalNeuromodulationDeviceCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.CorticalNeuromodulationDevice
domain: Engineering
line: 93 · 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 93.

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

formal source

  90  confidence_strict_anti : ∀ {k₁ k₂ : ℕ}, k₁ < k₂ →
  91    entrainmentConfidence k₂ < entrainmentConfidence k₁
  92
  93def corticalNeuromodulationDeviceCert : CorticalNeuromodulationDeviceCert where
  94  carrier_band := carrier_band
  95  spacing_pos := pulseSpacing_pos
  96  spacing_band := pulseSpacing_band
  97  confidence_zero := entrainmentConfidence_zero
  98  confidence_pos := entrainmentConfidence_pos
  99  confidence_le_one := entrainmentConfidence_le_one
 100  confidence_strict_anti := @entrainmentConfidence_strict_anti
 101
 102/-- **NEUROMODULATION ONE-STATEMENT.** Cortical-column carrier
 103`5φ ∈ (8.05, 8.10) Hz`; optimal pulse spacing `≈ 124 ms`;
 104entrainment confidence ladder `1/φ^k` strictly anti-monotonic. -/
 105theorem neuromod_one_statement :
 106    (8.05 : ℝ) < carrier ∧ carrier < 8.10 ∧
 107    (0.123 : ℝ) < pulseSpacing ∧ pulseSpacing < 0.125 ∧
 108    (∀ {k₁ k₂ : ℕ}, k₁ < k₂ →
 109      entrainmentConfidence k₂ < entrainmentConfidence k₁) :=
 110  ⟨carrier_band.1, carrier_band.2,
 111   pulseSpacing_band.1, pulseSpacing_band.2,
 112   @entrainmentConfidence_strict_anti⟩
 113
 114end
 115
 116end CorticalNeuromodulationDevice
 117end Engineering
 118end IndisputableMonolith

papers checked against this theorem

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