w_total_exceeds_secular
plain-language theorem explainer
The theorem shows that a positive secular weight multiplied by a resonant factor strictly larger than one yields a total kernel strictly larger than the secular weight alone. Modelers of off-resonance corrections in the eight-tick gravity kernel would cite it to bound the excess contribution. The proof is a one-line wrapper that unfolds the product definition of the total kernel and applies the standard real-number multiplication inequality.
Claim. Let $w_s > 0$ and $w_r > 1$ be real numbers. Then $w_s < w_s w_r$, where the total kernel is defined as the product of the secular and resonant factors.
background
In the EightTickResonance module the resonant factor is defined by $w_r(r) = 1 + C_{lag} · interpolation_cost(r)$. This expression equals 1 at integer rung values (resonance) and exceeds 1 off resonance. The total kernel is the product $w_{total}(w_s, w_r) = w_s w_r$. The local setting is the modulation of the ILG weight kernel by the eight-tick resonance structure, where the secular component is scaled by the resonant correction.
proof idea
The term proof first unfolds the definition of the total kernel to expose the product $w_s w_r$. It then applies the lemma lt_mul_of_one_lt_right directly to the two hypotheses $w_s > 0$ and $w_r > 1$.
why it matters
The result supplies the strict inequality required to quantify the weight reduction at resonance relative to off-resonance states, as recorded in the module comment following the proof. It supports the resonance-aware kernel construction that appears in the T7 eight-tick octave analysis and the associated weight-reduction statements in sibling declarations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.