WindowNeutralPattern
plain-language theorem explainer
WindowNeutralPattern encodes an 8-tick modulation pattern whose values sum to zero. Device physicists specifying RS-coherent photobiomodulation cite it to enforce neutrality and avoid recognition strain accumulation. The declaration is a bare structure definition with no lemmas or proof steps.
Claim. A structure consisting of a function $v : Fin(8) → ℝ$ together with the condition that the sum of $v(k)$ over the eight indices equals zero.
background
The module sets out RS foundations for photobiomodulation devices that operate on the φ-energy ladder E(n) = E_base · φⁿ. The eight-tick octave (T7) supplies the discrete time window; the 8-beat pattern s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2) is required to obey the neutrality constraint Σ s(k) = 0 so that recognition strain does not accumulate during treatment. WindowNeutralPattern is the minimal structure that records any such pattern.
proof idea
Structure definition. The two fields are declared directly: values as a map from Fin 8 to ℝ and neutral as the equality Finset.univ.sum values = 0. No tactics or upstream lemmas are invoked.
why it matters
Supplies the modulation_pattern field inside PBMDeviceSpec, the top-level RS-coherent device specification. It realizes the 8-window neutrality demanded by the eight-tick octave (T7) and the Recognition Composition Law. The definition therefore bridges the abstract forcing chain to concrete device modulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.