corticalNeuromodulationDeviceCert
plain-language theorem explainer
This definition assembles a concrete certificate object for a transcranial neuromodulation device whose carrier sits at 5φ Hz inside the interval (8.05, 8.10) Hz. Device engineers and neurophysicists cite it when fixing pulse spacing near 124 ms and when invoking the 1/φ^k entrainment ladder. The construction is a direct field assignment that pulls the required bounds and monotonicity statements from sibling lemmas already established in the same module.
Claim. The certificate asserts carrier frequency satisfies $8.05 < 5φ < 8.10$, pulse spacing $τ$ obeys $0 < τ$ and $0.123 < τ < 0.125$, and entrainment confidence $c(k) = φ^{-k}$ satisfies $c(0)=1$, $c(k)>0$ for all $k$, $c(k)≤1$ for all $k$, and $k_1 < k_2$ implies $c(k_2) < c(k_1)$.
background
The module specifies a transcranial neuromodulation device (RS_PAT_025) whose carrier frequency is defined by carrier := 5·φ. The structure CorticalNeuromodulationDeviceCert packages four groups of properties: a numerical band on the carrier, positivity and a 0.123–0.125 s band on pulse spacing, and the four axioms of the entrainment-confidence function entrainmentConfidence(k) := 1/φ^k. Upstream lemmas already establish carrier_band by invoking the numerical bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo, together with the four entrainment theorems that prove positivity, the value 1 at k=0, the upper bound 1, and strict decrease.
proof idea
The definition is a one-line wrapper that constructs the structure by direct field assignment: carrier_band is taken from the sibling theorem carrier_band, spacing_pos and spacing_band from pulseSpacing_pos and pulseSpacing_band, and the four confidence fields from the four corresponding entrainment lemmas. No additional tactics or reductions are performed.
why it matters
The definition supplies the single reference object that realizes the J10 engineering track for RS_PAT_025 inside the Recognition Science framework. It closes the derivation of device parameters from the phi-ladder constants and the eight-tick octave structure, allowing downstream engineering proofs to cite a single certified instance rather than repeated lemmas. The module falsifier remains an EEG entrainment study whose optimal frequency lies outside the interval [7.5, 8.1] Hz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.