rs_pattern
plain-language theorem explainer
The rs_pattern definition supplies the eight explicit real values for the RS modulation sequence in photobiomodulation applications. Device designers and biophysics researchers cite it to enforce zero net strain over each 8-beat cycle. The definition proceeds by case distinction on the index in Fin 8, assigning phi or 1-phi or signed sqrt(2)/2 according to the cosine-derived pattern.
Claim. Let $s : Fin 8 → ℝ$ be the function with $s(0) = φ$, $s(1) = √2/2$, $s(2) = 1-φ$, $s(3) = -√2/2$, $s(4) = φ-2$, $s(5) = -√2/2$, $s(6) = 1-φ$, $s(7) = √2/2$, where $φ$ denotes the golden ratio.
background
The photobiomodulation module formalizes an RS-coherent light therapy device built on the φ-energy ladder E(n) = E_base · φ^n. Rung 6 yields E = φ eV and wavelength ≈766 nm inside the red/near-IR therapeutic window. The 8-beat modulation pattern is required to meet the recognition ledger constraint of zero net strain accumulation over a complete cycle, expressed algebraically by cancellation of the φ terms and alternating √2/2 terms.
proof idea
This is a direct noncomputable definition by exhaustive case analysis on the Fin 8 index. No lemmas or tactics are invoked; the eight real values are assigned explicitly to produce the required cancellations.
why it matters
The definition supplies the concrete sequence used by rs_neutral_pattern, rs_pattern_window_neutral, and the component-neutrality theorems. It realizes the eight-tick octave (T7) inside the forcing chain T0-T8 and supplies the modulation that prevents strain accumulation in the φ-ladder device. Downstream results quote the algebraic cancellation φ + (1-φ) + (φ-2) + (1-φ) = 0 together with the signed √2/2 terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.