C_lag_pos
plain-language theorem explainer
The lag coupling constant is shown strictly positive as the fifth power of the reciprocal of the golden ratio. Workers on resonance weights in the ILG kernel cite the result to guarantee that w_resonant stays at least one everywhere and exceeds one away from integer frequencies. The proof is a one-line term-mode reduction that unfolds the definition and invokes positivity of powers of positive reals.
Claim. $0 < phi^{-5}$, where $phi > 1$ is the self-similar fixed point of the Recognition Composition Law.
background
The lag coupling is introduced in the EightTickResonance module as the fifth power of the reciprocal of the golden ratio. It scales the interpolation cost inside the resonant weight definition, where the cost is the distance to the nearest integer and vanishes at resonance. The module imports the BIT kernel families and the ILG kernel to place the resonance structure inside the gravity construction. Upstream kernel definitions supply context but are not used in this positivity argument.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of the lag coupling and applies pow_pos to the positive inverse of phi.
why it matters
The result is invoked by w_resonant_ge_one to establish that the resonant weight is everywhere at least one and by w_off_resonance to obtain the strict inequality off resonance. It therefore anchors the lower bound for the weight kernel in the gravity sector. Within the Recognition framework it supplies the concrete scale of the lag term that follows from J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.