Masses Rung Base Boundary Shifted Rungs Overdetermined

The overdetermined fit

In the Recognition Science framework, particle masses are organized on a ladder of rungs, where each rung is an integer exponent of the golden ratio φ. The framework's mass table assigns each fermion a rung, and a central structural claim, called the base rule, states that a particle's rung equals twice the number of channel classes it couples to, plus a generation term and a small anomaly. The declaration shiftedRungs_overdetermined (a machine-checked theorem in the framework's library of formal theorems) concerns what happens when one deforms this table by adding k rungs per coupled channel class, with k any integer.

The theorem states that the overdetermined fit survives every deformation. In plain terms, the framework's mass table has a built-in consistency check: fitting the channel coefficients on the lepton and up-quark bases predicts the down-quark base. The theorem proves that this prediction holds not just for the canonical table (k = 0) but for every integer k. The down-quark base is always correctly predicted, regardless of the deformation. This means the overdetermined fit, which is the one nontrivial prediction of the table's structure, does not select a unique coefficient. Many different deformations all satisfy the same consistency check.

The theorem also establishes that the third neutrino's anomaly, its departure from the expected rung by exactly two, is invariant under every deformation. The anomaly carries no information about the coefficient either. However, the choices are observably distinct: the theorem baseRule_predictions_differ proves that at any nonzero k, the electron's predicted mass changes. So the coefficient is contingent, not gauge. Different coefficients give different observable predictions, even though they all pass the overdetermined fit.

In Recognition Science, this result is part of a boundary analysis. The canonical coefficient and every deformation satisfy the table's entire banked structure, yet nonzero deformations change observable predictions. The coefficient is therefore a contingent choice, not a forced one. The framework's library explicitly names the missing premise: a channel-cost principle stating that each coupled gauge channel costs one φ²-step of the ladder (recognition price 1/2) would close the base rule and force the coefficient. That premise is in no current module; it remains an open target for derivation.

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

/-- **The anomaly is invariant.** The third neutrino departs by exactly two rungs under
every deformation, so the anomaly carries no information about the coefficient. -/
theorem shiftedRungs_nu3_anomaly (k : ℤ) :
    shiftedRungs k Fermion.nu3
      = (2 + k) * activeChannelClasses Fermion.nu3
        + Integers.tau (genOf Fermion.nu3).val + 2 := by
  rw [shiftedRungs_factors k Fermion.nu3]
  simp

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

What this page does not claim

The theorem does not prove that the base rule coefficient is forced or unique. The theorem does not claim that the deformation is physically realized. The theorem does not establish that the channel-cost premise is true.

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: