Masses Mass Law Gap Correction

The charge shift term

The recognition framework, a system that treats reality as a discrete record of events, proposes a master formula for particle masses. In this account, each stable particle sits on a rung of a ladder where each step multiplies mass by the golden ratio, about 1.618. The formula is m = yardstick(Sector) × φ^(r − 8 + gap(Z)), where the yardstick is a sector-specific prefactor, r is an integer rung, 8 is the fundamental cycle period, and Z is a charge-based shift index.

The term gap_correction is defined as gap(Z) = log_φ(1 + Z/φ). It is a mathematical definition, not a derived physical law. For a neutral baseline with Z = 0, the correction is exactly zero, a fact proved in the machine-checked library of formal theorems. The library also proves that increasing the rung by one scales the predicted mass by exactly φ, and that any valid configuration yields a positive mass.

In plain language, the gap term nudges the rung position based on electric charge. A positive Z shifts the effective rung upward, a negative Z downward, and the size of the shift follows a logarithmic curve. The definition is exact: it is a specific function of Z and the golden ratio, nothing vaguer.

What this declaration does not do is more important than what it does. The gap_correction definition is a model, a chosen functional form, not a theorem derived from the framework's first principles. The framework's own documentation describes it as a correction term, but the chain of reasoning that would force this particular logarithmic form from the recognition ledger is not present in the library. The physical bridge from recognition events to particle masses, and to this charge shift specifically, remains open.

/-- The recognition gap correction term: gap(Z) = log_φ(1 + Z/φ).
    This term corrects the rung position based on the charge-induced skew. -/
noncomputable def gap_correction (Z_val : ℤ) : ℝ :=
  Real.log (1 + (Z_val : ℝ) / phi) / Real.log phi

/-- The "gap" term corrects for the charge-based shift.
    When Z=0 (neutral sector baseline), gap(0) = 0. -/
theorem gap_zero_neutral : gap_correction 0 = 0 := by
  unfold gap_correction
  simp only [Int.cast_zero, zero_div, add_zero, Real.log_one, zero_div]

/-- The mass law exhibits φ-scaling: increasing rung by 1 scales mass by φ. -/
theorem mass_rung_scaling (s : Sector) (r : ℤ) (Z_val : ℤ) :
    predict_mass s (r + 1) Z_val = phi * predict_mass s r Z_val := by
  unfold predict_mass
  -- φ^(r+1-8+gap) = φ^1 * φ^(r-8+gap)
  set gap := gap_correction Z_val
  have h_add : (((r + 1 : ℤ) : ℝ) - 8 + gap) = 1 + (((r : ℤ) : ℝ) - 8 + gap) := by
    push_cast
    ring
  rw [h_add, Real.rpow_add phi_pos]
  rw [Real.rpow_one]
  ring

/-- Mass is positive for any valid configuration. -/
theorem predict_mass_pos (s : Sector) (r : ℤ) (Z_val : ℤ) :
    predict_mass s r Z_val > 0 := by
  unfold predict_mass
  apply mul_pos
  · -- yardstick is positive
    unfold yardstick Anchor.E_coh
    apply mul_pos
    · apply mul_pos
      · exact zpow_pos (by norm_num) (B_pow s)
      · exact zpow_pos phi_pos (-5 : ℤ)
    · exact zpow_pos phi_pos (r0 s)
  · -- phi^... is positive
    exact Real.rpow_pos_of_pos phi_pos _

What this page does not claim

The gap_correction definition is not derived from the framework's first principles; it is a chosen model. No claim is made that this charge shift term matches any specific measured particle mass. The physical bridge from recognition events to particle masses is not established by this declaration.

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/MassLaw.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: