Masses Ladder Offset Gauge Predict At

The mass prediction

Particle masses in this framework come from a ladder of rungs. Each rung is a whole number, and the mass is a power of the golden ratio φ raised to that number, multiplied by a fixed power of 2. The declaration predictAt, a function in the machine-checked library of formal theorems, packages this cleanly: given a sector, an exponent, and a correction, it returns the predicted mass directly.

The framework proves that this formula is not a new model. A theorem shows that predictAt is exactly a rewriting of the master mass law, with the integer part of the exponent collected into one number. The formula is 2^(B_pow) times φ^(e + gap_correction), where e is the collected integer exponent and the correction handles the gap between rungs. This is a definitional convenience, not a change in what the framework predicts.

The deeper result is about what a measurement can see. The framework proves that shifting every rung by some amount k, and taking k back out of the cycle period, changes no mass anywhere. The entire named decomposition of the exponent into offsets can be flattened away and the prediction stays identical. The converse also holds: if two predictions agree at a single charge, the sums must agree. So the sum of the exponent pieces is exactly the observable content, no more and no less.

In Recognition Science, this is an identifiability statement. The framework models the mass as depending only on the total exponent, not on how that exponent is split into named pieces. The rung table itself is not directly measurable; only the sum it produces is. This is what makes the ladder a prediction rather than a bookkeeping exercise.

The framework also proves that one piece 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. That power of two makes a claim a measurement can see, which keeps the audit from collapsing into pure unobservability.

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

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

predictAt does not by itself assign values to the sector parameters or the gap correction. The framework does not claim that the rung table itself is directly measurable. This page does not claim that any specific particle mass has been measured against this prediction.

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: