Encyclopedia Masses Masses Channel Cost Boundary

ARTICLE 5 claims 5 theorems

Masses Channel Cost Boundary

A machine-checked library proves exactly when a particle's mass channel can cost a rational amount, and why the smallest such cost picks the golden ratio squared.

Verify this page

The price of a channel

In the Recognition Science framework, a ledger, a discrete record of recognition events, assigns a cost to each step in a particle's mass ladder. The masses channel cost boundary is the theorem that classifies which costs are possible. The central object is the golden ratio φ, the number satisfying φ² = φ + 1, and the cost function J(x) = (x + 1/x)/2 − 1. The new result, proved in a machine-checked library of formal theorems, says that for a positive integer n, the cost J(φ^n) is a rational number exactly when n is even or n is zero. For odd n, the cost is irrational, involving √5.

The classical fact that makes this useful is the Lucas and Fibonacci connection. For even n, J(φ^n) equals (L_n − 2)/2, where L_n is the nth Lucas number (2, 1, 3, 4, 7, 11, 18, ...). For odd n, it equals (F_n√5 − 2)/2, where F_n is the nth Fibonacci number. So J(φ⁴) = 5/2 and J(φ⁶) = 8, both rational. The theorem sharpens an earlier conjecture that only n = 0 and n = 2 gave rational costs; the truth is stronger: among all positive n with rational cost, the minimum cost is 1/2, and it is attained only at n = 2. That is, J(φ²) = 1/2 is the unique smallest positive rational cost on the golden ladder.

In Recognition Science, this uniqueness becomes a selection principle. The framework models each coupled gauge channel as costing one φ²-step, meaning the per-channel cost is exactly 1/2. The module proves that if a channel's cost is a positive rational on the golden ladder, and an elementary coupling pays the least such cost, then the channel must cost exactly one φ²-step. This closes the base rule that the rung table uses a coefficient of 2, contingent on that cost premise. The proof is a theorem, not a definition: it derives the coefficient from the minimality of the rational cost.

The boundary itself is a conjunction of four proved statements. First, every integer shift k in the per-channel coefficient gives a cost J(φ^(2+k)), which is a positive rational exactly when k is even and k ≠ −2. Second, among those, the minimum 1/2 is attained only at k = 0 and its mirror k = −4, reflecting the symmetry J(x) = J(x⁻¹). Third, any nonzero shift produces observably distinct predictions for the lepton channel, so the shifts are not gauge-equivalent. Fourth, the minimality condition forces k = 2, which closes the base rule. Together these show that no banked theorem prices the channel without the minimality premise; the boundary is the precise statement of what remains contingent.

The practical consequence is that the framework has reduced an exact numerical assumption to a qualitative principle: a channel cost is a positive rational on the golden ladder, minimal among such, and directed upward (mass-lifting). This is a sharper target for future work than the old premise that the cost is simply 1/2. The boundary theorem does not prove that channels do cost 1/2; it proves that if they cost any positive rational at all, the minimal one is forced to be 1/2, and that is the only way to close the base rule.

THEOREM jcost_phi_pow_rational_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean
jcost_phi_pow_rational_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean:213 
/-- **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 jcost_phi_sq_minimal · IndisputableMonolith/Masses/ChannelCostBoundary.lean
jcost_phi_sq_minimal · IndisputableMonolith/Masses/ChannelCostBoundary.lean:233 
/-- **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⟩
THEOREM rational_minimal_channel_cost_eq_two · IndisputableMonolith/Masses/ChannelCostBoundary.lean
rational_minimal_channel_cost_eq_two · IndisputableMonolith/Masses/ChannelCostBoundary.lean:269 
/-- **THEOREM (a rational, minimal channel cost is forced to be two rungs).** If the
    per-channel rung count `k` is a positive natural whose golden cost `J(φ^k)` is rational,
    and `k` is minimal among positive naturals of rational golden cost, then `k = 2`: the
    channel costs exactly one `φ²`-step. -/
theorem rational_minimal_channel_cost_eq_two (k : ℕ) (hk : 1 ≤ k)
    (hrat : ∃ q : ℚ, Cost.Jcost (phi ^ k) = (q : ℝ))
    (hmin : ∀ m : ℕ, 1 ≤ m → (∃ q : ℚ, Cost.Jcost (phi ^ m) = (q : ℝ)) → k ≤ m) :
    k = 2 := by
  have h2rat : ∃ q : ℚ, Cost.Jcost (phi ^ 2) = (q : ℝ) := by
    refine ⟨1 / 2, ?_⟩
    rw [RungBaseBoundary.jcost_phi_sq]
    norm_num
  have hle : k ≤ 2 := hmin 2 (by norm_num) h2rat
  have hEven : Even k := by
    rcases (jcost_phi_pow_rational_iff k).1 hrat with h0 | hE
    · omega
    · exact hE
  obtain ⟨a, ha⟩ := hEven
  omega
THEOREM channel_cost_shift_rational_pos_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean
channel_cost_shift_rational_pos_iff · IndisputableMonolith/Masses/ChannelCostBoundary.lean:331 
/-- **THEOREM (the rational positive shifts are exactly the even nonzero ones).** The
    deformed per-channel cost `J(φ^{2+k})` is a positive rational iff `k` is even and
    `k ≠ -2`. So requiring a rational channel cost halves the deformation family to the even
    shifts (the odd shifts are irrational; `k = -2` is the zero-cost `φ⁰`). -/
theorem channel_cost_shift_rational_pos_iff (k : ℤ) :
    ((∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ)) ∧ 0 < Cost.Jcost (phi ^ (2 + k)))
      ↔ (Even k ∧ k ≠ -2) := by
  rw [jcost_phi_zpow_natAbs]
  set n := (2 + k).natAbs with hn
  have hrat : (∃ q : ℚ, Cost.Jcost (phi ^ (n : ℕ)) = (q : ℝ)) ↔ n = 0 ∨ Even n :=
    jcost_phi_pow_rational_iff n
  have hpos : 0 < Cost.Jcost (phi ^ (n : ℕ)) ↔ n ≠ 0 := by
    constructor
    · intro hp h0
      rw [h0, pow_zero, Cost.Jcost_unit0] at hp
      exact lt_irrefl _ hp
    · intro h0
      have hn1 : 1 ≤ n := by omega
      have h1 : (1 : ℝ) < phi ^ n := by
        have := pow_lt_pow_right₀ Constants.one_lt_phi hn1
        rwa [pow_zero] at this
      have hlt := Foundation.jcost_strictMono_one_lt (le_refl (1 : ℝ)) h1
      rwa [Cost.Jcost_unit0] at hlt
  rw [hrat, hpos]
  constructor
  · rintro ⟨(h0 | hE), hne⟩
    · omega
    · have hE' : Even (2 + k) := (even_natAbs_iff (2 + k)).1 hE
      have hk2 : k ≠ -2 := by
        intro hk2
        apply hne
        rw [hn, hk2]
        decide
      rcases hE' with ⟨a, ha⟩
      exact ⟨⟨a - 1, by omega⟩, hk2⟩
  · rintro ⟨hEk, hk2⟩
    have hE' : Even (2 + k) := by
      rcases hEk with ⟨a, ha⟩
      exact ⟨a + 1, by omega⟩
    have hnE : Even n := (even_natAbs_iff (2 + k)).2 hE'
    have hn0 : n ≠ 0 := by
      intro h0
      rw [hn, Int.natAbs_eq_zero] at h0
      omega
    exact ⟨Or.inr hnE, hn0⟩
THEOREM channel_cost_boundary · IndisputableMonolith/Masses/ChannelCostBoundary.lean
channel_cost_boundary · IndisputableMonolith/Masses/ChannelCostBoundary.lean:404 
/-- **THEOREM (channel cost is kernel-contingent, stratified).** One conjunction:

    1. every integer per-channel shift meets the table's entire banked structure (torsion
       factorization, channel linearity, the ν3 anomaly);
    2. nonzero shifts are observably distinct — the cost is contingent, not gauge;
    3. the shifts keeping the cost a positive rational are exactly the even nonzero ones;
    4. among those, the minimum `1/2` is attained exactly at the canonical `k = 0` and its
       cost mirror `k = -4`;
    5. conditional closure: a per-channel rung count that is positive, rational, and minimal
       among such is forced to be `2`, which closes the base rule.

    So the kernel does not price a gauge channel; but the price, *if* it is a minimal
    positive rational golden cost directed upward, is forced to be the `φ²`-step. -/
theorem channel_cost_boundary :
    (∀ k : ℤ, ∀ f : Fermion,
      shiftedRungs k f
        = (2 + k) * activeChannelClasses f + Integers.tau (genOf f).val
          + (if f = Fermion.nu3 then 2 else 0))
    ∧ (∀ k : ℤ, k ≠ 0 → ∀ Z : ℤ,
        predictAt .Lepton (deformedTotal k Fermion.e) Z
          ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z)
    ∧ (∀ k : ℤ,
        ((∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ))
            ∧ 0 < Cost.Jcost (phi ^ (2 + k)))
          ↔ (Even k ∧ k ≠ -2))
    ∧ (∀ k : ℤ,
        (∃ q : ℚ, Cost.Jcost (phi ^ (2 + k)) = (q : ℝ)) →
        0 < Cost.Jcost (phi ^ (2 + k)) →
        1 / 2 ≤ Cost.Jcost (phi ^ (2 + k))
          ∧ (Cost.Jcost (phi ^ (2 + k)) = 1 / 2 → k = 0 ∨ k = -4))
    ∧ (∀ k : ℕ, 1 ≤ k →
        (∃ q : ℚ, Cost.Jcost (phi ^ k) = (q : ℝ)) →
        (∀ m : ℕ, 1 ≤ m → (∃ q : ℚ, Cost.Jcost (phi ^ m) = (q : ℝ)) → k ≤ m) →
        ∀ f : Fermion, (k : ℤ) * activeChannelClasses f = 2 * activeChannelClasses f) :=
  ⟨shiftedRungs_factors,
   fun k hk Z => baseRule_predictions_differ k hk Z,
   channel_cost_shift_rational_pos_iff,
   channel_cost_shift_minimal,
   fun k hk hrat hmin f => rational_minimal_channel_cost_closes_base k hk hrat hmin f⟩

What this page does not claim

This module does not prove that the per-channel cost is 1/2; it proves a conditional statement. The theorem does not show that all channel costs are rational, only that rational costs occur at even powers of phi. The boundary theorem does not derive the coefficient 2 from the cost axioms alone; it requires the minimality premise.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND