rs_neutral_pattern
plain-language theorem explainer
The declaration packages the explicit RS 8-beat modulation values with their sum-to-zero theorem into the WindowNeutralPattern structure. Device modelers working in the Recognition Science framework cite it when specifying a φ-ladder photobiomodulation source that produces no net recognition strain. The definition is a direct constructor application pairing the pattern function with the neutrality theorem.
Claim. Let $s :$ Fin $8$ $→$ ℝ be the RS modulation pattern with $s(0)=φ$, $s(1)=√2/2$, $s(2)=1-φ$, $s(3)=-√2/2$, $s(4)=φ-2$ (and extended by the explicit definition). Then rs_neutral_pattern is the structure $(s, ∑_{k=0}^7 s(k)=0)$.
background
The Photobiomodulation Device module formalizes an RS-coherent light therapy source whose photon energies lie on the φ-ladder E(n) = E_base · φ^n. The 8-beat modulation pattern is supplied by the sibling definition rs_pattern, obtained from the trigonometric form s(k) = cos(kπ/4) + (1/φ) cos(kπ/2). WindowNeutralPattern is the structure whose fields are a function values : Fin 8 → ℝ together with the proposition that the sum of those values over the full 8-tick cycle equals zero. The upstream theorem rs_pattern_window_neutral proves that the RS pattern satisfies this sum-to-zero condition, which the module doc identifies as the fundamental recognition ledger constraint preventing net strain accumulation.
proof idea
The definition is a one-line wrapper that applies the WindowNeutralPattern constructor directly to the pair (rs_pattern, rs_pattern_window_neutral).
why it matters
rs_neutral_pattern supplies the modulation_pattern field of the canonical RS-coherent PBM device rs_device. It realizes the 8-tick octave neutrality required by the Recognition Science forcing chain (T7), ensuring the therapeutic modulation produces zero net recognition defect. The module documentation states that this neutrality constraint supports the device specification in RS_Biophase_Light_Device_Spec.tex and aligns with the eight-tick period and D = 3 spatial dimensions of the overall framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.