Masses Rung Base Boundary

The rung base boundary

The rung base boundary is a result in Recognition Science about the mass ladder, the framework's model where particle masses sit on steps indexed by powers of the golden ratio φ. The base rule states that the number of rungs for a particle species equals twice the number of its active channel classes. The boundary result examines whether this rule is forced by the framework's internal logic or is a contingent choice.

The module RungBaseBoundary.lean proves that the base rule is not forced. It shows that the canonical coefficient 2 can be deformed by any integer k, producing a family of rules where the rung count is (2 + k) times the channel classes, plus a generation torsion term and an anomaly term for the third neutrino. It proves that every such deformation preserves the table's banked structure: the torsion factorization, channel linearity, the overdetermined fit, and the anomaly all hold for any k. However, it also proves that different k values give different observable predictions for the electron mass, so the coefficient is not a gauge freedom; it is a contingent fact about the model.

The module then names the missing premise that would close the base rule. It proves that if each coupled gauge channel costs one φ²-step of the ladder, which has a recognition price of 1/2, then the base rule base = 2 * channels is forced. This is the exact shape a derivation must take, but the premise itself is in no current module; it remains an open assumption.

In plain language, the rung base boundary establishes that Recognition Science's mass ladder does not uniquely determine the base rule for particle masses. The framework's structure allows a family of rules, all internally consistent, but only one matches observations. The module identifies the specific premise that would select the observed rule, but that premise is not yet derived from the framework's axioms.

/-- **Every deformation keeps the table's banked structure.** At every `k`, each rung is
the channel base (with coefficient `2 + k`) plus the derived generation torsion, plus
the third-neutrino anomaly of exactly two. -/
theorem shiftedRungs_factors (k : ℤ) (f : Fermion) :
    shiftedRungs k f
      = (2 + k) * activeChannelClasses f + Integers.tau (genOf f).val
        + (if f = Fermion.nu3 then 2 else 0) := by
  cases f <;>
    simp [shiftedRungs, rung, activeChannelClasses, couplesToCharge, couplesToColor,
      tildeQ, sectorOf, genOf, Integers.tau, Anchor.E_passive, Anchor.W,
      passive_field_edges, cube_edges, active_edges_per_tick, D, wallpaper_groups] <;>
    omega

/-- **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

/-- **The boundary, as one conjunction.** The canonical coefficient and every
deformation satisfy the table's entire banked structure (torsion factorization,
channel linearity, the overdetermined fit, the anomaly), yet nonzero deformations
change observable predictions. The coefficient is contingent and not gauge. -/
theorem baseRule_contingent_not_gauge :
    (∀ k : ℤ, ∀ f : Fermion,
      shiftedRungs k f
        = (2 + k) * activeChannelClasses f + Integers.tau (genOf f).val
          + (if f = Fermion.nu3 then 2 else 0))
    ∧ (∀ k a b : ℤ, a = 2 + k → a + b = 2 * (2 + k) →
        a + b = (2 + k) * activeChannelClasses Fermion.d)
    ∧ (∀ k : ℤ, k ≠ 0 → ∀ Z : ℤ,
        predictAt .Lepton (deformedTotal k Fermion.e) Z
          ≠ predictAt .Lepton (deformedTotal 0 Fermion.e) Z) :=
  ⟨shiftedRungs_factors, shiftedRungs_overdetermined,
   fun k hk Z => baseRule_predictions_differ k hk Z⟩

/-- **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]

What this page does not claim

The channel-cost premise is not derived from the framework's axioms; it is a named assumption in no current module. The module does not prove that the canonical coefficient 2 is the only one consistent with observations. The rung base boundary does not establish that the mass ladder itself is the correct model of particle masses.

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: