pith. machine review for the scientific record. sign in
def definition def or abbrev

corticalNeuromodulationDeviceCert

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)

  93def corticalNeuromodulationDeviceCert : CorticalNeuromodulationDeviceCert where
  94  carrier_band := carrier_band

proof body

Definition body.

  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. -/

depends on (12)

Lean names referenced from this declaration's body.