Masses Mass Genesis T10 Conserved Ratio Dynamical Wall Evolution Orbit Selector

The dynamical wall

In the Recognition Science framework, a ledger (a discrete record of recognition events) holds patterns on eight positions. The framework's evolution rule, evolvePattern, shifts each window cyclically. Two things stay fixed under that shift: the neutral load, a measure of the pattern's content, and the topology amplitude, a measure of its shape. Because both stay fixed, their ratio stays fixed, and so does the recognition cost of that ratio.

A conserved quantity cannot be relaxed to its minimum by the flow that conserves it. The framework's ground state, called LoadNormalizedToTopology, is exactly the state where that ratio equals one. If a pattern starts with a ratio of four, evolution can never turn it into a pattern with ratio one. The theorem evolutionOrbitSelector_does_not_force_loadNormalized states this as a wall: no selector that depends only on the evolution orbit, meaning it accepts a pattern if and only if it accepts every shifted version of that pattern, can force every accepted pattern into the ground state. If such a selector accepts any off-ground pattern, the whole orbit of that pattern stays accepted and stays off-ground.

The proof is concrete. There exists a pattern with ratio exactly four, obtained by doubling the ground state. The universal selector, which accepts every pattern, is orbit-invariant and accepts that ratio-four witness. Therefore it cannot force load normalization. The theorem also exports the contrapositive: any selector that forces load normalization on every accepted pattern, and accepts an off-ground witness, cannot be orbit-invariant.

What the wall does not show is just as important. It does not show the ratio is unselectable in general. A selector that depends on what gets created, not on how it moves, could still force the ground state. Scale selection and genesis selection remain open. The residual PostedAmplitudeMatchesTopologyFactor remains false. The wall only closes the door on selectors that watch the orbit and nothing else.

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

/-- Admission export: any selector that forces load normalization on every
accepted pattern, and that accepts an off-ground witness, cannot be
orbit-invariant. -/
theorem loadNormalizedForcingSelector_not_evolutionOrbit
    (S : LightPattern (Fin 8) → Prop)
    (ψ : LightPattern (Fin 8))
    (hacc : S ψ)
    (hnot : ¬ LoadNormalizedToTopology ψ)
    (hforces :
      ∀ φ : LightPattern (Fin 8), S φ → LoadNormalizedToTopology φ) :
    ¬ IsEvolutionOrbitSelector S := by
  intro hS
  exact
    (evolutionOrbitSelector_does_not_force_loadNormalized
      S hS ψ hacc hnot) hforces

What this page does not claim

The ratio is unselectable in general; scale selection and genesis selection remain open. The ground state is unreachable by any means; only orbit-invariant selectors are blocked.

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: