module module

`IndisputableMonolith.Engineering.CorticalNeuromodulationDevice`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (14)

def carrier L32
theorem carrier_pos L34
theorem carrier_band L37
def pulseSpacing L44
theorem pulseSpacing_pos L46
theorem pulseSpacing_band L49
def entrainmentConfidence L62
theorem entrainmentConfidence_zero L64
theorem entrainmentConfidence_pos L67
theorem entrainmentConfidence_le_one L70
theorem entrainmentConfidence_strict_anti L75
structure CorticalNeuromodulationDeviceCert L83
def corticalNeuromodulationDeviceCert L93
theorem neuromod_one_statement L105