Masses Mass Genesis T10 Amplitude Freedom Refutation Not Forall Stable Rest Mass

The amplitude freedom refutation

The declaration not_forall_stable_restMass_eq_predictedMass is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves a negative universal statement: it is not the case that for every stable pattern, the rest mass equals the predicted mass. In plain terms, the framework cannot assert that these two quantities always match.

The proof works by constructing a specific counterexample. Given any stable pattern, the framework can double all its window amplitudes, creating a new pattern that is also stable. This rescaled pattern has the same topology, and therefore the same predicted mass, but its load, which determines rest mass, is four times larger. Since the two sides transform differently under rescaling, they can agree at most once along each scaling orbit, so the universal identity fails.

The root cause is that the admissibility conditions for a stable pattern do not constrain the amplitude. The framework's definition of a stable pattern requires localized support, nontrivial neutral load, and closed orbit, none of which see the window's complex amplitude values. This is what the framework calls amplitude blindness.

What this theorem does not do is refute the idea that rest mass comes from meaning. The identity restMass = integratedMeaningLoad for stable patterns remains untouched and is the genuine object of study. The refutation targets only the identification of that load with the topology-labelled mass law on this surface. The constructive next step is to add an amplitude-fixing condition to admissibility, and the framework already has an example of what such a condition looks like in a theorem that pins one specific window to a load of exactly 2.

/-- The same statement in the headline variables: rest mass and predicted mass
cannot agree on every stable pattern. -/
theorem not_forall_stable_restMass_eq_predictedMass
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    ¬ (∀ χ : LightPattern (Fin 8),
        StableClosedLightPattern χ → restMass χ = predictedMass χ) := by
  intro hall
  refine not_forall_stable_massLawLoadRealized h (fun χ hχ => ?_)
  have := hall χ hχ
  rwa [restMass_eq_integratedMeaningLoad_of_stable χ hχ] at this

/-- **Admissibility is amplitude-blind.** A nonzero rescaling of any stable closed
pattern is again a stable closed pattern. -/
theorem stableClosedLightPattern_scalePattern {c : ℝ} (hc : c ≠ 0)
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    StableClosedLightPattern (scalePattern c ψ) :=
  ⟨localizedSupport_scalePattern c h.1,
   nontrivialNeutralLoad_scalePattern hc h.2.1,
   closedRHatOrbit_of_any _⟩

/-- **Main theorem.** The mass-law load identity cannot hold for every stable
pattern. Given any single stable pattern, its double is also stable, has the same
topology and therefore the same predicted mass, but four times the load. -/
theorem not_forall_stable_massLawLoadRealized
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    ¬ (∀ χ : LightPattern (Fin 8),
        StableClosedLightPattern χ → MassLawLoadRealized χ) := by
  intro hall
  have hL : 0 < integratedMeaningLoad ψ :=
    integratedMeaningLoad_pos_of_nontrivial ψ h.2.1
  have h2 : StableClosedLightPattern (scalePattern 2 ψ) :=
    stableClosedLightPattern_scalePattern (by norm_num) h
  have e1 : integratedMeaningLoad ψ = predictedMass ψ := hall ψ h
  have e2 : integratedMeaningLoad (scalePattern 2 ψ)
      = predictedMass (scalePattern 2 ψ) := hall _ h2
  rw [integratedMeaningLoad_scalePattern, predictedMass_scalePattern, ← e1] at e2
  have hfour : (2 : ℝ) ^ 2 = 4 := by norm_num
  rw [hfour] at e2
  linarith

What this page does not claim

This does not claim that rest mass and predicted mass never agree, only that they cannot agree for every stable pattern. This does not claim that mass genesis from meaning is refuted, only that the specific identification with the topology-labelled mass law fails on this surface. This does not claim that the framework has solved the problem of what fixes the amplitude, which remains an open question.

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