resonant_frequency
plain-language theorem explainer
The definition supplies the resonant frequency for harmonic n at φ-sub-harmonic depth k using fundamental tick period τ₀. Researchers deriving frequency ladders in eight-tick gravity models cite it when scaling sub-harmonics on the phi ladder. It is a direct algebraic expression that unfolds immediately in downstream proofs of positivity and monotonic decrease.
Claim. Let τ₀ > 0 be the fundamental tick period. The resonant frequency for harmonic n at sub-harmonic depth k is given by f_{n,k} = n / (8 τ₀ φ^k).
background
The EightTickResonance module works inside the Recognition Science forcing chain at step T7, where the eight-tick octave fixes the base period as 2^3. The golden ratio φ enters as the self-similar fixed point from T6 and appears in the denominator to produce the sub-harmonic ladder. The parameter τ₀ sets the absolute scale while n indexes the harmonic and k the depth on the phi-ladder.
proof idea
This is a direct definition. It is a one-line algebraic expression that unfolds in the proofs of resonant_frequency_pos and resonant_frequency_decreasing.
why it matters
The definition is invoked by resonant_frequency_pos and resonant_frequency_decreasing to establish positivity and strict decrease with k. It supplies the concrete frequency expression required by the eight-tick resonance structure (T7) inside the gravity section, where the period-8 octave and phi scaling together generate the ladder used for later mass and coupling derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.