Constants Phi Ladder Fibonacci Rung Identifiable Of Lt

The identifiable rung

The golden ratio, φ = (1 + √5)/2 ≈ 1.618, has a famous property: its powers can be written as Fibonacci numbers. For any integer n, φ^n equals F(n)·φ + F(n−1), where F is the integer Fibonacci sequence extended to negative indices. The golden ratio is irrational, so this representation is unique: if two integers produce the same real number this way, they are the same integer. This is the classical fact that makes the ladder of powers φ^n identifiable: each rung has a distinct value, and that value can be recovered from the number itself.

The Recognition Science framework uses this ladder as a model of discrete states, where each power of φ is a rung. The question is whether a rung can still be identified when a measurement is noisy. The theorem rung_identifiable answers yes, with a precise condition. If a measured value x is within a relative error c of two different rungs φ^m and φ^n, and the error bound c is at most φ^(−3) ≈ 0.236, then m must equal n. In other words, as long as the relative error is below about 23.6 percent, no single measurement can be ambiguous between two distinct rungs. The proof uses the fact that the rungs are separated by a factor of φ, so the error intervals around them cannot overlap when c is small enough.

This is a theorem about real numbers and error intervals, not a physical claim. It does not say that any particular particle mass or coupling constant sits on this ladder, nor that the framework's rung assignments match experiment. It proves a structural property: the map from integers to powers of φ is injective, and that injectivity survives a bounded amount of relative noise. The threshold φ^(−3) is a property of the golden ratio itself, not of any physical system.

In the framework's library, this result is the general form behind many one-off claims about specific rungs. It says that if a prediction is assigned to a rung, you cannot relabel it to a different rung to make it fit a measurement, provided the measurement error is within the bound. The rung is an arithmetic property of the number, not a modelling choice.

/-- **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

/-- The representation of a real number as `a·φ + b` with integer `a, b` is unique,
because `φ` is irrational. -/
theorem int_combination_unique {a b c d : ℤ}
    (h : (a : ℝ) * phi + (b : ℝ) = (c : ℝ) * phi + (d : ℝ)) : a = c ∧ b = d := by
  have hirr : Irrational phi := phi_irrational
  have hac : a = c := by
    by_contra hne
    have hk : ((a - c : ℤ) : ℝ) ≠ 0 := Int.cast_ne_zero.mpr (sub_ne_zero.mpr hne)
    have hval : phi = ((d - b : ℤ) : ℝ) / ((a - c : ℤ) : ℝ) := by
      rw [eq_div_iff hk]
      push_cast
      linear_combination h
    exact hirr.ne_rational (d - b) (a - c) hval
  refine ⟨hac, ?_⟩
  subst hac
  have : (b : ℝ) = (d : ℝ) := by linarith
  exact_mod_cast this

/-- **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)

What this page does not claim

The theorem does not assign any physical quantity to a rung of the ladder. The theorem does not say that any measured value actually lies near a rung. The theorem does not compare the framework's rung predictions to experimental data.

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: