CorticalNeuromodulationDeviceCert
plain-language theorem explainer
The neuromodulation device certificate structure collects the band constraints on the carrier frequency near 8.07 Hz, the pulse spacing interval around 0.124 s, and the monotonic decay properties of the entrainment confidence function 1/φ^k. Engineers working on transcranial neuromodulation devices would reference this certificate to validate device parameters against Recognition Science predictions. The structure is populated by a one-line definition that directly assembles the pre-proved lemmas for each field.
Claim. A certificate for cortical neuromodulation consists of a carrier frequency $c$ obeying $8.05 < c < 8.10$, a pulse spacing $s$ satisfying $0 < s$ and $0.123 < s < 0.125$, and an entrainment confidence $e(k) = φ^{-k}$ for $k ∈ ℕ$ such that $e(0) = 1$, $0 < e(k) ≤ 1$ for all $k$, and $e(k_2) < e(k_1)$ whenever $k_1 < k_2$.
background
The module develops an engineering specification for a transcranial neuromodulation device tuned to cortical-column resonance. Carrier frequency is defined as 5·φ Hz and pulse spacing as its reciprocal. Entrainment confidence at rung k is 1/φ^k, whose positivity, normalization at zero, upper bound of one, and strict decrease are established in sibling theorems. The module states: Transcranial neuromodulation device operates at the cortical-column resonance 5φ Hz ≈ 8.09 Hz, with optimal pulse spacing τ = 1 / (5φ) s ≈ 124 ms. The carrier_band theorem confirms the numerical interval using bounds on φ.
proof idea
The structure declaration enumerates seven fields. Each field is a direct reference to a pre-established lemma: carrier_band supplies the frequency interval, pulseSpacing_pos and pulseSpacing_band supply the spacing constraints, and the four entrainmentConfidence theorems supply the confidence properties. No tactics or reductions occur inside the structure itself.
why it matters
This structure provides the master certificate for the neuromodulation device in the engineering track. It is instantiated by the downstream definition that wires the concrete lemmas into the record. The construction ties the device parameters to the golden-ratio ladder and the predicted cortical resonance near 8.09 Hz, closing one segment of the engineering derivation from the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.