Masses Mass Genesis T10 Conserved Ratio Dynamical Wall Load Normalized Forcing S

The dynamical wall

In the Recognition Science framework, patterns on an eight-tick cycle carry two measurable features: a neutral load, which is the squared size of the pattern after its mean is removed, and a topology amplitude, which records a structural label that motion does not change. The framework's library proves that its evolution rule, a cyclic shift of each window, leaves both features untouched. Therefore the ratio of load to topology is a constant of the motion, and so is the recognition cost of that ratio, which is the cost function J applied to it. A conserved quantity cannot be relaxed to its minimum by the flow that conserves it.

The declaration loadNormalizedForcingSelector_not_evolutionOrbit states the consequence as a formal theorem. A selector is a rule that accepts or rejects patterns; an evolution-orbit selector is one whose acceptance is invariant under the evolution rule, meaning it depends only on the orbit, the set of patterns reachable by repeated evolution. The theorem proves: any selector that accepts a pattern off the load-normalized ground state, and that forces every accepted pattern to be load-normalized, cannot be an evolution-orbit selector. The proof is short. If the selector were orbit-invariant, the whole orbit of the off-ground witness would stay accepted, and by conservation every image would stay off-ground, contradicting the forcing condition. A concrete witness exists: scaling the ground state by two multiplies the ratio by four, so the doubled pattern is off-ground and accepted by the universal selector that accepts everything, which is orbit-invariant and therefore cannot force load normalization.

What the theorem does not claim is just as important. It does not show the ratio is unselectable in general. Scale selection, genesis selection, and any selector that is not orbit-invariant remain open. The theorem is a wall against one class of mechanisms, not a proof that no mechanism exists. The residual statement that posted amplitude matches the topology factor remains false. The declaration is a theorem in the machine-checked library of formal theorems, proved with no sorry and no new axiom, but it lives entirely inside the framework's model of patterns and evolution; it is not a claim about any physical system outside that model.

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

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

/-- Scaling by two multiplies the load-to-topology ratio by four (topology
amplitude fixed; site-0 neutralized load scales by `c²`). -/
theorem loadTopologyRatio_scalePattern
    (c : ℝ) (ψ : LightPattern (Fin 8)) :
    loadTopologyRatio (scalePattern c ψ) = c ^ 2 * loadTopologyRatio ψ := by
  unfold loadTopologyRatio
  have hamp :
      primitiveClosedPatternAmplitude (scalePattern c ψ) =
        primitiveClosedPatternAmplitude ψ :=
    rfl
  have hload :
      normSq8 (neutralize ((scalePattern c ψ).window 0)) =
        c ^ 2 * normSq8 (neutralize (ψ.window 0)) :=
    normSq8_neutralize_smul c (ψ.window 0)
  rw [hload, hamp, mul_div_assoc]

What this page does not claim

This theorem does not claim that the load-to-topology ratio is unselectable in general, only that evolution-orbit selectors cannot force it. This theorem does not claim that scale selection or genesis selection are impossible, as these remain open. This theorem does not claim anything about physical systems outside the framework's formal model of patterns and evolution.

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: