coherence_exponent_unique
plain-language theorem explainer
The theorem fixes the coherence exponent at 5 by showing that D equals the fourth Fibonacci number while the octave equals the sixth, so their difference is the fifth. Researchers deriving mass ladders or coherence energies in Recognition Science would cite it to remove the exponent as a free parameter. The proof is a one-line term that packages four prior lemmas on the Fibonacci identifications.
Claim. Let $D$ be the spatial dimension and let the octave period be $2^D$. Define the coherence exponent by $2^D - D$. Then $D = F_4$, $2^D = F_6$, and the coherence exponent equals both $F_5$ and 5, where $F_n$ denotes the $n$th Fibonacci number.
background
The module derives the coherence exponent from the Fibonacci constraint that both the spatial dimension and the octave period must belong to the Fibonacci sequence. The Fibonacci function is defined recursively by fib 0 = 1, fib 1 = 1, fib (n+2) = fib n + fib (n+1). D is fixed at 3, which equals fib 4, and the octave is 8, which equals fib 6. The coherence exponent is then defined as octave minus D, yielding the value 5 that appears in the coherence energy E_coh = phi^{-5}.
proof idea
The proof is a term-mode exact that directly assembles the conjunction from the four lemmas D_is_fib_4, octave_is_fib_6, coherence_exponent_is_fib_5, and coherence_exponent_eq_5. No additional tactics are required beyond the exact constructor.
why it matters
This result shows that the coherence energy E_coh = phi^{-5} is fixed by the Fibonacci constraint on dimension rather than chosen freely. It supports downstream mass formulas by supplying the rung offset in the phi-ladder. The derivation aligns with T8 forcing of D = 3 and the eight-tick octave period from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.