entrainmentConfidence_strict_anti
plain-language theorem explainer
Entrainment confidence at φ-rung k equals 1/φ^k and is strictly decreasing in the natural-number index k. Device engineers cite the result to confirm the anti-monotonic ladder in the cortical neuromodulation specification. The proof is a one-line term that unfolds the definition and invokes the reciprocal inequality on strictly increasing phi-powers.
Claim. For natural numbers $k_1 < k_2$, the entrainment confidence at rung $k_2$ satisfies $1/φ^{k_2} < 1/φ^{k_1}$, where entrainment confidence at rung $k$ is defined by $1/φ^k$ and $φ$ denotes the golden ratio.
background
The module derives the transcranial neuromodulation device (RS_PAT_025) that operates at cortical-column resonance $5φ$ Hz ≈ 8.09 Hz with optimal pulse spacing $τ = 1/(5φ)$ s ≈ 124 ms. Entrainment confidence is the function $1/φ^k$ that gives relative confidence at φ-rung $k$ with respect to baseline value 1. The local setting is the engineering derivation track J10 of Plan v5, whose falsifier is an EEG study placing optimal entrainment outside the interval [7.5, 8.1] Hz.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of entrainmentConfidence, then applies one_div_lt_one_div_of_lt to the pair consisting of the positivity of phi-powers and the strict power inequality pow_lt_pow_right₀ instantiated with one_lt_phi and the hypothesis k₁ < k₂.
why it matters
The theorem supplies the strict anti-monotonicity of the entrainment-confidence ladder and is invoked directly by corticalNeuromodulationDeviceCert and neuromod_one_statement. It completes the φ-rational pulse-schedule step in the Recognition Science engineering derivation, supporting the phi-ladder structure (T5–T6) in which higher rungs carry lower relative confidence. It touches the open empirical question of EEG validation for the 5φ resonance band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.