Masses Mass Genesis T10 Unit Free Anchor Wall Distinct Masses Stable Under Unit

The unit-free wall

In the Recognition Science account, the predicted mass of a particle is a number of energy units, such as electronvolts, chosen by hand from outside the theory. A theorem in the framework's machine-checked library of formal theorems shows that this choice of unit is powerless against a particular structural obstruction. The theorem, distinct_masses_stable_under_unit_rescaling, states that if two patterns have different predicted masses, then multiplying both masses by any positive factor, which is exactly what a change of unit does, leaves them different. The proof is one line: multiplying two unequal positive numbers by the same positive factor cannot make them equal.

The statement matters because it separates what depends on a human convention from what does not. An earlier ceiling argument in the same library compared a predicted mass, a number of eV, against fixed thresholds like 64 and 256. Read the electron's mass in GeV instead of eV and its predicted value drops below every threshold, so that ceiling collapses under a unit change. The ratio law does not. Between two species, the predicted masses and posting amplitudes satisfy m * b² = m' * a², an equation in which every quantity is a ratio once divided through. The new theorem is the contrapositive of the simpler fact that one amplitude cannot serve two different masses: the electron and the muon, which the library proves have different predicted masses, cannot both post at the ledger's unit amplitude, no matter what unit is chosen.

The declaration also carries a sharper companion. Two rungs of the same sector at the same charge index stand in a ratio that is an irrational power of phi, the golden ratio. A common rescaling cancels out of that ratio, so no change of unit can make two different rungs both rational compositions of the unit posting. The electron and the muon, rungs 2 and 13, have ratio phi^11, and the Fibonacci number 89 appears in the proof that this ratio is irrational.

What the theorem does not claim is a value for any mass. It never says what the electron or muon mass is in kilograms or eV. It only says that the difference between them is not an artifact of units. The numerical ceiling wall, with its 64 and 256 thresholds, is shown to be unit-dependent and therefore not a genuine obstruction. The ratio wall is unit-independent and stands. The distinction is the whole point: a reader should compare the two halves, one defeated by a unit change, the other untouched by it.

/-- **The ratio wall does survive.** A positive rescaling of the mass unit cannot
make two different predicted masses agree, so the obstruction of section 1 is
untouched by any unit identification. -/
theorem distinct_masses_stable_under_unit_rescaling
    {k : ℝ} (hk : 0 < k) {ψ χ : LightPattern (Fin 8)}
    (hne : predictedMass ψ ≠ predictedMass χ) :
    k * predictedMass ψ ≠ k * predictedMass χ := fun h =>
  hne (mul_left_cancel₀ (ne_of_gt hk) h)

/-- **The ceiling wall does not survive a change of mass unit.** For every pattern
there is a positive rescaling of the mass unit placing its rescaled predicted mass
below the Boolean ceiling. Nothing about the pattern is used except that its
predicted mass is positive, so this applies to the whole charged spectrum. -/
theorem exists_unit_rescaling_below_ceiling (ψ : LightPattern (Fin 8)) :
    ∃ k : ℝ, 0 < k ∧ k * predictedMass ψ < 64 := by
  have hpos : 0 < predictedMass ψ := predictedMass_pos ψ
  refine ⟨1 / predictedMass ψ, div_pos one_pos hpos, ?_⟩
  have hcancel : 1 / predictedMass ψ * predictedMass ψ = 1 := by
    field_simp
  rw [hcancel]
  norm_num

/-- **The ratio law.** Two load-normalized patterns with settled anchors relate
their predicted masses and their posting amplitudes by `m * b² = m' * a²`. Every
quantity here is a ratio once the equation is divided through, so the statement is
untouched by a change of mass unit. -/
theorem settledAnchor_mass_amplitude_ratio
    {a b : ℝ} {ψ χ : LightPattern (Fin 8)}
    (hψ : LoadNormalizedToTopology ψ) (hwψ : SettledAnchorWindow a ψ)
    (hχ : LoadNormalizedToTopology χ) (hwχ : SettledAnchorWindow b χ) :
    predictedMass ψ * b ^ 2 = predictedMass χ * a ^ 2 := by
  rw [loadNormalized_settledAnchor_predictedMass_eq hψ hwψ,
    loadNormalized_settledAnchor_predictedMass_eq hχ hwχ]
  ring

/-- **The instantiated wall.** A pattern carrying the electron's mass-law value and
a pattern carrying the muon's cannot both have the ledger's unit posting at their
anchors, and no choice of mass unit changes that. -/
theorem electron_muon_not_both_unitSettled
    {ψ χ : LightPattern (Fin 8)}
    (hψ : LoadNormalizedToTopology ψ) (hχ : LoadNormalizedToTopology χ)
    (hmψ : predictedMass ψ = MassLaw.predict_mass
      (rowSector ChargedMassRow.electron) (rowRung ChargedMassRow.electron)
      (rowZ ChargedMassRow.electron))
    (hmχ : predictedMass χ = MassLaw.predict_mass
      (rowSector ChargedMassRow.muon) (rowRung ChargedMassRow.muon)
      (rowZ ChargedMassRow.muon)) :
    ¬ (SettledAnchorWindow 1 ψ ∧ SettledAnchorWindow 1 χ) := by
  refine distinct_masses_not_both_unitSettled hψ hχ ?_
  rw [hmψ, hmχ]
  exact electron_muon_predict_mass_ne

/-- Two rungs of one sector at one charge index stand in ratio `phi ^ (r' - r)`. -/
theorem predict_mass_rung_ratio (s : Anchor.Sector) (r r' Z : ℤ) :
    MassLaw.predict_mass s r' Z
      = phi ^ (r' - r) * MassLaw.predict_mass s r Z := by
  have hcast : (r' : ℝ) - (r : ℝ) = ((r' - r : ℤ) : ℝ) := by push_cast; ring
  rw [predict_mass_rung_shift s r r' Z, hcast, Real.rpow_intCast]

What this page does not claim

The theorem does not predict the numerical value of any particle mass. The theorem does not claim the numerical ceiling of 64 or 256 is a meaningful physical bound. The theorem does not say which unit, if any, the theory itself selects.

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/MassGenesis/T10UnitFreeAnchorWall.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: