Masses Ladder Offset Gauge Sum Identifiable

The observable sum

The framework's mass law predicts a particle's mass from a few integer labels: a sector, a rung number, and a charge. The formula multiplies a power of two by a power of the golden ratio, with a small correction term. The exponent of the golden ratio is not a single number but a sum of four named pieces: a sector offset, a fixed minus five, the rung number, and a fixed minus eight. The declaration sum_identifiable proves that if two different choices of these labels produce the same predicted mass, then the total exponent must be the same in both cases. In plain language: the sum is exactly what a measurement can see, no more and no less.

This is a theorem about the model, not a new physical assumption. It is proved in the framework's machine-checked library of formal theorems. The theorem's converse is also proved: shifting every rung by a constant and taking that constant back out of the cycle period leaves every mass unchanged. The same holds for flattening all three offsets to zero. These results together mean the individual offsets and rung numbers are not separately observable; only their total enters the mass prediction.

The theorem does not claim that the mass law itself is correct. It says nothing about whether the predicted masses match measured particle masses. That comparison is a separate empirical check, not a theorem. The theorem also does not claim that every part of the formula is unobservable. The power of two is not absorbable: no nonzero power of the golden ratio is rational, so the sector's power of two cannot be traded for rungs. That part makes a claim a measurement can see.

What the theorem changes is the status of the model's internal labels. A reader can now treat the total exponent as the physically meaningful quantity and the individual offsets as gauge choices. This is a structural result about the framework's mass law, not a statement about the physical world.

/-- The converse, which is what makes the previous theorems an identifiability statement
rather than a curiosity: predictions agreeing at a single charge already force the sums to
agree. So the sum is exactly the observable content, no more and no less. -/
theorem sum_identifiable (s : Sector) (e₁ e₂ Z : ℤ) (h : predictAt s e₁ Z = predictAt s e₂ Z) :
    e₁ = e₂ := by
  unfold predictAt at h
  have h2pos : (0 : ℝ) < (2 : ℝ) ^ (B_pow s) := zpow_pos (by norm_num) _
  have hphi : phi ^ ((e₁ : ℝ) + MassLaw.gap_correction Z)
      = phi ^ ((e₂ : ℝ) + MassLaw.gap_correction Z) :=
    mul_left_cancel₀ (ne_of_gt h2pos) h
  have hlog := congrArg Real.log hphi
  rw [Real.log_rpow phi_pos, Real.log_rpow phi_pos] at hlog
  have hne : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
  have : ((e₁ : ℝ)) = ((e₂ : ℝ)) := by
    have := mul_right_cancel₀ hne hlog
    linarith
  exact_mod_cast this

/-- **A different rung table predicts identically.** Shift every rung by `k` and take `k` back
out of the cycle period: no mass anywhere changes. Stated against the master formula, so it is
a claim about the model and not about the rewriting. -/
theorem rung_shift_absorbs_offset (s : Sector) (r k Z : ℤ) :
    predictAt s (totalIntExponent s (r + k) - k) Z = MassLaw.predict_mass s r Z := by
  rw [predict_mass_factored]
  congr 1
  simp only [totalIntExponent]
  ring

/-- **The power of two is not absorbable.** An integer rung shift multiplies the mass by a
power of `φ`, and no nonzero power of `φ` is rational, so the sector's power of two cannot be
traded for rungs. `B_pow` therefore makes a claim a measurement can see. -/
theorem power_of_two_not_absorbable :
    ¬ ∃ k : ℤ, (2 : ℝ) = phi ^ k := by
  rintro ⟨k, hk⟩
  have h1 : (1 : ℝ) ≤ phi := phi_ge_one
  rcases le_or_lt k 0 with hle | hpos
  · have hup : phi ^ k ≤ 1 := by
      calc phi ^ k ≤ phi ^ (0 : ℤ) := zpow_le_zpow_right₀ h1 hle
        _ = 1 := by simp
    rw [← hk] at hup
    norm_num at hup
  · rcases eq_or_lt_of_le (show (1 : ℤ) ≤ k by omega) with heq | hgt
    · rw [← heq, zpow_one] at hk
      linarith [phi_lt_two]
    · have hge : phi ^ (2 : ℤ) ≤ phi ^ k := zpow_le_zpow_right₀ h1 (by omega)
      have hsq : phi ^ (2 : ℤ) = phi + 1 := by
        rw [show (2 : ℤ) = ((2 : ℕ) : ℤ) by norm_num, zpow_natCast]
        exact phi_sq_eq
      rw [hsq, ← hk] at hge
      linarith [one_lt_phi]

What this page does not claim

This theorem does not claim that the mass law's predictions match measured particle masses. This theorem does not claim that the individual offsets and rung numbers are physically meaningful. This theorem does not claim that the power of two is observable, only that it is not absorbable into the rung shift.

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/LadderOffsetGauge.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: