pith. machine review for the scientific record. sign in
theorem proved term proof high

coherence_exponent_unique

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 123theorem coherence_exponent_unique :
 124    D = fib 4 ∧
 125    octave = fib 6 ∧
 126    coherence_exponent = fib 5 ∧
 127    coherence_exponent = 5 := by

proof body

Term-mode proof.

 128  exact ⟨D_is_fib_4, octave_is_fib_6, coherence_exponent_is_fib_5, coherence_exponent_eq_5⟩
 129
 130/-! ## Connection to E_coh -/
 131
 132/-- The coherence energy E_coh = φ^{-5} in RS-native units. -/

depends on (14)

Lean names referenced from this declaration's body.