resonant_frequency_pos
plain-language theorem explainer
The theorem shows that the resonant frequency n over 8 tau zero times phi to the k is strictly positive when tau zero exceeds zero and n is a positive natural number. Researchers modeling eight-tick resonance in Recognition Science cite it to keep all sub-harmonic frequencies physically positive. The proof is a direct term-mode verification that unfolds the definition and chains div_pos with mul_pos and pow_pos.
Claim. Let $0 < tau_0$ and $n > 0$ with $k$ any natural number. Then the resonant frequency $n / (8 tau_0 phi^k) > 0$.
background
The module Gravity.EightTickResonance defines resonant frequency as the frequency for harmonic n at phi-sub-harmonic depth k with fundamental tick period tau zero, given by the quotient n over 8 tau zero phi to the k. This construction sits inside the eight-tick octave of Recognition Science, where the period 2 cubed is forced by the T7 step of the unified forcing chain. The theorem depends on the resonant_frequency definition and standard real-number positivity facts.
proof idea
The proof unfolds resonant_frequency to the explicit quotient. It applies div_pos with numerator positivity from hn, then shows the denominator positive by mul_pos of a positive constant, h tau zero, and pow_pos of phi_pos.
why it matters
The result supplies the basic positivity needed for the eight-tick resonance model before statements on weight reduction or off-resonance behavior can be formed. It closes a routine gap in the gravity module tied to the phi-ladder and T7 octave. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.