rs_pattern_phi_components_neutral
plain-language theorem explainer
The declaration establishes that the φ-dependent entries of the RS 8-beat modulation pattern at even indices sum independently to zero. Photobiomodulation device designers would cite it to confirm that the even components of the pattern introduce no net recognition strain. The proof reduces directly to the piecewise definition of the pattern and applies ring arithmetic for cancellation.
Claim. Let $s$ be the RS-coherent 8-beat modulation pattern on the cycle of length 8. Then $s(0) + s(2) + s(4) + s(6) = 0$.
background
The Applied.PhotobiomodulationDevice module develops Recognition Science foundations for coherent light therapy devices. It defines the φ-energy ladder via E(n) = E_base · φ^n and introduces an 8-beat modulation pattern that enforces neutrality over the octave. The upstream rs_pattern definition supplies the concrete values: phi at index 0, 1-phi at 2, phi-2 at 4, and the matching term at 6, all derived from the trigonometric expression s(k) = cos(kπ/4) + φ^{-1} cos(kπ/2).
proof idea
The proof is a one-line term wrapper. It applies simp only on the rs_pattern definition to substitute the four even-index values, then invokes the ring tactic to execute the algebraic cancellation that yields zero.
why it matters
The result supplies one half of the 8-window neutrality constraint Σ s(k) = 0 required by the module to prevent recognition strain accumulation during treatment. It instantiates the eight-tick octave structure from the forcing chain and isolates the φ-components that align with the energy ladder at rung 6. The parent constraint is the full sum-zero condition stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.