Masses Ladder Offset Gauge Rung Shift Absorbs Offset

The shift that changes nothing

In the Recognition Science model of particle masses, each particle sits on a rung of a ladder, and its mass is computed from a formula that adds several integer offsets: a sector base, a rung number, and a cycle correction. The declaration rung_shift_absorbs_offset proves a plain fact about that formula: if you shift every rung by the same integer k, and then subtract k from the cycle period, the predicted mass does not change at all. The proof is a short algebraic identity in the framework's machine-checked library of formal theorems.

Why should a stranger care? Because it says where the model's freedom actually lives. The formula is built from several named pieces, but the theorem shows that those pieces are not separately meaningful. Only their sum enters the mass. A different choice of rung table, with all rungs moved together, produces exactly the same predictions for every particle. The framework states this as a claim about the model itself, not about a rewriting of the formula.

The stronger form, flatten_offsets_invisible, goes further: you can set all three named offsets to zero, absorb them into the table, and again no mass changes. The entire named decomposition can be flattened away. The converse, sum_identifiable, is what turns this from a curiosity into an identifiability statement: if two predictions agree at a single charge, then the sums of their offsets must already agree. So the sum is exactly the observable content, no more and no less.

The theorem does not claim that everything is unobservable. The same file proves that the power of two in the sector is not absorbable: no nonzero power of φ is rational, so a sector's power of two cannot be traded for rungs. That gives a measurement something real to see. The shift theorem is about the offsets, not about the whole mass law.

In Recognition Science, the mass law is not a free parameter fit; it is derived from the forcing chain that starts from the cost function. The rung shift theorem is a check on that derivation: it shows the model has exactly the right amount of internal freedom, and that the observable content is the sum, not the parts.

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

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

/-- 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 theorem does not claim that the mass law is unobservable; the power of two remains measurable. It does not claim that the offsets are meaningless in every context, only that their sum is the observable content. It does not claim that the mass law itself is derived in this file; that derivation lives elsewhere in the framework.

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: