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

coherence_exponent_unique

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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.