Encyclopedia Masses Masses Rung Base Boundary Base Rule Predictions Differ

ARTICLE 5 claims 5 theorems

Masses Rung Base Boundary Base Rule Predictions Differ

A machine-checked proof shows that a free parameter in a particle mass table is not a mathematical illusion: changing it changes the predicted electron mass.

Verify this page

The coefficient is real

The Recognition Science framework builds particle masses from a ladder of steps, each step a factor of the golden ratio φ. A table of integer rungs on this ladder assigns each fermion a position. One number in that table, the channel coefficient, multiplies the number of gauge channels a species couples to. The question is whether that coefficient is a genuine physical choice or just a gauge artifact, a relabeling that leaves all predictions untouched.

The framework's machine-checked library of formal theorems settles the question. The theorem baseRule_predictions_differ proves that for any nonzero deformation of the coefficient, the predicted mass of the electron changes. The proof is direct: the electron's total integer exponent moves by exactly the deformation, and the prediction function is injective in that exponent. A gauge symmetry, by contrast, would leave every observable invariant. Since the electron mass moves, the coefficient cannot be dismissed as pure convention.

This result sits inside a larger boundary statement. The same library proves that every deformation, zero or not, preserves the table's entire banked structure: the torsion factorization, the channel linearity, the overdetermined fit that predicts the down quark base from the lepton and up bases, and the third-neutrino anomaly of exactly two rungs. The canonical coefficient and all its deformations are equally consistent with that structure. Yet only the canonical value, the one with zero deformation, matches the measured mass spectrum. The structure alone does not select the coefficient; the coefficient is contingent, a fact about the world, not a theorem about the ladder.

In Recognition Science, this is the difference between a derived constant and a contingent one. The framework proves the scaling law and the ladder; it does not prove that the channel coefficient must be two. A named premise, that each coupled gauge channel costs one φ²-step of the ladder, would close the rule and force the coefficient, but that premise lives in no current module. The theorem's power is negative and precise: it rules out the cheap escape of calling the coefficient gauge. Whatever the coefficient is, it is observable, and the electron's mass is the witness.

THEOREM baseRule_predictions_differ · IndisputableMonolith/Masses/RungBaseBoundary.lean
baseRule_predictions_differ · IndisputableMonolith/Masses/RungBaseBoundary.lean:164 
/-- **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
THEOREM baseRule_total_moves · IndisputableMonolith/Masses/RungBaseBoundary.lean
baseRule_total_moves · IndisputableMonolith/Masses/RungBaseBoundary.lean:157 
/-- **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]
THEOREM shiftedRungs_factors · shiftedRungs_overdetermined · shiftedRungs_nu3_anomaly · IndisputableMonolith/Masses/RungBaseBoundary.lean
shiftedRungs_factors · IndisputableMonolith/Masses/RungBaseBoundary.lean:118 
/-- **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
shiftedRungs_overdetermined · IndisputableMonolith/Masses/RungBaseBoundary.lean:131 
/-- **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
shiftedRungs_nu3_anomaly · IndisputableMonolith/Masses/RungBaseBoundary.lean:142 
/-- **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
THEOREM baseRule_contingent_not_gauge · IndisputableMonolith/Masses/RungBaseBoundary.lean
baseRule_contingent_not_gauge · IndisputableMonolith/Masses/RungBaseBoundary.lean:174 
/-- **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⟩
THEOREM channel_cost_premise_closes_base · IndisputableMonolith/Masses/RungBaseBoundary.lean
channel_cost_premise_closes_base · IndisputableMonolith/Masses/RungBaseBoundary.lean:193 
/-- **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 theorem does not prove that the channel coefficient must be two. The theorem does not prove that the canonical coefficient matches the measured mass spectrum. The theorem does not derive the electron mass from first principles.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND