EightTickResonanceCert
plain-language theorem explainer
The EightTickResonanceCert structure records three properties of the resonance weight kernel: it equals 1 at every integer frequency ratio, exceeds 1 whenever the interpolation cost is positive, and is strictly smaller at resonance than at any off-resonance point. Gravity and acoustic-levitation modelers cite it to certify that the eight-tick ILG kernel reaches its global minimum precisely at synchronized ledger ticks. The declaration is a plain record bundling the three axioms; no further proof steps are performed inside the structure itself.
Claim. Let $w(r) = 1 + C_0 d(r)$ where $d(r) = min({r},1-{r})$ is the distance to the nearest integer. The certificate asserts: (i) $w(n)=1$ for every integer $n$; (ii) $w(r)>1$ whenever $d(r)>0$; (iii) $w(n)<w(r)$ for any integer $n$ and any $r$ with $d(r)>0$.
background
In the EightTickResonance module the interpolation cost $d(r)$ is defined as the distance to the nearest integer, vanishing exactly when the frequency ratio is integer and reaching its maximum of 1/2 at half-integers. The resonant weight is then obtained by the linear lift $w(r)=1+C_0 d(r)$, where $C_0$ is the fixed lag constant imported from Constants. This construction sits inside the eight-tick octave framework (T7) that forces spatial dimension three and supplies the self-similar phi-ladder for mass and frequency scaling.
proof idea
The declaration is a structure definition that simply packages three named properties. Each property is supplied by a sibling lemma already proved in the same module: minimum_at_resonance comes from w_at_resonance, exceeds_off_resonance from w_off_resonance, and resonance_reduces_weight from weight_reduction_at_resonance. No tactics or reductions occur inside the structure; it functions as a typed interface record.
why it matters
EightTickResonanceCert is the canonical interface that the downstream eight_tick_resonance_certified theorem instantiates and that UnconditionalLevitationCert imports to close the resonance leg of the levitation argument. It directly encodes the minimum-weight property required by the ILG time-kernel at the eight-tick resonance points, thereby linking the Recognition Composition Law to the acoustic-phase levitation bridge. The certificate remains open on the concrete numerical value of $C_0$ and on the energy-processing equivalence gap listed in the levitation module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.