Encyclopedia Masses Masses Mass Genesis T10 Conserved Ratio Dynamical Wall Primitive Closed Pattern

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Conserved Ratio Dynamical Wall Primitive Closed Pattern

A machine-checked theorem shows that a certain ratio of load to topology cannot be changed by the recognition flow, which blocks one class of explanations for how masses arise.

The conserved ratio

In the Recognition Science framework, patterns of light on a discrete ring evolve by a fixed rule called the recognition flow. The declaration primitiveClosedPatternAmplitude_evolve_invariant is a theorem stating that one particular quantity, the primitive closed pattern amplitude, is unchanged by this flow. The amplitude reads only the topology of the pattern, and the flow preserves topology, so the proof is a direct definitional check. A second theorem, site0_neutralLoad_evolve_invariant, shows that the neutralized load at the first site is likewise invariant, because the flow merely cyclically shifts each window.

Together these two invariants give a stronger result. The load-to-topology ratio, defined as the site-zero neutral load divided by the primitive closed pattern amplitude, is a constant of the motion. Its recognition cost, computed by applying the framework's cost function to the ratio, is also conserved. The framework proves all of this in a machine-checked library of formal theorems, with no unproved assumptions added.

The consequence is a wall against a certain kind of explanation. A conserved quantity cannot be relaxed to its minimum by the flow that conserves it. Therefore no selector that depends only on the orbit of the flow, meaning a condition that cannot distinguish a pattern from its evolved images, can force the load-to-topology ratio to its ground-state value. Selection, if it exists, must be a condition on what gets created at the start, not on how patterns move afterward.

This does not show that the ratio is unselectable in general. Scale selection, genesis selection, and any selector that is not orbit-invariant remain open. The residual claim PostedAmplitudeMatchesTopologyFactor remains false. The wall is precise: it blocks only selectors that are invariant under the recognition flow, and it leaves the door open for other kinds of selection.

THEOREM primitiveClosedPatternAmplitude_evolve_invariant · IndisputableMonolith/Masses/MassGenesis/T10ConservedRatioDynamicalWall.lean
primitiveClosedPatternAmplitude_evolve_invariant · IndisputableMonolith/Masses/MassGenesis/T10ConservedRatioDynamicalWall.lean:45
/-- Topology amplitude is definitionally invariant under `evolvePattern`
because the amplitude reads only topology and `evolvePattern` keeps topology. -/
private theorem primitiveClosedPatternAmplitude_evolve_invariant
    (ψ : LightPattern (Fin 8)) (k : ℕ) :
    primitiveClosedPatternAmplitude (evolvePattern k ψ) =
      primitiveClosedPatternAmplitude ψ :=
  rfl
THEOREM loadTopologyRatio_evolve_invariant · IndisputableMonolith/Masses/MassGenesis/T10ConservedRatioDynamicalWall.lean
/-- 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]
THEOREM evolutionOrbitSelector_does_not_force_loadNormalized · IndisputableMonolith/Masses/MassGenesis/T10ConservedRatioDynamicalWall.lean
evolutionOrbitSelector_does_not_force_loadNormalized · IndisputableMonolith/Masses/MassGenesis/T10ConservedRatioDynamicalWall.lean:163
/-- 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')

What this page does not claim

The ratio is unselectable in general; scale and genesis selection remain open. The residual claim PostedAmplitudeMatchesTopologyFactor is established; it remains false. The recognition flow is the only possible dynamics; the wall concerns only this flow.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND