pulseSpacing_pos
plain-language theorem explainer
The declaration proves that the optimal pulse spacing for the cortical neuromodulation device is strictly positive. Neuromodulation engineers and device certifiers cite it to confirm the timing parameter remains well-defined in the φ-rational schedule. The proof is a one-line wrapper applying the positivity of division to the unit interval and the carrier frequency.
Claim. $0 < 1/f$ where $f$ is the carrier resonance frequency of the device.
background
The Cortical Neuromodulation Device module derives parameters for transcranial neuromodulation (RS_PAT_025) at cortical-column resonance 5φ Hz, with optimal pulse spacing τ = 1/(5φ) s ≈ 124 ms. pulseSpacing is defined as the reciprocal 1/carrier, where carrier denotes the resonance frequency. carrier_pos in the same module establishes 0 < carrier by unfolding the definition and applying mul_pos with phi_pos.
proof idea
One-line wrapper that applies div_pos to one_pos and carrier_pos.
why it matters
Supplies the spacing_pos field inside corticalNeuromodulationDeviceCert, completing the device certification for track J10. It anchors the φ-rational pulse schedule in the Recognition framework, consistent with the phi-ladder and eight-tick octave. The module falsifier remains an EEG entrainment study outside the [7.5, 8.1] Hz band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.