entrainmentConfidence_pos
plain-language theorem explainer
Engineers specifying the cortical neuromodulation device rely on the fact that entrainment confidence at any phi-rung k remains strictly positive. The quantity equals one divided by phi to the power k. This positivity is required to certify the device parameters. The proof applies standard positivity lemmas for division and exponentiation in a single step.
Claim. For every natural number $k$, $0 < 1/phi^k$.
background
The module specifies a transcranial neuromodulation device operating at cortical-column resonance frequency of 5 phi hertz, with pulse spacing tau equal to one over 5 phi seconds. Entrainment confidence is introduced as the function assigning to each natural number k the value one divided by phi to the power k. The upstream definition states: Confidence at phi-rung k (relative to baseline 1): 1 over phi to the k. This definition appears in the same module and serves as the basis for the device certificate. The local setting includes a falsifier based on EEG studies showing optimal frequency outside the interval from 7.5 to 8.1 hertz.
proof idea
This is a one-line wrapper proof. It invokes div_pos on the positivity of one and the result of pow_pos applied to the positivity of phi.
why it matters
The theorem supplies the positivity field required by the cortical neuromodulation device certificate definition. It supports the engineering derivation in track J10 of plan v5, aligning with the phi-ladder structure. The result closes the positivity check for the confidence values used in pulse scheduling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.