modes_span_distinct_bands
plain-language theorem explainer
The theorem establishes that the frequencies phi cubed, phi to the fifth, and phi to the eighth are strictly increasing. Device designers following the Recognition Science photobiomodulation specification would cite this to confirm the theta, alpha, and gamma modes occupy distinct EEG bands. The proof constructs the conjunction and applies linear arithmetic directly to the bounding lemmas for each power of phi.
Claim. The theta, alpha, and gamma mode frequencies satisfy $phi^3 < phi^5 land phi^5 < phi^8$.
background
In the Recognition Science photobiomodulation module the device modes receive frequencies from the phi-ladder: theta at phi cubed hertz, alpha at phi to the fifth, and gamma at phi to the eighth. These derive from the energy ladder E(n) = E_base · phi^n with E_coh = phi^{-5} eV, so that rung 6 yields the therapeutic wavelength near 766 nm. Upstream lemmas supply the concrete bounds: phi cubed lies between 4.0 and 4.25, phi fifth between 10.7 and 11.3, and phi eighth between 30 and 100, the last placing it inside the gamma EEG band.
proof idea
The term proof opens with constructor to split the conjunction. The first inequality is discharged by linarith on the upper bound of phi cubed and the lower bound of phi fifth. The second inequality is discharged by linarith on the upper bound of phi fifth and the lower bound of phi eighth supplied by phi_eighth_in_gamma_band.
why it matters
The result is invoked by the rs_device definition to guarantee the canonical RS-coherent PBM specification has non-overlapping frequency assignments. It directly implements the module claim that the three modes span distinct ranges and reinforces the eight-tick octave structure together with the placement of successive phi powers inside EEG bands. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.