Masses Channel Cost Sqrt5 Irrational

The irrational step

The square root of 5 is the number that, multiplied by itself, gives 5. It is irrational: it cannot be written as a fraction of two whole numbers. This is a classical fact, known since antiquity, and it follows from a simple observation. If a fraction in lowest terms squared to 5, then the numerator and denominator would both have to be divisible by 5, which is impossible unless both are zero. The Recognition Science library contains a machine-checked proof of this fact, named sqrt5_irrational, which derives it from the primality of 5.

Why does the framework care? In Recognition Science, a ledger (a discrete record of recognition events) assigns a cost to every possible scaling factor. The cost function J(x) = (x + 1/x)/2 - 1 measures the price of recognizing a change of size x. The golden ratio φ, about 1.618, is the unique self-similar scaling in the framework, and its powers appear throughout the theory. The library proves that for any even power of φ, the cost is a rational number, a fraction. For any odd power, the cost is irrational, and the proof of that fact is exactly the irrationality of √5.

Concretely, the cost of φ² is 1/2, a clean rational price. The cost of φ³ is √5/2 - 1, which is irrational because √5 is irrational. This split between even and odd powers is not an accident. The proof shows that φ to an even power plus its conjugate is an integer (a Lucas number), while φ to an odd power minus its conjugate is a Fibonacci number times √5. The irrationality of √5 is what makes the odd powers have irrational costs.

In Recognition Science, this means that the recognition cycle has a built-in irrationality at odd steps. The framework's library proves that the smallest positive power of φ with a rational cost is exactly the second power, φ². This is the theorem minimal_rational_power_eq_two. It uses the irrationality of √5 to rule out all odd powers, and the structure of even powers to find the minimum. So the humble fact that √5 is irrational becomes the reason why the first rational step in the recognition cycle is a two-step, not a one-step.

What the declaration does not claim is just as important. It does not claim that the cost of every odd power is irrational in some physical sense, only that the number is not a fraction. It does not claim that √5 is irrational because of anything specific to Recognition Science; the proof uses only the primality of 5. And it does not claim that the recognition cycle must be eight ticks; that is a separate theorem built from other ingredients. The irrationality of √5 is a supporting lemma, not the whole story.

/-- `√5` is irrational (5 is prime). -/
theorem sqrt5_irrational : Irrational (Real.sqrt 5) := by
  have h : Nat.Prime 5 := by norm_num
  have h2 := Nat.Prime.irrational_sqrt h
  exact_mod_cast h2

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

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

/-- **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 declaration does not claim that irrational costs have a physical interpretation beyond being non-fractional numbers. The declaration does not claim that the irrationality of √5 is a consequence of Recognition Science; it is a classical number-theoretic fact. The declaration does not claim that the recognition cycle is eight ticks; that is a separate theorem.

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: