Encyclopedia Masses Masses Channel Cost Phi Pow Add Conj Int

ARTICLE 5 claims 5 theorems

Masses Channel Cost Phi Pow Add Conj Int

A simple pattern in the powers of the golden ratio: add a power to its conjugate, and you always get a whole number.

Verify this page

The Lucas sum theorem

The golden ratio, usually written φ, is the number about 1.618 that solves the equation x² = x + 1. Its conjugate, often written ψ, is the other solution, about -0.618. The two numbers are tied together: they sum to 1, they differ by the square root of 5, and each satisfies the same quadratic equation. A classical fact about them is that their powers have a hidden integer structure. For any whole number n, the sum φⁿ + ψⁿ is an integer. This is the Lucas number sequence: for n = 0, 1, 2, 3, 4, the sums are 2, 1, 3, 4, 7, and the sequence follows the Fibonacci recurrence, where each term is the sum of the two before it.

The theorem phi_pow_add_conj_int in the framework's machine-checked library of formal theorems establishes exactly this. It states that for every natural number n, there exists an integer L such that φⁿ + ψⁿ equals L. The proof is short and relies on two identities: φ² = φ + 1 and ψ² = ψ + 1. These identities let the sum φⁿ + ψⁿ satisfy the Fibonacci recurrence, and since the first two sums are the integers 2 and 1, every later sum is an integer by induction. The same library also proves the companion fact that φⁿ − ψⁿ equals the n-th Fibonacci number times the square root of 5, which shows that the difference is irrational for every positive n.

In Recognition Science, this integer-sum fact becomes a tool for pricing. The framework models recognition cost, a measure of how expensive it is for a system to register a distinction, and it has a specific cost function J. The library proves that when this cost function is evaluated at an even power of φ, the result is always a rational number, and when evaluated at an odd power, the result is always irrational. This split comes directly from the Lucas sum theorem: even powers use the integer sum directly, while odd powers involve the irrational difference. The framework then proves that the power n = 2 is the unique minimal positive power whose cost is rational, a fact that anchors a step in its derivation of particle mass ratios.

The theorem does not claim that the Lucas sums themselves are prime, nor that they follow any pattern beyond being integers. It does not claim that the cost function J is the only possible cost function, nor that the rationality split at even and odd powers explains why particle masses take the values they do. The theorem is a pure number-theoretic fact, and its use in the framework is an application, not a derivation of the masses themselves. The framework's mass ladder is a separate chain of reasoning that builds on this and other results.

THEOREM phi_pow_add_conj_int · IndisputableMonolith/Masses/ChannelCost.lean
phi_pow_add_conj_int · IndisputableMonolith/Masses/ChannelCost.lean:86 
/-- **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 phi_pow_sub_conj_eq_fib_sqrt5 · IndisputableMonolith/Masses/ChannelCost.lean
phi_pow_sub_conj_eq_fib_sqrt5 · IndisputableMonolith/Masses/ChannelCost.lean:116 
/-- **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 jcost_phi_pow_even_rational · IndisputableMonolith/Masses/ChannelCost.lean
jcost_phi_pow_even_rational · IndisputableMonolith/Masses/ChannelCost.lean:185 
/-- **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
THEOREM jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean
jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean:196 
/-- **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
THEOREM minimal_rational_power_eq_two · IndisputableMonolith/Masses/ChannelCost.lean
minimal_rational_power_eq_two · IndisputableMonolith/Masses/ChannelCost.lean:216 
/-- **The `φ²`-step is the unique minimal positive rational power price.** A power
`n ≥ 1` whose price is rational and minimal among such powers is exactly `2`. -/
theorem minimal_rational_power_eq_two (n : ℕ) (hn : 1 ≤ n)
    (hrat : ∃ q : ℚ, Cost.Jcost (phi ^ n) = (q : ℝ))
    (hmin : ∀ m : ℕ, 1 ≤ m → (∃ q : ℚ, Cost.Jcost (phi ^ m) = (q : ℝ)) →
      Cost.Jcost (phi ^ n) ≤ Cost.Jcost (phi ^ m)) :
    n = 2 := by
  rcases Nat.even_or_odd n with ⟨k, hk⟩ | ⟨k, hk⟩
  · have hk2 : n = 2 * k := by omega
    by_cases hk0 : k = 0
    · omega
    · by_cases hk1 : k = 1
      · omega
      · have hkge2 : 2 ≤ k := by omega
        have htwo_rat : ∃ q : ℚ, Cost.Jcost (phi ^ 2) = (q : ℝ) := by
          have h1 := jcost_phi_pow_even_rational 1
          rwa [show (2 : ℕ) * 1 = 2 by ring] at h1
        have hle := hmin 2 (by norm_num) htwo_rat
        have hlt : Cost.Jcost (phi ^ 2) < Cost.Jcost (phi ^ n) := by
          have h2gt : (1 : ℝ) < phi ^ 2 := by nlinarith [one_lt_phi, phi_pos]
          have hne : phi ^ 2 ≠ 1 := ne_of_gt h2gt
          have hlt' := IndisputableMonolith.Cost.UnitFromMinimality.jcost_lt_pow
            (phi ^ 2) (by positivity) hne k hkge2
          have hpow : (phi ^ 2) ^ k = phi ^ n := by
            rw [← pow_mul, hk2]
          rwa [hpow] at hlt'
        linarith
  · obtain ⟨q, hq⟩ := hrat
    have hirr := jcost_phi_pow_odd_irrational k
    rw [hk] at hq
    exact absurd ⟨q, hq.symm⟩ hirr

What this page does not claim

The Lucas sums are prime or follow any pattern beyond being integers. The cost function J is the only possible cost function. The rationality split alone explains the measured values of particle masses. The theorem derives the fine-structure constant or any other coupling constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND