corticalNeuromodulationDeviceCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish hardware realizability or clinical safety.
- Does not derive the carrier frequency from the forcing chain T0–T8.
- Does not quantify entrainment efficacy in vivo.
- Does not address regulatory or electromagnetic compatibility constraints.
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. -/