Encyclopedia Masses Masses Channel Cost Boundary Rational Minimal Channel Cost Closes Base

ARTICLE 4 claims 4 theorems

Masses Channel Cost Boundary Rational Minimal Channel Cost Closes Base

A theorem about the golden ratio pins down the price of a particle channel, but only if you accept a principle it cannot prove.

Verify this page

The cost of a channel

The golden ratio, the number φ ≈ 1.618, is the unique positive solution to r² = r + 1. It appears in pentagons, in Fibonacci numbers, and in a machine-checked library of formal theorems about particle masses. The library models the cost of a recognition event, a discrete record of an interaction, with a specific function J(x) = (x + 1/x)/2 − 1. A central result proves this is the only cost function satisfying five plain conditions. This page concerns one consequence: the cost of a particle channel, a distinct way a particle can interact.

The library's theorem `rational_minimal_channel_cost_closes_base` states that if a channel's cost is a positive rational number attained on the golden ladder (costs of the form J(φ^n) for whole numbers n), and if it is the smallest such positive rational cost, then that cost is exactly 1/2. The proof is a chain of formal steps. First, the library proves J(φ^n) is rational exactly when n is zero or even. For example, J(φ⁴) = 5/2 and J(φ⁶) = 8. Second, among positive n with rational cost, the minimum is 1/2, achieved only at n = 2, meaning the cost is J(φ²). This closes the base rule: the coefficient 2 in the rung table, the ladder of mass steps, is forced to be 2, not some other number.

The theorem is contingent in the banked kernel, the library's core of accepted theorems. It does not prove that any actual channel has a rational cost. That is a premise, a selection principle, not a derived fact. The theorem's conclusion follows only if you grant that a channel cost is a positive rational on the golden ladder, minimal among such, and directed upward. The library also shows this premise is sharp: shifting the cost by k rungs per channel gives a positive rational only for even k, and the minimum 1/2 occurs at k = 0 and its mirror k = −4, with k = 0 the unique upward choice. No banked theorem prices the channel; the boundary theorem states every integer shift meets every banked clause and nonzero shifts are observably distinct.

What this means in plain terms: the framework has reduced a missing numerical premise to a qualitative principle. The cost is not an arbitrary real number; it is forced to be one of a discrete ladder of rational values. The smallest such value is unique. If you accept that an elementary coupling pays the least such cost, the price is set. The framework does not, and cannot, prove that an elementary coupling is minimal. That is the remaining open step, a target for future derivation, not a result in hand.

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_closes_base · IndisputableMonolith/Masses/ChannelCostBoundary.lean
rational_minimal_channel_cost_closes_base · IndisputableMonolith/Masses/ChannelCostBoundary.lean:289 
/-- **THEOREM (the base rule, conditional on the qualitative premise).** Under a rational,
    minimal per-channel rung count, the channel costs one `φ²`-step and the canonical base
    rule `base = 2 * channels` follows (`RungBaseBoundary.channel_cost_premise_closes_base`).
    The residual premise is qualitative — rationality (the ledger books in calibrated units),
    minimality (an elementary coupling), upward direction (channels lift mass) — not an exact
    number. -/
theorem rational_minimal_channel_cost_closes_base (k : ℕ) (hk : 1 ≤ k)
    (hrat : ∃ q : ℚ, Cost.Jcost (phi ^ k) = (q : ℝ))
    (hmin : ∀ m : ℕ, 1 ≤ m → (∃ q : ℚ, Cost.Jcost (phi ^ m) = (q : ℝ)) → k ≤ m)
    (f : Fermion) :
    (k : ℤ) * activeChannelClasses f = 2 * activeChannelClasses f := by
  have h2 : k = 2 := rational_minimal_channel_cost_eq_two k hk hrat hmin
  exact RungBaseBoundary.channel_cost_premise_closes_base (k : ℤ) (by exact_mod_cast h2) f
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 actual channel has a rational cost. The theorem does not derive the value 1/2 from the five cost conditions alone. The theorem does not establish that an elementary coupling is minimal among all possible couplings.

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