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

The amplitude obstruction

In the framework's account, a particle is a stable pattern of light: a discrete record of eight windows, each carrying a complex amplitude, with a support and a topology. The framework models a particle's rest mass as its integrated meaning load, a real number derived from the pattern. The question at issue is whether this load can be predicted from the pattern's topology alone, the way a mass law would require.

The declaration not_forall_stable_massLawLoadRealized proves that it cannot. The theorem states that for any stable pattern, it is false that every stable pattern with the same topology has the same integrated meaning load. The proof exhibits a concrete witness: multiply every window amplitude by a nonzero constant c. This rescaling preserves all three conditions that define a stable pattern: localization of support, nontrivial neutral load, and closure under the eight-tick orbit. The topology is copied exactly, so the mass law predicts the same mass. But the load side scales as c squared, so the load changes. Two sides that transform differently under a map that preserves admissibility can agree on at most one point of each scaling orbit, so the universal identity is false.

The sharpest form of the obstruction is a theorem that at fixed topology, the integrated meaning load of a stable pattern can be made equal to any positive real number. The load carries no information that the topology constrains, so no function of the topology can predict it. This is what the nine failed searches for a realization theorem were missing: they sought a theorem that cannot exist while admissibility is blind to the amplitude.

In Recognition Science, this refutes the identification of rest mass with the topology-labelled mass law on the present pattern surface. It does not refute mass genesis from meaning: the identity restMass = integratedMeaningLoad for stable patterns remains untouched and is the genuine object. The constructive reading is that an amplitude-fixing condition must be added to admissibility. The theorem T10AnchorLoadTransportComposition already shows what such a condition looks like, since unitPosting_load pins one specific window to load exactly 2. The open question is what forces a realized particle's window to be that one.

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

/-- At fixed topology, the integrated meaning load of a stable pattern can be made
equal to ANY positive real. This is the sharpest form of the obstruction: the load
carries no information that the topology constrains, so no function of the topology
can predict it. -/
theorem exists_sameTopology_stable_load_eq
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ)
    {r : ℝ} (hr : 0 < r) :
    ∃ χ : LightPattern (Fin 8),
      SameTopology ψ χ ∧ StableClosedLightPattern χ ∧
        integratedMeaningLoad χ = r := by
  have hL : 0 < integratedMeaningLoad ψ :=
    integratedMeaningLoad_pos_of_nontrivial ψ h.2.1
  have hquot : 0 < r / integratedMeaningLoad ψ := div_pos hr hL
  have hLne : integratedMeaningLoad ψ ≠ 0 := ne_of_gt hL
  refine ⟨scalePattern (Real.sqrt (r / integratedMeaningLoad ψ)) ψ,
    (scalePattern_topology _ ψ).symm,
    stableClosedLightPattern_scalePattern (ne_of_gt (Real.sqrt_pos.mpr hquot)) h, ?_⟩
  rw [integratedMeaningLoad_scalePattern, Real.sq_sqrt (le_of_lt hquot)]
  field_simp

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

What this page does not claim

The declaration does not refute mass genesis from meaning, only the identification of the load with the topology-labelled mass law on this surface. The theorem does not claim that the load is unconstrained for all patterns, only that it is free at fixed topology under the current admissibility conditions. The proof does not rely on any new axioms; it uses only the library's existing theorems and the definition of scalePattern.

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: