Encyclopedia Constants Constants Phi Ladder Fibonacci

ARTICLE 4 claims 4 theorems

Constants Phi Ladder Fibonacci

The golden ratio's powers form a ladder whose rungs are Fibonacci numbers, and the Recognition Science library proves each rung is uniquely identifiable.

Verify this page

The phi ladder

The golden ratio, φ = (1 + √5)/2 ≈ 1.618, is the positive solution to φ² = φ + 1. This equation means its powers can be written as integer combinations of φ and 1. For example, φ² = φ + 1, φ³ = 2φ + 1, and φ⁴ = 3φ + 2. The coefficients are exactly the Fibonacci numbers: φⁿ = F(n)·φ + F(n−1), where F(0) = 0, F(1) = 1, and each subsequent Fibonacci number is the sum of the previous two.

This identity is classical, but the Recognition Science framework extends it to all integer exponents, including negative ones. The module phi ladder, a sequence of values indexed by integers as powers of the golden ratio, proves that φ⁻¹ = φ − 1, φ⁻² = 2 − φ, and φ⁻³ = 2φ − 3. The general theorem, phi_zpow_eq_fib, states that for every integer n, φⁿ = F(n)·φ + F(n−1), where F is the integer Fibonacci function. This is the version the framework's physics needs, since its constants are indexed by integers, not just natural numbers.

The central result is that each rung of the ladder is uniquely recoverable from its value. Since φ is irrational, the representation φⁿ = aφ + b with integer coefficients a and b is unique. The theorem rung_of_value_unique proves that if φᵐ = φⁿ, then m = n. This means the ladder map from integers to real numbers is injective: no two different rungs share the same value. A corollary, rung_identifiable, extends this to nearby values: if a number x is close enough to two rungs, within a threshold of φ⁻³ ≈ 0.236 times the rung's value, then those rungs must be the same.

In Recognition Science, this uniqueness has a direct consequence for physics. The framework places particle masses on this phi ladder, indexed by integer rungs. The injectivity result proves that a ladder value determines its rung as an arithmetic fact, not a modelling choice. You cannot relabel a prediction onto a different rung to make it fit a measurement, because the rung is a property of the number itself. The library's machine-checked theorems, audited to the standard axioms, establish this general form that the mass modules previously proved one particle at a time.

What this changes is that the phi ladder is no longer a collection of hand-written instances, but a single provable structure. The framework's constants, such as ħ = φ⁻⁵ and G = φ⁵/π, sit on this ladder at specific rungs. The injectivity result guarantees these rungs are well-defined and unambiguous, which is what allows the framework to make precise, falsifiable predictions about particle masses.

THEOREM phi_zpow_eq_fib · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
phi_zpow_eq_fib · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:59 
/-- **Every integer power of φ is a Fibonacci pair.** For all `n : ℤ`,
`φ ^ n = F n · φ + F (n-1)`, where `F` is the Fibonacci sequence extended to the
negative integers.

This is the statement the library's 287 hand-written instances are shadows of, and
unlike Mathlib's natural-exponent version it covers the negative rungs that
Recognition Science actually uses. -/
theorem phi_zpow_eq_fib (n : ℤ) :
    phi ^ n = (Int.fib n : ℝ) * phi + (Int.fib (n - 1) : ℝ) := by
  have hφ : Real.goldenRatio ≠ 0 := Real.goldenRatio_ne_zero
  have hψ : Real.goldenConj ≠ 0 := Real.goldenConj_ne_zero
  have h5 : Real.sqrt 5 ≠ 0 := by positivity
  have hsub : Real.goldenRatio - Real.goldenConj = Real.sqrt 5 :=
    Real.goldenRatio_sub_goldenConj
  rw [phi_eq_goldenRatio, Real.coe_intFib_eq, Real.coe_intFib_eq,
      zpow_sub₀ hφ, zpow_sub₀ hψ, zpow_one, zpow_one]
  -- `φ⁻¹ = -ψ` and `ψ⁻¹ = -φ` are what make the conjugate terms cancel.
  have e1 : Real.goldenRatio ^ n / Real.goldenRatio
      = -(Real.goldenRatio ^ n * Real.goldenConj) := by
    rw [div_eq_mul_inv, Real.inv_goldenRatio]; ring
  have e2 : Real.goldenConj ^ n / Real.goldenConj
      = -(Real.goldenConj ^ n * Real.goldenRatio) := by
    rw [div_eq_mul_inv, Real.inv_goldenConj]; ring
  rw [e1, e2, div_mul_eq_mul_div, ← add_div, eq_div_iff h5, ← hsub]
  ring
THEOREM rung_of_value_unique · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
rung_of_value_unique · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:112 
/-- **The rung is recoverable from the value.** The ladder map `n ↦ φ ^ n` is
injective on `ℤ`, so a ladder value belongs to exactly one rung.

This is the general form of the no-relabelling argument that the mass modules prove
one particle at a time. It says the rung index is an arithmetic property of the real
number, not a choice the modeller gets to make. -/
theorem rung_of_value_unique {m n : ℤ} (h : phi ^ m = phi ^ n) : m = n := by
  have hlog : Real.log (phi ^ m) = Real.log (phi ^ n) := by rw [h]
  rw [Real.log_zpow, Real.log_zpow] at hlog
  have hpos : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
  have hmn : (m : ℝ) = (n : ℝ) := mul_right_cancel₀ hpos hlog
  exact_mod_cast hmn
THEOREM rung_identifiable · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
rung_identifiable · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:261 
/-- **A measurement better than `φ⁻³` in relative precision pins the rung.** If a
value sits within relative distance `c ≤ φ⁻³ ≈ 0.236` of two rungs, those rungs are
the same one.

This is the general form of the per-particle rung-family exclusions: rather than
showing case by case that no integer rung shift rescues a prediction, it bounds once
and for all how loose a measurement has to be before a rung reassignment is even
arithmetically available. -/
theorem rung_identifiable {x c : ℝ} {m n : ℤ}
    (hc : c ≤ phi ^ (-3 : ℤ))
    (hm : |x - phi ^ m| < c * phi ^ m)
    (hn : |x - phi ^ n| < c * phi ^ n) : m = n := by
  rcases lt_trichotomy m n with h | h | h
  · exact absurd (rung_identifiable_of_lt hc h hm hn) (by simp)
  · exact h
  · exact absurd (rung_identifiable_of_lt hc h hn hm) (by simp)
THEOREM phi_zpow_eq_fib · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
phi_zpow_eq_fib · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:59 
/-- **Every integer power of φ is a Fibonacci pair.** For all `n : ℤ`,
`φ ^ n = F n · φ + F (n-1)`, where `F` is the Fibonacci sequence extended to the
negative integers.

This is the statement the library's 287 hand-written instances are shadows of, and
unlike Mathlib's natural-exponent version it covers the negative rungs that
Recognition Science actually uses. -/
theorem phi_zpow_eq_fib (n : ℤ) :
    phi ^ n = (Int.fib n : ℝ) * phi + (Int.fib (n - 1) : ℝ) := by
  have hφ : Real.goldenRatio ≠ 0 := Real.goldenRatio_ne_zero
  have hψ : Real.goldenConj ≠ 0 := Real.goldenConj_ne_zero
  have h5 : Real.sqrt 5 ≠ 0 := by positivity
  have hsub : Real.goldenRatio - Real.goldenConj = Real.sqrt 5 :=
    Real.goldenRatio_sub_goldenConj
  rw [phi_eq_goldenRatio, Real.coe_intFib_eq, Real.coe_intFib_eq,
      zpow_sub₀ hφ, zpow_sub₀ hψ, zpow_one, zpow_one]
  -- `φ⁻¹ = -ψ` and `ψ⁻¹ = -φ` are what make the conjugate terms cancel.
  have e1 : Real.goldenRatio ^ n / Real.goldenRatio
      = -(Real.goldenRatio ^ n * Real.goldenConj) := by
    rw [div_eq_mul_inv, Real.inv_goldenRatio]; ring
  have e2 : Real.goldenConj ^ n / Real.goldenConj
      = -(Real.goldenConj ^ n * Real.goldenRatio) := by
    rw [div_eq_mul_inv, Real.inv_goldenConj]; ring
  rw [e1, e2, div_mul_eq_mul_div, ← add_div, eq_div_iff h5, ← hsub]
  ring

What this page does not claim

The phi ladder does not prove the values of physical constants; it only establishes the arithmetic structure of the ladder itself. The injectivity theorem does not say that every real number is close to a ladder rung, only that nearby rungs are identifiable within the threshold. The module does not derive the fine-structure constant or any other specific 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/Constants/PhiLadderFibonacci.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