Masses Rung Base Boundary Base Rule Contingent Not Gauge

The contingent base rule

In the Recognition Science account, particle masses sit on a ladder of integer exponents of the golden ratio φ. The base rule is the choice that fixes the ladder's starting point: each species of fermion gets a base number of rungs equal to twice the number of gauge channels it couples to. The declaration baseRule_contingent_not_gauge is a machine-checked theorem that this base rule is a real, observable choice, not a mathematical redundancy.

The theorem proves three things together. First, every possible deformation of the base rule, shifting each species by a whole number of extra rungs per channel, still satisfies the table's entire banked structure: the torsion factorization, the channel linearity, the overdetermined fit, and the third-neutrino anomaly. Second, the overdetermined fit survives every deformation, meaning the one nontrivial prediction of the table structure does not select the coefficient. Third, and decisively, different coefficients give different observable predictions: at any nonzero deformation, the electron's predicted mass changes. The electron's integer exponent moves by exactly k when the deformation is k, so the coefficient is observable, not gauge.

What the theorem does not claim is that the base rule is derived from something deeper. The theorem establishes that the coefficient is contingent, not that it is forced. The named premise that would close the base rule, that each coupled gauge channel costs one φ²-step of the ladder with recognition price 1/2, is stated as a theorem with that premise assumed, but the premise itself is in no current module. The base rule remains a choice, now proven to be a choice with observable consequences.

The practical consequence is that the mass ladder's anchor is not an artifact of the formalism. If the base rule were a gauge freedom, changing it would leave all predictions unchanged, and the choice would be meaningless. Instead, the theorem shows that the choice of base rule is exactly the kind of thing that must be explained, not discarded. The framework's library proves the choice is real, and leaves the explanation as an open target.

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

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

/-- **The overdetermined fit survives every deformation.** Fitting the channel
coefficients on the lepton and up bases predicts the down base at every `k`, so the
one nontrivial prediction of `RungTableStructure` does not select the coefficient. -/
theorem shiftedRungs_overdetermined (k a b : ℤ)
    (_hlep : a = 2 + k) (hup : a + b = 2 * (2 + k)) :
    a + b = (2 + k) * activeChannelClasses Fermion.d := by
  have hch : activeChannelClasses Fermion.d = 2 := by
    simp [activeChannelClasses, couplesToCharge, couplesToColor, tildeQ, sectorOf]
  rw [hch]
  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

/-- **Different coefficients give different observable totals.** At any `k`, the
electron's integer exponent moves by exactly `k`. -/
theorem baseRule_total_moves (k : ℤ) :
    deformedTotal k Fermion.e - deformedTotal 0 Fermion.e = k := by
  simp [deformedTotal, shiftedRungs, anchorSectorOf, rung, activeChannelClasses,
    couplesToCharge, couplesToColor, tildeQ, sectorOf]

What this page does not claim

The base rule is not derived from any deeper principle in the current library. The theorem does not state that the canonical coefficient k = 0 is the physically correct one. The theorem does not claim that the channel-cost premise is true, only that it would close the base rule if assumed.

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: