Masses Ladder Offset Gauge Flatten Offsets Invisible

The invisible offsets

The Recognition Science mass ladder predicts particle masses from a base scale multiplied by powers of the golden ratio. The ladder's bookkeeping splits the exponent into four named integer pieces: a sector offset, a fixed shift of minus five, a rung number, and a fixed shift of minus eight. The declaration flatten_offsets_invisible proves that if you set all three adjustable offsets to zero and fold their combined effect into the rung number, every predicted mass comes out identical to the original formula. In plain terms, the offsets are a gauge: a choice of coordinates that leaves the physics untouched.

The theorem is a rewriting of the master mass formula, not a new model. It says that the four pieces never matter separately; only their sum enters the prediction. The companion theorem sum_identifiable goes further: if two exponent choices predict the same mass at a single charge, their sums must be equal. So the sum is exactly the observable content, no more and no less. The framework's library of machine-checked formal theorems records both results.

The audit would be worthless if everything were unobservable, so the framework checks what the gauge does not absorb. The power of two in the mass law is not absorbable: an integer rung shift multiplies the mass by a power of the golden ratio, and no nonzero power of the golden ratio is rational, so the sector's power of two cannot be traded for rungs. That power remains a visible, measurable claim.

What the declaration does not claim is just as important. It does not say the offsets are physically meaningless; it says their individual values are unobservable, while their sum is forced. It does not claim that all parameters of the mass ladder are unobservable, since the power of two survives. And it does not claim anything about the physical origin of the offsets, only about their mathematical redundancy in the prediction.

/-- **Setting all three offsets to zero and absorbing them into the table is invisible.** The
strongest form: the entire named decomposition can be flattened away. -/
theorem flatten_offsets_invisible (s : Sector) (r Z : ℤ) :
    predictAt s (0 - 0 + (r0 s - 5 + r - 8) - 0) Z = MassLaw.predict_mass s r Z := by
  rw [predict_mass_factored]
  congr 1
  simp only [totalIntExponent]
  ring

theorem predict_mass_factored (s : Sector) (r Z : ℤ) :
    MassLaw.predict_mass s r Z = predictAt s (totalIntExponent s r) Z := by
  unfold MassLaw.predict_mass predictAt Anchor.yardstick Anchor.E_coh
  have hexp : ((totalIntExponent s r : ℤ) : ℝ) + MassLaw.gap_correction Z
      = ((-(5 : ℤ) : ℤ) : ℝ) + ((r0 s : ℤ) : ℝ)
        + (((r : ℤ) : ℝ) - 8 + MassLaw.gap_correction Z) := by
    simp only [totalIntExponent]
    push_cast
    ring
  rw [hexp]
  simp only [Real.rpow_add phi_pos, Real.rpow_intCast]
  ring

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

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

The offsets are physically meaningless; they are unobservable individually, but their sum is forced. All parameters of the mass ladder are unobservable; the power of two remains visible. Anything about the physical origin of the offsets.

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: