Masses Mass Genesis T10 Unit Free Anchor Wall

The unit-free wall

In the Recognition Science account of particle masses, each species is a pattern of eight ticks, and its predicted mass comes from a formula involving the golden ratio. The framework's machine-checked library of formal theorems asks a pointed question: which parts of the mass law survive a change of unit, and which are artifacts of measuring in electronvolts? The module T10UnitFreeAnchorWall separates the two with exact proofs.

The classical facts about the golden ratio matter here. The golden ratio φ is the positive solution to r² = r + 1, about 1.618. It is irrational, and so are its nonzero integer powers. The mass law in this framework places species on rungs: moving up one rung multiplies the predicted mass by a power of φ. The electron and the muon sit in the same sector, at the same charge index, on rungs 2 and 13, so their predicted masses differ by a factor of φ¹¹, which is irrational.

The framework models a ledger: a discrete record of recognition events. Each species posts an amplitude at its anchor. The settled-anchor equation links posting amplitude a to predicted mass m by m = 16a². From this, the module proves a ratio law: for two species with amplitudes a and b, the relation m·b² = m′·a² holds, and every quantity in it is a ratio once divided through. This statement is untouched by a change of mass unit. A corollary is the wall itself: two species with different predicted masses cannot both post at the unit amplitude 1. The electron and the muon instantiate this, and the proof shows no rescaling of the mass unit can make their predicted masses agree.

The module also audits a numerical ceiling that earlier work recorded. That ceiling caps predicted masses at 64, with charged rows exceeding 256. But these thresholds are stated in electronvolts. The theorem exists_unit_rescaling_below_ceiling shows that for every pattern, some positive rescaling of the mass unit places its predicted mass below 64. Read the electron in GeV instead of eV and its predicted mass is about 5.1e-4. The ceiling wall, on its own, does not survive a unit change. The ratio wall does. The certificate theorem t10UnitFreeAnchorWallCert packages both halves: the ceiling is unit-dependent, the ratio is unit-independent.

What this establishes in plain language is a sharper obstruction. The numerical ceiling was a statement about a chosen unit, and it evaporates under rescaling. The ratio wall is a statement about the structure of the mass law itself, and it stands. One amplitude cannot serve two different masses, no matter what units you choose. The reader can now see which parts of the mass-genesis argument are load-bearing and which were scaffolding tied to a particular convention.

/-- **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 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 wall, with no numeral in it.** Two species whose predicted masses differ
cannot both post at the ledger's unit amplitude. -/
theorem distinct_masses_not_both_unitSettled
    {ψ χ : LightPattern (Fin 8)}
    (hψ : LoadNormalizedToTopology ψ) (hχ : LoadNormalizedToTopology χ)
    (hne : predictedMass ψ ≠ predictedMass χ) :
    ¬ (SettledAnchorWindow 1 ψ ∧ SettledAnchorWindow 1 χ) := by
  rintro ⟨hwψ, hwχ⟩
  exact hne (settledAnchor_same_amplitude_forces_same_mass hψ hwψ hχ hwχ)

/-- **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 electron and the muon sit in the same sector at the same charge index and
differ only in rung, so their predicted masses differ. -/
theorem electron_muon_predict_mass_ne :
    MassLaw.predict_mass (rowSector ChargedMassRow.electron)
        (rowRung ChargedMassRow.electron) (rowZ ChargedMassRow.electron)
      ≠ MassLaw.predict_mass (rowSector ChargedMassRow.muon)
        (rowRung ChargedMassRow.muon) (rowZ ChargedMassRow.muon) := by
  have h : MassLaw.predict_mass Anchor.Sector.Lepton 2 1332
      < MassLaw.predict_mass Anchor.Sector.Lepton 13 1332 :=
    predict_mass_lt_of_rung_lt Anchor.Sector.Lepton 1332 (by norm_num)
  simpa [rowSector, rowRung, rowZ] using ne_of_lt h

theorem t10UnitFreeAnchorWallCert : T10UnitFreeAnchorWallCert where
  ratio_law := fun hψ hwψ hχ hwχ =>
    settledAnchor_mass_amplitude_ratio hψ hwψ hχ hwχ
  ceiling_is_unit_dependent := exists_unit_rescaling_below_ceiling
  ratio_is_unit_independent := fun hk hne =>
    distinct_masses_stable_under_unit_rescaling hk hne
  wall_without_numerals := fun hψ hχ hne =>
    distinct_masses_not_both_unitSettled hψ hχ hne
  not_vacuous_on_the_species_table := electron_muon_predict_mass_ne

What this page does not claim

This module does not derive the numerical value of any particle mass. The ceiling wall is not claimed to be a valid obstruction; it is shown to be unit-dependent. The ratio law does not by itself determine the absolute scale of masses.

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: