Constants Phi Ladder Fibonacci Phi Neg Three Mul Succ

The rung that identifies itself

The golden ratio, phi, is the number (1 + sqrt(5))/2, roughly 1.61803398875. It is the positive solution to the equation x^2 = x + 1, which means phi^2 = phi + 1 and phi^(-1) = phi - 1. These identities are classical, known since antiquity. The new declaration, phi_neg_three_mul_succ, states a specific arithmetic consequence: phi^(-3) * (phi + 1) = phi - 1. In words, the negative third power of phi, when multiplied by one more than phi, equals one less than phi.

This identity is a special case of a much broader theorem. The framework's machine-checked library of formal theorems proves that every integer power of phi, positive or negative, can be written as a Fibonacci number times phi plus another Fibonacci number. For example, phi^3 = 2*phi + 1, and phi^(-3) = 2*phi - 3. The general formula is phi^n = F(n)*phi + F(n-1), where F(n) is the nth Fibonacci number, extended to negative indices. This is a theorem in the library, not a definition or a choice.

The deeper consequence is that this representation is unique. Because phi is irrational, no two different pairs of integer coefficients can produce the same real number. So if phi^n = phi^m, then n must equal m. The library proves this injectivity: the map from integers to powers of phi is one-to-one. This means a value like phi^(-3) determines its own rung, or index, unambiguously. You cannot relabel a prediction onto a different rung to make it fit; the rung is an arithmetic property of the number itself, not a modelling choice.

In Recognition Science, this rung is not abstract. The framework indexes its ladder of constants by integers, and the strong coupling route sits at phi^(-3). The identifiability theorem states that if a value x is close to phi^m and also close to phi^n, with a tolerance no larger than phi^(-3) times the value itself, then m and n must be the same. This gives a concrete threshold: about 0.2360, between 0.2360 and 0.2361. The negative third power is the largest tolerance that still guarantees a unique rung. This is the payoff: a measurement with sufficient precision cannot be ambiguous about which rung it came from.

What the declaration does not claim is just as important. It does not claim that any physical quantity equals phi^(-3). It does not claim that the strong coupling constant is measured to be this value. It does not claim that the rung determines any particle mass or coupling by itself. The theorem is purely arithmetic: it establishes an identity and a uniqueness property. The physical application, the identification of a measured value with a rung, is a separate empirical step, not a consequence of this theorem.

/-- The identifiability threshold in closed form: `φ⁻³ · (φ + 1) = φ - 1`. -/
theorem phi_neg_three_mul_succ : phi ^ (-3 : ℤ) * (phi + 1) = phi - 1 := by
  have hne : phi ≠ 0 := phi_ne_zero
  have hp1 : phi + 1 ≠ 0 := ne_of_gt (by linarith [phi_pos])
  have hz : phi ^ (-3 : ℤ) = (phi ^ (3 : ℕ))⁻¹ := by
    rw [show (-3 : ℤ) = -((3 : ℕ) : ℤ) by norm_num, zpow_neg, zpow_natCast]
  rw [hz, phi_cubed, ← phi_inv_eq_sub_one]
  field_simp

/-- **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 ladder_injective : Function.Injective (fun n : ℤ => phi ^ n) :=
  fun _ _ h => rung_of_value_unique h

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

This theorem does not claim that any measured physical constant equals phi^(-3). The rung uniqueness does not by itself assign a mass or coupling to a particle. The identity holds for the real number phi, not for a complex or other algebraic extension.

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: