Masses Ladder Offset Gauge Power Of Two Not Absorbable

The unabsorbable power of two

In the Recognition Science framework, particle masses are not arbitrary numbers. They are predicted by a formula that multiplies a power of two by a power of the golden ratio, φ ≈ 1.618. The formula is a ladder: each integer rung of the ladder shifts the exponent of φ by one, and the exponent of two is fixed by the particle's sector. The question is whether the two factors can be traded against each other, so that a measurement could not tell them apart.

The framework's machine-checked library of formal theorems answers no. Its theorem power_of_two_not_absorbable states that there is no integer k such that 2 = φ^k. Because the golden ratio is irrational, no nonzero power of φ can equal a rational number, and 2 is rational. Shifting a rung by k multiplies the mass by φ^k, so no rung shift can reproduce the effect of changing the power of two. The two factors are independent, and the exponent of two is observable in principle.

The theorem is a statement about the model's identifiability. It does not say that the power of two has been measured, nor that the mass ladder has been confirmed by experiment. It says that if the framework's mass law is correct, then a measurement that determines a mass with enough precision can in principle distinguish a change in the power of two from any change in the rung number. The theorem is a no-go result for a certain kind of reparameterization, not a positive prediction about any specific particle.

In Recognition Science, this matters because the framework's mass law is not a single formula but a family of formulas related by shifts of the rung index. The library proves that shifting every rung by an integer k and taking k back out of the cycle period leaves every predicted mass unchanged. That is a gauge symmetry: the rung table is not unique. The power of two breaks that symmetry. It is the part of the mass formula that a measurement can see, and it is the part that cannot be absorbed into the ladder.

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

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

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

What this page does not claim

No claim that the power of two has been measured or that any specific particle mass has been confirmed. No claim that the golden ratio is irrational in a way that applies to all powers, only that no integer power equals 2. No claim that the mass ladder is the only possible mass formula, only that within this model the power of two is identifiable.

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: