Encyclopedia Constants Constants Phi Ladder Fibonacci Identifiability Threshold Bounds

ARTICLE 4 claims 4 theorems

Constants Phi Ladder Fibonacci Identifiability Threshold Bounds

A number near 0.236 is the tolerance limit that lets one tell which rung of the golden-ratio ladder a value came from.

Verify this page

The identifiability threshold

The golden ratio φ is the positive solution of φ² = φ + 1, about 1.61803398875. Raising it to whole-number powers gives a ladder of values, and each rung can be written as a Fibonacci pair: φⁿ equals a Fibonacci number times φ plus the previous Fibonacci number. For instance, φ³ is 2φ + 1 and φ⁻³ is 2φ − 3. This ladder appears in the Recognition Science framework as a way of indexing physical constants, with the strong coupling route sitting at the rung φ⁻³.

The identifiability threshold is a tolerance bound. The framework's machine-checked library of formal theorems proves that a value close to one rung cannot also be close to a different rung, once the relative error is small enough. The bound is φ⁻³, and the library pins it between 0.2360 and 0.2361. If a candidate value x is within a relative error c·φᵐ of rung m and within the same relative error of rung n, and c is no larger than φ⁻³, then m must equal n. The rung is recoverable from the number.

The proof rests on the arithmetic of the ladder. Every rung φⁿ equals a Fibonacci pair, and φ is irrational, so the pair of integer coefficients is unique: no two different rungs share a value. A separate theorem shows the ladder map from integers to reals is injective. The threshold result sharpens this: even a noisy measurement, with error bounded by the threshold, still identifies the rung. This is the general form of a claim the mass modules prove one particle at a time.

In Recognition Science, the framework models the ladder as a discrete record of recognition events, and the rung of a constant is an arithmetic property of its number, not a modelling choice. The threshold bound is what makes that property stable under small perturbations. It does not say which rung any particular measured constant sits on, nor does it derive the value of φ⁻³ from the cost function; it only states the tolerance within which a rung can be told apart from its neighbours.

THEOREM identifiability_threshold_bounds · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
identifiability_threshold_bounds · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:278 
/-- The threshold, numerically: about 23.6 percent. -/
theorem identifiability_threshold_bounds :
    (0.2360 : ℝ) < phi ^ (-3 : ℤ) ∧ phi ^ (-3 : ℤ) < 0.2361 := by
  have h := phi_zpow_eq_fib (-3)
  have h3 : Int.fib (-3) = 2 := by decide
  have h4 : Int.fib (-3 - 1) = -3 := by decide
  rw [h3, h4] at h
  push_cast at h
  refine ⟨?_, ?_⟩ <;> nlinarith [phi_lower, phi_upper, h]
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 · phi_irrational · int_combination_unique · 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
phi_irrational · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:54 
theorem phi_irrational : Irrational phi := by
  rw [phi_eq_goldenRatio]; exact Real.goldenRatio_irrational
int_combination_unique · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:94 
/-- 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
THEOREM ladder_injective · IndisputableMonolith/Constants/PhiLadderFibonacci.lean
ladder_injective · IndisputableMonolith/Constants/PhiLadderFibonacci.lean:125 
theorem ladder_injective : Function.Injective (fun n : ℤ => phi ^ n) :=
  fun _ _ h => rung_of_value_unique h

What this page does not claim

The threshold bound does not say which rung any particular measured constant sits on. The framework does not derive the value of φ⁻³ from its cost function; the bound is a property of the ladder, not a consequence of the forcing chain. The theorem does not claim that all constants in nature lie on the φ-ladder; it only states the tolerance within which a rung can be identified.

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