Masses Ladder Offset Gauge

The offset gauge

The masses ladder offset gauge is a bookkeeping device inside Recognition Science's model of particle masses. The model places each particle on a ladder of masses spaced by powers of the golden ratio φ, and the gauge is a way of splitting the exponent on that ladder into named pieces: a sector offset, a rung number, and two fixed constants. The pieces are arbitrary, like choosing where to put the zero mark on a ruler; what matters is their sum. The first theorem, predict_mass_factored, proves that the full mass formula equals a simpler expression in which only the total integer exponent appears. The named pieces are a convenience, not a physical fact.

The central result is that the sum, not the pieces, is the observable content. The theorem rung_shift_absorbs_offset shows that shifting every rung by an integer k and taking k back out of the cycle period leaves every predicted mass unchanged. The stronger flatten_offsets_invisible shows that setting all three offsets to zero and absorbing them into the table is invisible: the predictions are identical. These are not rewritings; they are statements about the model itself. The converse, sum_identifiable, proves that if two exponent sums give the same predicted mass at a single charge, the sums must be equal. So the sum is exactly what a measurement can determine, no more and no less.

The audit would be worthless if everything were unobservable, so the module also proves what the gauge cannot absorb. The theorem power_of_two_not_absorbable states that no nonzero power of φ is rational, and therefore the sector's power of two cannot be traded for rungs. A rung shift multiplies the mass by a power of φ, and since that power is never rational, it cannot cancel a factor of two. The power of two remains a visible, testable claim. This is the boundary of the gauge: it can absorb offsets, but not the sector's fundamental scaling.

In plain terms, the module tells a physicist what the mass ladder can and cannot say. The offsets are a gauge freedom, like the choice of origin in a coordinate system; they carry no information. The single integer sum, and the power of two, are what survive. A measurement that agrees with the model pins down the sum and the power of two, but never the individual offsets. The framework's library, a machine-checked collection of formal theorems, establishes this identifiability result without relying on unstated assumptions.

/-- **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 offset gauge does not change the predicted masses; it only reorganizes the exponent. The module does not prove that the mass ladder itself is correct, only that its offset decomposition is unobservable. The power of two being non-absorbable does not mean the sector offset is measurable; only the sum and the power of two are.

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: