Masses Mass Genesis T10 Conserved Ratio Dynamical Wall

The conserved ratio wall

In the Recognition Science framework, a recognition event is a discrete record of a pattern's state, and the cost of that recognition is a fixed number, not a choice. The framework's library of formal theorems has now proved a result it calls the T10 conserved-ratio dynamical wall. The wall is a boundary on what the framework's own evolution rule, evolvePattern, can accomplish: it cannot by itself produce the mass ground state from any other pattern.

The proof works by finding a quantity that evolution never changes. For any pattern, the framework defines a load-to-topology ratio, a comparison between the pattern's neutralized amplitude and its topology amplitude. The theorem loadTopologyRatio_evolve_invariant proves that this ratio stays exactly the same no matter how many steps of evolution are applied. Because the ratio is conserved, its recognition cost is conserved too. A conserved quantity cannot be relaxed to a minimum by the very flow that conserves it.

The wall then states a general class of impossibility. Suppose a selector, a rule for accepting or rejecting patterns, depends only on the orbit of evolution, meaning it gives the same answer for a pattern and for every pattern it evolves into. If such a selector accepts any pattern that is not already the ground state, it cannot force the ground state on everything it accepts. The theorem evolutionOrbitSelector_does_not_force_loadNormalized proves this. A concrete witness exists: the doubled ground state has ratio exactly four, is off the ground state, and evolution keeps it that way forever.

What this means in plain language is that mass selection, if it happens at all in the framework, must be a condition on what gets created, not on how patterns move. The framework calls this genesis selection. The wall does not say the ratio is unselectable in general; scale selection and other non-orbit selectors remain open targets. The wall is a theorem with no unproved assumptions, and it is the framework's way of saying that dynamics alone cannot explain why masses are what they are.

/-- The load-to-topology ratio is a constant of the recognition motion. -/
theorem loadTopologyRatio_evolve_invariant
    (ψ : LightPattern (Fin 8)) (k : ℕ) :
    loadTopologyRatio (evolvePattern k ψ) = loadTopologyRatio ψ := by
  unfold loadTopologyRatio
  rw [site0_neutralLoad_evolve_invariant ψ k,
    primitiveClosedPatternAmplitude_evolve_invariant ψ k]

/-- If an orbit-invariant selector accepts any off-ground pattern, it cannot
force `LoadNormalizedToTopology` on its accept set: the whole evolve-orbit of
that witness stays accepted and stays off-ground. -/
theorem evolutionOrbitSelector_does_not_force_loadNormalized
    (S : LightPattern (Fin 8) → Prop)
    (hS : IsEvolutionOrbitSelector S)
    (ψ : LightPattern (Fin 8))
    (hacc : S ψ)
    (hnot : ¬ LoadNormalizedToTopology ψ) :
    ¬ ∀ φ : LightPattern (Fin 8), S φ → LoadNormalizedToTopology φ := by
  intro hall
  obtain ⟨hacc', hnot'⟩ :=
    evolutionOrbitSelector_preserves_offGround S hS ψ hacc hnot 0
  exact hnot' (hall _ hacc')

/-- Strengthened witness: the doubled ground state has ratio exactly four. -/
theorem exists_loadTopologyRatio_eq_four :
    ∃ ψ : LightPattern (Fin 8),
      loadTopologyRatio ψ = 4 ∧ ¬ LoadNormalizedToTopology ψ := by
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  obtain ⟨c, hc, hground⟩ := exists_scale_loadNormalizedToTopology Eseed
  let seed := worldlinePattern gapOneTwoPhaseMode
  let ground := scalePattern c seed
  let ψ := scalePattern 2 ground
  have hratio0 : loadTopologyRatio ground = 1 :=
    (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ground).2 hground
  have hratio : loadTopologyRatio ψ = 4 := by
    calc
      loadTopologyRatio ψ = (2 : ℝ) ^ 2 * loadTopologyRatio ground := by
        simpa [ψ] using loadTopologyRatio_scalePattern 2 ground
      _ = 4 * 1 := by rw [hratio0]; norm_num
      _ = 4 := by norm_num
  have hnot : ¬ LoadNormalizedToTopology ψ := by
    intro hnorm
    have hone : loadTopologyRatio ψ = 1 :=
      (loadTopologyRatio_eq_one_iff_loadNormalizedToTopology ψ).2 hnorm
    have hne : (4 : ℝ) ≠ 1 := by norm_num
    exact hne (hratio.symm.trans hone)
  exact ⟨ψ, hratio, hnot⟩

What this page does not claim

This does not claim the ratio is unselectable in general, only that evolution-orbit selectors cannot force it. This does not claim to derive any specific particle mass from the wall.

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