pith. machine review for the scientific record. sign in
theorem proved term proof

neuromod_one_statement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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₁) :=

proof body

Term-mode proof.

 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

depends on (8)

Lean names referenced from this declaration's body.