Encyclopedia Masses Masses Channel Cost

ARTICLE 5 claims 5 theorems

Masses Channel Cost

A simple counting rule, two sides per distinction, forces the base coefficient in a machine-checked theory of particle masses.

Verify this page

Channel cost and the base rule

Channel cost is a counting rule used inside Recognition Science to set the base coefficient in a mass formula. The rule says: each configuration degree of freedom costs one rung, and each gauge channel is one distinction with exactly two sides. Multiply them, one rung per degree of freedom times two sides per channel, and the base coefficient is 2. That is the entire content of the base rule, and the first job is to state it precisely and prove it from those two named premises.

The two premises are explicit. The structure ChannelCostPremises declares: dofOfChannel = 2, meaning a distinction has two sides, and rungPerDof = 1, meaning one rung per degree of freedom. From those two equalities the theorem base_rule_of_channelCostPremises derives, for every fermion f, that the product (rungPerDof * dofOfChannel) * activeChannelClasses f equals 2 * activeChannelClasses f. The proof is a single rewrite: substitute 1 for rungPerDof and 2 for dofOfChannel, then simplify. The coefficient 2 is not assumed; it is forced by the premises.

The premises are not empty. Without them, the coefficient is independent: at deformation k = 2, the coefficient becomes 4 instead of 2, every banked structure of the table survives, and observable predictions change. The theorem channel_cost_independent_without_premises states this in one package: at k = 2, the shifted rungs formula holds with coefficient 4, and the predicted lepton total at deformation 2 differs from the undeformed prediction. So the premises do real work; drop them and the predictions move.

The rest concerns the cost function J on powers of the golden ratio phi. It proves that even powers have rational price: for every m, J(phi^(2m)) = (L - 2)/2 where L is the 2m-th Lucas integer. Odd powers have irrational price: J(phi^(2m+1)) = F(2m+1)*sqrt(5)/2 - 1, irrational because F(2m+1) is nonzero and sqrt(5) is irrational. The theorem minimal_rational_power_eq_two then closes the story: among powers n >= 1 with rational price, the unique minimal one is n = 2. That is the phi^2 step, and it is the only power that achieves the smallest rational cost.

The consequence is concrete. The base coefficient 2 is not a free parameter; it is the forced product of two plain modeling choices, one rung per degree of freedom and two sides per distinction. The phi^2 step is the unique minimal rational power price, which pins down the first nontrivial step in the mass ladder. What a reader can now see is the exact shape of the base rule, the two premises that make it hold, and the proof that without those premises the predictions change.

THEOREM base_rule_of_channelCostPremises · IndisputableMonolith/Masses/ChannelCost.lean
base_rule_of_channelCostPremises · IndisputableMonolith/Masses/ChannelCost.lean:262 
/-- **Under the two named premises the base rule is forced.** The coefficient is
`rungPerDof * dofOfChannel = 1 * 2 = 2`, closing
`RungBaseBoundary.channel_cost_premise_closes_base`. -/
theorem base_rule_of_channelCostPremises (P : ChannelCostPremises) :
    ∀ f : Fermion,
      (P.rungPerDof * P.dofOfChannel : ℕ) * activeChannelClasses f
        = 2 * activeChannelClasses f := by
  intro f
  rw [P.rungPerDof_eq_one, P.dof_eq_two_sides]
  norm_num
THEOREM channel_cost_independent_without_premises · IndisputableMonolith/Masses/ChannelCost.lean
channel_cost_independent_without_premises · IndisputableMonolith/Masses/ChannelCost.lean:273 
/-- **Without the premises, the coefficient is independent.** At deformation `k = 2`
(coefficient 4 instead of 2) every banked structure of the table survives
(`RungBaseBoundary.shiftedRungs_factors`), yet observable predictions change
(`RungBaseBoundary.baseRule_predictions_differ`). -/
theorem channel_cost_independent_without_premises (Z : ℤ) :
    (∀ f : Fermion,
      shiftedRungs 2 f
        = (2 + 2) * activeChannelClasses f + Integers.tau (genOf f).val
          + (if f = Fermion.nu3 then 2 else 0))
    ∧ predictAt .Lepton (deformedTotal 2 Fermion.e) Z
        ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z :=
  ⟨shiftedRungs_factors 2, baseRule_predictions_differ 2 (by norm_num) Z⟩
THEOREM jcost_phi_pow_even_rational · IndisputableMonolith/Masses/ChannelCost.lean
jcost_phi_pow_even_rational · IndisputableMonolith/Masses/ChannelCost.lean:185 
/-- **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
THEOREM jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean
jcost_phi_pow_odd_irrational · IndisputableMonolith/Masses/ChannelCost.lean:196 
/-- **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
THEOREM minimal_rational_power_eq_two · IndisputableMonolith/Masses/ChannelCost.lean
minimal_rational_power_eq_two · IndisputableMonolith/Masses/ChannelCost.lean:216 
/-- **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 premises rungPerDof = 1 and dofOfChannel = 2 are modeling choices, not derived facts. The module does not prove that the base rule is physically correct; it proves the coefficient follows from the premises. The irrationality of odd power prices does not imply anything about the rationality of the physical mass spectrum.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND