WindowNeutralPattern
plain-language theorem explainer
A record type holding an 8-tuple of reals whose sum is zero, encoding a neutral modulation pattern over one 8-tick cycle. Device modelers and biophysics researchers cite it when constructing RS-coherent PBM hardware specifications. The definition is a direct structure declaration that packages the values map and the sum-zero constraint with no further lemmas.
Claim. A window-neutral pattern is a function $v : [8] → ℝ$ such that $∑_{k=0}^7 v(k) = 0$.
background
The module formalizes photobiomodulation devices whose energy rungs follow the φ-ladder E(n) = E_base · φ^n, with rung 6 yielding the therapeutic wavelength ≈766 nm. The eight-tick cycle is the octave period fixed by Recognition Science (T7). Neutrality of the modulation pattern prevents net recognition strain accumulation, consistent with the Recognition Composition Law.
proof idea
Structure definition that directly introduces the fields values : Fin 8 → ℝ and neutral : sum values = 0. No upstream lemmas are invoked; the declaration itself supplies the type used by rs_neutral_pattern and PBMDeviceSpec.
why it matters
Supplies the modulation_pattern field inside PBMDeviceSpec, the top-level RS-coherent device specification whose every component derives from φ. It realizes the 8-beat neutrality condition stated in the module doc, closing the link between the eight-tick octave (T7) and practical light-therapy hardware. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.