Encyclopedia Masses Masses Mass Genesis T10 Amplitude Freedom Refutation Exists Same Topology Stable

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Amplitude Freedom Refutation Exists Same Topology Stable

A machine-checked proof shows that two stable patterns with identical topology can carry different loads, blocking one route from topology to mass.

The amplitude freedom refutation

The declaration exists_sameTopology_stable_different_load proves a negative result about a proposed identification. In the Recognition Science framework, a stable pattern is a discrete record of recognition events that satisfies three admissibility conditions: its support is localized, it carries a nontrivial neutral load, and its orbit under an eight-tick shift is closed. The declaration shows that for any such stable pattern, there exists another stable pattern with the same topology but a different integrated meaning load. The topology, meaning the shape of the support, is copied exactly; the load, a measure of accumulated meaning, differs.

The proof constructs the witness explicitly by rescaling every window amplitude by a nonzero constant. This rescaling preserves all three admissibility conditions, so the new pattern is stable. The topology is copied by definition, and the load scales by the square of the constant, so choosing a constant other than one produces a different load. The theorem therefore establishes that the load at fixed topology is completely free: it can be made equal to any positive real number. No function of the topology alone can predict it.

This refutes the identification of rest mass with the topology-labelled mass law, on the present pattern surface. The mass-law side is scale-invariant, while the load side is scale-covariant of degree two, so the two sides can agree on at most one point of each scaling orbit. The universal identity is false. The cause is named precisely: the window is free complex data that no admissibility condition constrains. The nine earlier scale attacks failed not by bad luck but because they sought a theorem that cannot exist while admissibility is amplitude-blind.

The declaration does not refute mass genesis from meaning. The identity restMass = integratedMeaningLoad for stable patterns remains untouched and is the genuine object. It refutes only the identification of that load with the topology-labelled mass law. The constructive reading is that an amplitude-fixing condition must be added to admissibility, and the open question is what forces a realized particle's window to be that one.

The classical analogue is a counterexample to a universal claim. If one conjectured that all triangles with the same base have the same area, a single pair of triangles with the same base and different heights would refute it. Here, the base is the topology and the height is the amplitude. The theorem exhibits the pair explicitly, closing a question that had been left open by conditional obstructions.

THEOREM exists_sameTopology_stable_different_load · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeFreedomRefutation.lean
exists_sameTopology_stable_different_load · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeFreedomRefutation.lean:154
/-- The witness pair, exhibited explicitly, for use with the conditional
obstruction theorems that until now had to assume it. -/
theorem exists_sameTopology_stable_different_load
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    ∃ χ : LightPattern (Fin 8),
      SameTopology ψ χ ∧ StableClosedLightPattern χ ∧
        integratedMeaningLoad χ ≠ integratedMeaningLoad ψ := by
  have hL : 0 < integratedMeaningLoad ψ :=
    integratedMeaningLoad_pos_of_nontrivial ψ h.2.1
  refine ⟨scalePattern 2 ψ, (scalePattern_topology _ ψ).symm,
    stableClosedLightPattern_scalePattern (by norm_num) h, ?_⟩
  rw [integratedMeaningLoad_scalePattern]
  intro hEq
  have hfour : (2 : ℝ) ^ 2 = 4 := by norm_num
  rw [hfour] at hEq
  linarith
THEOREM exists_sameTopology_stable_load_eq · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeFreedomRefutation.lean
/-- 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
THEOREM not_forall_stable_restMass_eq_predictedMass · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeFreedomRefutation.lean
not_forall_stable_restMass_eq_predictedMass · IndisputableMonolith/Masses/MassGenesis/T10AmplitudeFreedomRefutation.lean:143
/-- 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

Mass genesis from meaning is not refuted; the identity restMass = integratedMeaningLoad for stable patterns remains untouched. The refutation applies only to the present pattern surface where admissibility is amplitude-blind, not to any strengthened admissibility condition. The theorem does not identify which amplitude-fixing condition is the correct one; it only shows that one must be added.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND