Encyclopedia Masses Masses Channel Cost Boundary Rational Minimal Channel Cost Eq Two

ARTICLE 4 claims 4 theorems

Masses Channel Cost Boundary Rational Minimal Channel Cost Eq Two

A theorem about the golden ratio pins down the smallest possible cost of a particle channel, but only under conditions the framework itself has not yet proven.

Verify this page

The minimal channel cost

The golden ratio, usually written φ, is the number that solves r² = r + 1, about 1.618. In the Recognition Science framework, a ledger, a discrete record of events, assigns a cost to each recognition event. The framework's central cost function, J, is forced by its own axioms to take the form J(x) = (x + 1/x)/2 - 1. The declaration rational_minimal_channel_cost_eq_two is a theorem about the values this cost function takes when its input is a power of the golden ratio.

The theorem classifies the rational costs on this golden ladder. For a positive whole number 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. The theorem then asks a sharper question: among all positive rational costs on the ladder, which is the smallest? The answer, proved in the machine-checked library of formal theorems, is that the minimum is 1/2, and it is attained only at n = 2. That is, the cost of one φ² step is the unique minimal positive rational cost. The declaration rational_minimal_channel_cost_eq_two states this uniqueness: if a channel's cost is a positive rational on the golden ladder and is minimal among all such costs, then that channel costs exactly one φ² step.

In Recognition Science, this result sharpens a missing premise in the framework's account of particle masses. The base rule for the rung table, which organizes particle masses, needs the coefficient 2 to be justified. The theorem does not prove that coefficient. It proves a conditional statement: if a channel's cost is a positive rational on the golden ladder, and if an elementary coupling pays the least such cost, then the channel costs one φ² step. This closes the base rule only under those two hypotheses, which the framework has not yet derived from its axioms. The theorem also shows that shifting the coefficient by any nonzero integer produces observably different predictions, so no already-proven theorem can price the channel.

The distinction between what is proved and what is assumed is the whole point. The theorem proves the uniqueness of the minimal rational cost. It does not prove that a channel's cost is rational, nor that an elementary coupling is minimal. Those remain open targets. The framework's own boundary theorem states that no banked result prices the channel; the missing premise is now reduced to a qualitative selection principle: channel costs are rational, minimal, and upward-directed. This is a sharper statement than before, but it is still a premise, not a conclusion.

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_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

The theorem does not prove that any channel cost is rational, nor that an elementary coupling is minimal. The theorem does not derive the coefficient 2 in the rung table base rule from the framework's axioms. The theorem does not identify which physical channel, if any, actually pays the minimal cost.

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