Masses Rung Base Boundary Channel Cost Premise Closes Base

The closing premise

The recognition framework, a discrete record of events with forced costs, builds particle masses on a ladder of rungs. Each rung is a factor of the golden ratio φ, about 1.618. The base rule says that the starting rung for a particle family equals twice the number of coupled gauge channels it carries. A quark, with two channels, starts at rung 4; a charged lepton, with one, at rung 2. The framework's library, a machine-checked collection of formal theorems, proves this structure holds under every deformation of the rung table.

The open question was why the coefficient is exactly 2. The theorem channel_cost_premise_closes_base supplies the missing premise: each coupled gauge channel costs one φ²-step of the ladder. In cost language, a φ² factor has recognition price 1/2, so two channels cost 1, which forces the base rule. The theorem states this cleanly: if channelCost equals 2, then for every fermion, channelCost times the channel count equals twice the channel count. The proof is a one-line rewrite; the content is in the premise.

The premise itself lives in no current module. The theorem shows the exact shape a derivation must take, but it does not derive the channel cost from deeper principles. The coefficient 2 remains a contingent choice, not a gauge artifact: nonzero deformations change the electron's predicted mass, so the coefficient is observable. The framework names this boundary precisely: the base rule is closed by a premise, not forced by the recognition cost function alone.

/-- **A channel-cost principle closes the base rule.** Under the single named premise
that each coupled gauge channel costs one `φ²`-step of the ladder (recognition price
`1/2`, by `jcost_phi_sq`), the base rule `base = 2 * channels` is forced. This is the
exact shape a derivation must take; the premise itself is in no current module. -/
theorem channel_cost_premise_closes_base
    (channelCost : ℤ)
    (hpremise : channelCost = 2) :
    ∀ f : Fermion,
      channelCost * activeChannelClasses f = 2 * activeChannelClasses f := by
  intro f
  rw [hpremise]

/-- **Two rungs cost exactly half a unit.** The recognition price of a `φ²` factor is
`J(φ²) = 1/2`, by `φ² = φ + 1` and `φ⁻² = 2 - φ`. -/
theorem jcost_phi_sq : Cost.Jcost (phi ^ 2) = 1 / 2 := by
  have hsq : phi ^ 2 = phi + 1 := phi_sq_eq
  have h3 : phi ^ 3 = 2 * phi + 1 := by
    calc phi ^ 3 = phi * phi ^ 2 := by ring
      _ = phi * (phi + 1) := by rw [hsq]
      _ = phi ^ 2 + phi := by ring
      _ = (phi + 1) + phi := by rw [hsq]
      _ = 2 * phi + 1 := by ring
  have hmul : phi ^ 2 * (2 - phi) = 1 := by
    calc phi ^ 2 * (2 - phi) = 2 * phi ^ 2 - phi ^ 3 := by ring
      _ = 2 * (phi + 1) - (2 * phi + 1) := by rw [hsq, h3]
      _ = 1 := by ring
  have hmul' : (2 - phi) * phi ^ 2 = 1 := by rw [mul_comm]; exact hmul
  have hinv : (phi ^ 2)⁻¹ = 2 - phi := (eq_inv_of_mul_eq_one_left hmul').symm
  unfold Cost.Jcost
  rw [hinv, hsq]
  ring

/-- **Different coefficients give different predictions.** At a nonzero deformation the
electron's predicted mass changes, so the coefficient is observable, not gauge. -/
theorem baseRule_predictions_differ (k : ℤ) (hk : k ≠ 0) (Z : ℤ) :
    predictAt .Lepton (deformedTotal k Fermion.e) Z
      ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z := by
  intro h
  have hsum := sum_identifiable .Lepton _ _ Z h
  have hm := baseRule_total_moves k
  omega

What this page does not claim

The channel cost premise is derived from deeper principles; it is a named assumption in no current module. The theorem proves the coefficient is 2; it proves that if the coefficient is 2, the base rule follows. The framework derives the fine-structure constant or any coupling constant from this 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/RungBaseBoundary.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: