`neuromod_one_statement`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.CorticalNeuromodulationDevice on GitHub at line 105.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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.