resonant_frequency_decreasing
plain-language theorem explainer
The resonant frequency for harmonic n at φ-sub-harmonic depth k decreases strictly as k increases by one, for any positive fundamental tick period τ₀ and positive integer n. Modelers of sub-harmonic ladders in Recognition Science gravity would cite this monotonicity to order the frequency spectrum. The proof unfolds the explicit formula and compares the denominators using the fact that phi exceeds one.
Claim. Let τ₀ > 0 and n ∈ ℕ with n > 0. Then n / (8 τ₀ ϕ^{k+1}) < n / (8 τ₀ ϕ^k) for any natural number k.
background
The resonant frequency is defined explicitly as n divided by the product of eight times the base period τ₀ and phi raised to the depth k. This places frequencies on a geometric ladder scaled by the golden ratio, consistent with the eight-tick octave structure. The supporting lemma one_lt_phi establishes that phi is strictly greater than one, which drives the growth of the denominator with k.
proof idea
The proof unfolds the definition of resonant_frequency to reach the quotient form. It first records positivity of both denominators via multiplication of positives and power positivity. It then proves the denominator at depth k is smaller than at k+1 by rewriting the successor power and applying nlinarith with one_lt_phi. The final step invokes div_lt_div_of_pos_left on the positive numerator and strictly increasing positive denominators.
why it matters
This monotonicity supports the sub-harmonic ladder in the eight-tick resonance model of the gravity sector. It aligns with the T7 eight-tick octave and the phi-ladder construction in the Recognition framework. No downstream uses are recorded, yet the result closes a basic ordering property required for any spectral analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.