Masses Channel Cost Boundary Jcost Phi Pow Irrational Of Odd

The golden ladder's rational costs

The golden ratio, φ ≈ 1.618, has a famous arithmetic personality: its powers mix the Fibonacci numbers (1, 1, 2, 3, 5, 8...) and the Lucas numbers (2, 1, 3, 4, 7, 11...). The Recognition Science framework's cost function J, which measures the price of a recognition event, turns out to read that personality exactly. The theorem jcost_phi_pow_irrational_of_odd states that for any odd power of φ (except the zeroth power), the cost J(φ^n) is an irrational number. In plainer terms: if n is odd and not zero, you cannot write the cost as a simple fraction.

This is not a random curiosity. The framework's library proves a complete classification: J(φ^n) is rational if and only if n is even or n is zero. For even n, the cost is (Lucas_n − 2)/2, which is always a rational number. For odd n, the cost is (Fibonacci_n × √5 − 2)/2, and because √5 is irrational, the whole expression is irrational. The theorem jcost_phi_pow_irrational_of_odd is the odd-n half of that classification, and it relies on the classical fact that the square root of 5 is irrational.

Why should a stranger care? Because the framework uses this ladder to price physical channels. A channel is a way a particle couples, and its cost is a number on this golden ladder. The classification shows that the cheapest positive rational cost on the ladder is exactly 1/2, achieved only at n = 2, the φ² step. If a channel's cost is a positive rational, and an elementary coupling pays the least such cost, then that channel costs exactly one φ²-step. This is the missing premise that would close a long-standing gap in the framework's derivation of particle masses. The theorem does not prove that channels cost 1/2; it proves that if they cost a rational at all, the minimal such cost is 1/2.

In Recognition Science, the library's theorems are machine-checked. This one is a proved theorem, not a conjecture. It is also honest about its limits: it does not say which channels exist, what their costs are, or that any physical channel actually attains the 1/2 cost. It only describes the shape of the ladder. The framework's own boundary theorem states that no banked theorem prices a channel; the choice of cost remains an open premise, now sharpened to a selection principle: a channel cost is a positive rational on the golden ladder, minimal among such, directed upward.

/-- Odd powers have irrational cost: `F_n√5` with `F_n ≥ 1` cannot be rational. -/
theorem jcost_phi_pow_irrational_of_odd (n : ℕ) (hn : ¬ Even n) (hn0 : n ≠ 0) :
    ¬ ∃ q : ℚ, Cost.Jcost (phi ^ n) = (q : ℝ) := by
  rintro ⟨q, hq⟩
  rw [jcost_phi_pow, if_neg hn] at hq
  have hFpos : 0 < Nat.fib n := Nat.fib_pos.mpr (Nat.pos_of_ne_zero hn0)
  have hF : (Nat.fib n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hFpos.ne'
  have eq1 : (Nat.fib n : ℝ) * Real.sqrt 5 = 2 * (q : ℝ) + 2 := by linarith [hq]
  have hmem : Real.sqrt 5 ∈ Set.range ((↑) : ℚ → ℝ) := by
    refine ⟨(2 * q + 2) / (Nat.fib n : ℚ), ?_⟩
    rw [Rat.cast_div]
    push_cast
    rw [div_eq_iff hF]
    exact eq1.symm.trans (mul_comm _ _)
  exact sqrt5_irrational hmem

/-- **THEOREM (rationality classification).** `J(φ^n)` is rational iff `n = 0` or `n` is
    even. This corrects the attack prompt's conjecture (rationals only at `n = 0, 2`): every
    even power is rational — but see `jcost_phi_sq_minimal` for the true uniqueness. -/
theorem jcost_phi_pow_rational_iff (n : ℕ) :
    (∃ q : ℚ, Cost.Jcost (phi ^ n) = (q : ℝ)) ↔ n = 0 ∨ Even n := by
  constructor
  · rintro ⟨q, hq⟩
    by_contra hcon
    push_neg at hcon
    exact jcost_phi_pow_irrational_of_odd n hcon.2 hcon.1 ⟨q, hq⟩
  · rintro (rfl | h)
    · refine ⟨0, ?_⟩
      rw [pow_zero, Cost.Jcost_unit0]
      norm_cast
    · refine ⟨((lucas n - 2 : ℤ) : ℚ) / 2, ?_⟩
      rw [jcost_phi_pow_even n h]
      norm_cast

/-- **THEOREM (the φ²-step is the unique minimal positive rational golden cost).** For
    `n ≥ 1` with `J(φ^n)` rational, the cost is at least `1/2 = J(φ²)`, with equality iff
    `n = 2`. The even–Lucas values grow (`1/2, 5/2, 8, …`) and the odd powers are
    irrational, so the smallest positive rational price on the golden ladder is exactly the
    `φ²`-step. -/
theorem jcost_phi_sq_minimal (n : ℕ) (hn : 1 ≤ n)
    (hrat : ∃ q : ℚ, Cost.Jcost (phi ^ n) = (q : ℝ)) :
    1 / 2 ≤ Cost.Jcost (phi ^ n) ∧ (Cost.Jcost (phi ^ n) = 1 / 2 → n = 2) := by
  have hEven : Even n := by
    rcases (jcost_phi_pow_rational_iff n).1 hrat with h0 | hE
    · omega
    · exact hE
  have hn2 : 2 ≤ n := by
    obtain ⟨k, hk⟩ := hEven
    omega
  rcases eq_or_lt_of_le hn2 with h2 | h2
  · subst h2
    rw [RungBaseBoundary.jcost_phi_sq]
    exact ⟨le_refl _, fun _ => rfl⟩
  · have hpow : phi ^ 2 < phi ^ n := pow_lt_pow_right₀ Constants.one_lt_phi h2
    have h1 : 1 ≤ phi ^ 2 := by nlinarith [Constants.one_lt_phi, Constants.phi_pos]
    have hlt := Foundation.jcost_strictMono_one_lt h1 hpow
    rw [RungBaseBoundary.jcost_phi_sq] at hlt
    exact ⟨le_of_lt hlt, fun h => (ne_of_gt hlt h).elim⟩

What this page does not claim

This theorem does not prove that any physical channel costs 1/2. It does not derive the number of channel classes or the existence of fermions. It does not claim that the golden ladder is the only possible cost structure.

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/ChannelCostBoundary.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: