rs_neutral_pattern
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive photon energies or wavelengths on the φ-ladder.
- Does not address biological or clinical efficacy of the device.
- Does not extend the pattern beyond a single 8-tick cycle.
- Does not supply numerical approximations or floating-point implementations.
formal statement (Lean)
236noncomputable def rs_neutral_pattern : WindowNeutralPattern :=
proof body
Definition body.
237 ⟨rs_pattern, rs_pattern_window_neutral⟩
238
239/-- The peak value of the pattern occurs at k=0 and equals φ. -/