entrainmentConfidence_le_one
plain-language theorem explainer
Entrainment confidence at φ-rung k satisfies 1/φ^k ≤ 1 for every natural number k. Neuromodulation device engineers cite the bound when assembling certificates for the φ-rational pulse schedule at 5φ Hz. The proof is a term-mode reduction that unfolds the definition and invokes 1 ≤ φ^k from φ > 1.
Claim. For every natural number $k$, $1/φ^k ≤ 1$, where $φ$ is the golden ratio with $φ > 1$.
background
The module derives the transcranial neuromodulation device (RS_PAT_025) tuned to cortical-column resonance 5φ Hz ≈ 8.09 Hz and pulse spacing τ = 1/(5φ) s. The function entrainmentConfidence k is defined as 1/φ^k, the relative confidence at rung k on the phi-ladder. The result depends on the upstream lemma one_lt_phi establishing 1 < φ, which is proved in Constants and re-exported in PhiSupport and PhiSupport.Lemmas.
proof idea
The term proof unfolds the definition of entrainmentConfidence, rewrites the target via div_le_one using positivity of φ^k, and concludes by applying one_le_pow₀ to le_of_lt one_lt_phi.
why it matters
The bound is used in the construction of corticalNeuromodulationDeviceCert, which packages carrier band, spacing constraints, and confidence properties into the device certificate. It closes the upper-bound step in the engineering derivation for the RS_PAT_025 spec. The module falsifier remains an EEG entrainment study with optimal frequency outside [7.5, 8.1] Hz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.