Encyclopedia Masses Masses Channel Cost Phi Pow Sub Conj Eq Fib Sqrt5
ARTICLE 3 claims 3 theorems
Masses Channel Cost Phi Pow Sub Conj Eq Fib Sqrt5
A proved identity links powers of the golden ratio to Fibonacci numbers, but it says nothing about particle masses or the fine-structure constant.
A bridge between powers and Fibonacci numbers
The golden ratio φ ≈ 1.618 and its conjugate ψ ≈ -0.618 are the two roots of x² = x + 1. A classical identity, sometimes called Binet's formula, states that the n-th Fibonacci number F(n) equals (φⁿ - ψⁿ)/√5. The declaration phi_pow_sub_conj_eq_fib_sqrt5 is the framework's machine-checked version of this fact: for every natural number n, φⁿ - ψⁿ = F(n)·√5. This is a theorem in the framework's library, meaning it is proved from the axioms of the real numbers and the definition of Fibonacci numbers, with no additional assumptions.
The identity is not new mathematics. It has been known since the 18th century, when Jacques Philippe Marie Binet and, independently, Abraham de Moivre derived it. The framework's contribution is to have the statement checked by a machine, so that every step of the proof is verified. The declaration also comes with a companion theorem: φⁿ + ψⁿ is always an integer, the n-th Lucas number. These two identities together show that the golden ratio and its conjugate are not just algebraic curiosities but sit naturally inside the integer sequence of Fibonacci and Lucas numbers.
Within the Recognition Science framework, this identity appears in a file about channel costs, which are a way of pricing configurations in a ledger of recognition events. The framework uses the identity to show that certain costs, when evaluated at powers of φ, are either rational or irrational depending on the parity of the exponent. For even powers, the cost is a rational number; for odd powers, it is irrational. This distinction is used later to single out the power n = 2 as the unique minimal positive power with rational cost, a step in the framework's derivation of the number 2 as a structural constant.
The declaration itself makes no claim about particle masses, the fine-structure constant, or any physical measurement. It is a pure statement about real numbers and integer sequences. The framework's later use of this identity in mass calculations is a separate matter, governed by additional premises that are not part of this theorem. The identity is a bridge between the golden ratio and Fibonacci numbers, nothing more and nothing less.
THEOREM phi_pow_sub_conj_eq_fib_sqrt5 · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Fibonacci differences.** `φⁿ − ψⁿ = F(n)·√5` for every natural `n`. -/
theorem phi_pow_sub_conj_eq_fib_sqrt5 (n : ℕ) :
φr ^ n - ψr ^ n = (Nat.fib n : ℝ) * Real.sqrt 5 := by
have key : ∀ k : ℕ, (φr ^ k - ψr ^ k = (Nat.fib k : ℝ) * Real.sqrt 5)
∧ (φr ^ (k + 1) - ψr ^ (k + 1) = (Nat.fib (k + 1) : ℝ) * Real.sqrt 5) := by
intro k
induction k with
| zero =>
constructor
· simp
· rw [pow_one, pow_one, Nat.fib_one, Nat.cast_one, one_mul]
exact ratio_sub_conj
| succ k ih =>
obtain ⟨hk, hk1⟩ := ih
refine ⟨hk1, ?_⟩
have hφ : φr ^ (k + 2) = φr ^ (k + 1) + φr ^ k := by
have h2 : φr ^ (k + 2) = φr ^ k * φr ^ 2 := by rw [← pow_add]
rw [h2, ratio_sq]; ring
have hψ : ψr ^ (k + 2) = ψr ^ (k + 1) + ψr ^ k := by
have h2 : ψr ^ (k + 2) = ψr ^ k * ψr ^ 2 := by rw [← pow_add]
rw [h2, conj_sq]; ring
have e1 : φr ^ (k + 2) - ψr ^ (k + 2)
= (φr ^ (k + 1) - ψr ^ (k + 1)) + (φr ^ k - ψr ^ k) := by
rw [hφ, hψ]; ring
have hfib : (Nat.fib (k + 2) : ℝ) = Nat.fib k + Nat.fib (k + 1) := by
rw [Nat.fib_add_two]; push_cast; ring
rw [e1, hk1, hk, hfib]
push_cast
ring
exact (key n).1
THEOREM phi_pow_add_conj_int · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Lucas sums are integers.** `φⁿ + ψⁿ` satisfies the Fibonacci recurrence with
integer seeds `2, 1`, so it is an integer for every natural `n`. -/
theorem phi_pow_add_conj_int (n : ℕ) : ∃ L : ℤ, φr ^ n + ψr ^ n = (L : ℝ) := by
have key : ∀ k : ℕ, (∃ L : ℤ, φr ^ k + ψr ^ k = (L : ℝ))
∧ (∃ L : ℤ, φr ^ (k + 1) + ψr ^ (k + 1) = (L : ℝ)) := by
intro k
induction k with
| zero =>
constructor
· exact ⟨2, by norm_num⟩
· refine ⟨1, ?_⟩
rw [pow_one, pow_one, show ((1 : ℤ) : ℝ) = 1 by norm_num]
exact ratio_add_conj
| succ k ih =>
obtain ⟨⟨Lk, hLk⟩, ⟨Lk1, hLk1⟩⟩ := ih
refine ⟨⟨Lk1, hLk1⟩, ⟨Lk + Lk1, ?_⟩⟩
have hφ : φr ^ (k + 2) = φr ^ (k + 1) + φr ^ k := by
have h2 : φr ^ (k + 2) = φr ^ k * φr ^ 2 := by rw [← pow_add]
rw [h2, ratio_sq]; ring
have hψ : ψr ^ (k + 2) = ψr ^ (k + 1) + ψr ^ k := by
have h2 : ψr ^ (k + 2) = ψr ^ k * ψr ^ 2 := by rw [← pow_add]
rw [h2, conj_sq]; ring
have e1 : φr ^ (k + 2) + ψr ^ (k + 2)
= (φr ^ (k + 1) + ψr ^ (k + 1)) + (φr ^ k + ψr ^ k) := by
rw [hφ, hψ]; ring
rw [e1, hLk1, hLk]
push_cast
ring
exact (key n).1
THEOREM jcost_phi_pow_even_rational · jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Even powers have rational price.** For every `m`, `J(φ^(2m)) = (L−2)/2` where
`L` is the `2m`-th Lucas integer. -/
theorem jcost_phi_pow_even_rational (m : ℕ) :
∃ q : ℚ, Cost.Jcost (phi ^ (2 * m)) = (q : ℝ) := by
obtain ⟨L, hL⟩ := phi_pow_add_conj_int (2 * m)
refine ⟨(L - 2 : ℚ) / 2, ?_⟩
unfold Cost.Jcost
rw [inv_pow_even m, phi_eq, hL]
push_cast
ring
/-- **Odd powers have irrational price.** For every `m`, `J(φ^(2m+1)) =
F(2m+1)·√5/2 − 1`, irrational because `F(2m+1) ≥ 1` and `√5` is irrational. -/
theorem jcost_phi_pow_odd_irrational (m : ℕ) :
Irrational (Cost.Jcost (phi ^ (2 * m + 1))) := by
have hfib_ne : Nat.fib (2 * m + 1) ≠ 0 :=
ne_of_gt (Nat.fib_pos.mpr (by omega : 0 < 2 * m + 1))
have hirr : Irrational ((Nat.fib (2 * m + 1) : ℝ) * Real.sqrt 5 - 2) :=
irrational_sub_int (irrational_nat_mul_of_ne_zero sqrt5_irrational hfib_ne) 2
have h2J : 2 * Cost.Jcost (phi ^ (2 * m + 1))
= (Nat.fib (2 * m + 1) : ℝ) * Real.sqrt 5 - 2 := by
unfold Cost.Jcost
rw [inv_pow_odd m, ← sub_eq_add_neg, phi_eq, phi_pow_sub_conj_eq_fib_sqrt5]
ring
rintro ⟨q, hq⟩
apply hirr
refine ⟨2 * q, ?_⟩
rw [← h2J, ← hq]
push_cast
ring
What this page does not claim
This theorem does not derive the fine-structure constant or any particle mass. The identity is not new; it is a classical result known since the 18th century. The theorem does not require the framework's recognition axioms; it holds in ordinary real analysis.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Masses/ChannelCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- How does the framework use the rational-versus-irrational distinction to derive the number 2?
- What are the two named premises that close the base rule for channel costs?
- How does the framework connect channel costs to particle masses?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM phi_pow_sub_conj_eq_fib_sqrt5 · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Fibonacci differences.** `φⁿ − ψⁿ = F(n)·√5` for every natural `n`. -/ theorem phi_pow_sub_conj_eq_fib_sqrt5 (n : ℕ) : φr ^ n - ψr ^ n = (Nat.fib n : ℝ) * Real.sqrt 5 := by have key : ∀ k : ℕ, (φr ^ k - ψr ^ k = (Nat.fib k : ℝ) * Real.sqrt 5) ∧ (φr ^ (k + 1) - ψr ^ (k + 1) = (Nat.fib (k + 1) : ℝ) * Real.sqrt 5) := by intro k induction k with | zero => constructor · simp · rw [pow_one, pow_one, Nat.fib_one, Nat.cast_one, one_mul] exact ratio_sub_conj | succ k ih => obtain ⟨hk, hk1⟩ := ih refine ⟨hk1, ?_⟩ have hφ : φr ^ (k + 2) = φr ^ (k + 1) + φr ^ k := by have h2 : φr ^ (k + 2) = φr ^ k * φr ^ 2 := by rw [← pow_add] rw [h2, ratio_sq]; ring have hψ : ψr ^ (k + 2) = ψr ^ (k + 1) + ψr ^ k := by have h2 : ψr ^ (k + 2) = ψr ^ k * ψr ^ 2 := by rw [← pow_add] rw [h2, conj_sq]; ring have e1 : φr ^ (k + 2) - ψr ^ (k + 2) = (φr ^ (k + 1) - ψr ^ (k + 1)) + (φr ^ k - ψr ^ k) := by rw [hφ, hψ]; ring have hfib : (Nat.fib (k + 2) : ℝ) = Nat.fib k + Nat.fib (k + 1) := by rw [Nat.fib_add_two]; push_cast; ring rw [e1, hk1, hk, hfib] push_cast ring exact (key n).1For every natural number n, φⁿ - ψⁿ = F(n)·√5. phi_pow_sub_conj_eq_fib_sqrt5 · IndisputableMonolith/Masses/ChannelCost.leanTHEOREM phi_pow_add_conj_int · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Lucas sums are integers.** `φⁿ + ψⁿ` satisfies the Fibonacci recurrence with integer seeds `2, 1`, so it is an integer for every natural `n`. -/ theorem phi_pow_add_conj_int (n : ℕ) : ∃ L : ℤ, φr ^ n + ψr ^ n = (L : ℝ) := by have key : ∀ k : ℕ, (∃ L : ℤ, φr ^ k + ψr ^ k = (L : ℝ)) ∧ (∃ L : ℤ, φr ^ (k + 1) + ψr ^ (k + 1) = (L : ℝ)) := by intro k induction k with | zero => constructor · exact ⟨2, by norm_num⟩ · refine ⟨1, ?_⟩ rw [pow_one, pow_one, show ((1 : ℤ) : ℝ) = 1 by norm_num] exact ratio_add_conj | succ k ih => obtain ⟨⟨Lk, hLk⟩, ⟨Lk1, hLk1⟩⟩ := ih refine ⟨⟨Lk1, hLk1⟩, ⟨Lk + Lk1, ?_⟩⟩ have hφ : φr ^ (k + 2) = φr ^ (k + 1) + φr ^ k := by have h2 : φr ^ (k + 2) = φr ^ k * φr ^ 2 := by rw [← pow_add] rw [h2, ratio_sq]; ring have hψ : ψr ^ (k + 2) = ψr ^ (k + 1) + ψr ^ k := by have h2 : ψr ^ (k + 2) = ψr ^ k * ψr ^ 2 := by rw [← pow_add] rw [h2, conj_sq]; ring have e1 : φr ^ (k + 2) + ψr ^ (k + 2) = (φr ^ (k + 1) + ψr ^ (k + 1)) + (φr ^ k + ψr ^ k) := by rw [hφ, hψ]; ring rw [e1, hLk1, hLk] push_cast ring exact (key n).1φⁿ + ψⁿ is always an integer, the n-th Lucas number. phi_pow_add_conj_int · IndisputableMonolith/Masses/ChannelCost.leanTHEOREM jcost_phi_pow_even_rational · jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean
/-- **Even powers have rational price.** For every `m`, `J(φ^(2m)) = (L−2)/2` where `L` is the `2m`-th Lucas integer. -/ theorem jcost_phi_pow_even_rational (m : ℕ) : ∃ q : ℚ, Cost.Jcost (phi ^ (2 * m)) = (q : ℝ) := by obtain ⟨L, hL⟩ := phi_pow_add_conj_int (2 * m) refine ⟨(L - 2 : ℚ) / 2, ?_⟩ unfold Cost.Jcost rw [inv_pow_even m, phi_eq, hL] push_cast ring/-- **Odd powers have irrational price.** For every `m`, `J(φ^(2m+1)) = F(2m+1)·√5/2 − 1`, irrational because `F(2m+1) ≥ 1` and `√5` is irrational. -/ theorem jcost_phi_pow_odd_irrational (m : ℕ) : Irrational (Cost.Jcost (phi ^ (2 * m + 1))) := by have hfib_ne : Nat.fib (2 * m + 1) ≠ 0 := ne_of_gt (Nat.fib_pos.mpr (by omega : 0 < 2 * m + 1)) have hirr : Irrational ((Nat.fib (2 * m + 1) : ℝ) * Real.sqrt 5 - 2) := irrational_sub_int (irrational_nat_mul_of_ne_zero sqrt5_irrational hfib_ne) 2 have h2J : 2 * Cost.Jcost (phi ^ (2 * m + 1)) = (Nat.fib (2 * m + 1) : ℝ) * Real.sqrt 5 - 2 := by unfold Cost.Jcost rw [inv_pow_odd m, ← sub_eq_add_neg, phi_eq, phi_pow_sub_conj_eq_fib_sqrt5] ring rintro ⟨q, hq⟩ apply hirr refine ⟨2 * q, ?_⟩ rw [← h2J, ← hq] push_cast ringFor even powers of φ, the cost is a rational number; for odd powers, it is irrational. jcost_phi_pow_even_rational · jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean