Masses Mass Genesis Support Symmetry Support Averaged Factorized Load Of Support

The equipartition theorem

In classical physics, equipartition is the idea that energy spreads evenly among the parts of a system that are in thermal contact. The theorem at issue here is a discrete, structural version of that idea. It starts with a finite set of sites, some occupied, each carrying a numeric load. A ledger is a discrete record of such sites and loads. The theorem says: if a symmetry moves occupied sites around, reaches every occupied site from every other, and preserves the load at each step, then all occupied sites carry the same load.

The formal statement is supportAveragedFactorizedLoad_of_supportRHatTransitive_and_factorization in the framework's machine-checked library of formal theorems. It proves that, under two conditions, a certain averaged load equals the factorization of the primitive load. The first condition is transitivity: the symmetry can move any occupied site to any other. The second is factorization: the primitive load splits cleanly into a product of factors. The conclusion, SupportAveragedFactorizedLoad, is the averaged load that appears in the mass prediction.

The proof is short and direct. Transitivity gives, for any two occupied sites x and y, a number of steps n such that the symmetry moves x to y. Load preservation along each step gives that the load at the image equals the load at the source. Chaining the steps, the load at y equals the load at x. Hence the load is constant across the support. The factorization condition then turns that constant into the averaged load. The theorem is a composition of two earlier results: uniform load from transitivity, and the averaged load from uniform load plus factorization.

In Recognition Science, the framework models particle mass as a function of a stable closed light pattern. The theorem is one step in a chain that aims to derive rest mass from the pattern's structure. It does not, by itself, produce a number for any particle. It does not say which symmetry acts on a real particle's support; that is future work, as the library notes. It does not prove that the symmetry exists. What it proves is conditional: if such a symmetry is transitive and load-preserving, and if the primitive load factorizes, then the averaged load follows.

The practical consequence is a reduction. Instead of computing the averaged load directly, one may verify two simpler properties: transitivity and factorization. This is the kind of modular decomposition that makes a large formal development tractable. The theorem also illustrates a general principle: symmetry, when strong enough, forces uniformity. That principle is not unique to this framework; it echoes the classical equipartition theorem and the fact that a transitive group action on a set makes all orbits equal.

theorem supportAveragedFactorizedLoad_of_supportRHatTransitive_and_factorization
    {ψ : LightPattern Λ}
    (hsupp : ψ.support.Nonempty)
    (A : SupportRHatAction ψ)
    (htrans : SupportRHatTransitive A)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    SupportAveragedFactorizedLoad ψ :=
  supportAveragedFactorizedLoad_of_uniform_and_factorization
    ψ hsupp (uniformSiteMeaningLoad_of_supportRHatTransitive A htrans) hfactor

/-- The Rhat support action is transitive on the occupied support. -/
def SupportRHatTransitive
    {ψ : LightPattern Λ}
    (A : SupportRHatAction ψ) : Prop :=
  ∀ x ∈ ψ.support, ∀ y ∈ ψ.support,
    ∃ n : ℕ, (A.step^[n]) x = y

theorem load_iterate
    {ψ : LightPattern Λ}
    (A : SupportRHatAction ψ)
    (n : ℕ) {x : Λ}
    (hx : x ∈ ψ.support) :
    siteMeaningLoad ψ ((A.step^[n]) x) = siteMeaningLoad ψ x := by
  induction n generalizing x with
  | zero =>
      rfl
  | succ n ih =>
      calc
        siteMeaningLoad ψ ((A.step^[n.succ]) x)
            = siteMeaningLoad ψ ((A.step^[n]) (A.step x)) := rfl
        _ = siteMeaningLoad ψ (A.step x) := ih (A.step_mem x hx)
        _ = siteMeaningLoad ψ x := A.load_step x hx

/-- The equipartition theorem: transitive load-preserving Rhat support action
forces uniform neutral load across the occupied support. -/
theorem uniformSiteMeaningLoad_of_supportRHatTransitive
    {ψ : LightPattern Λ}
    (A : SupportRHatAction ψ)
    (htrans : SupportRHatTransitive A) :
    UniformSiteMeaningLoad ψ := by
  intro x hx y hy
  rcases htrans x hx y hy with ⟨n, hn⟩
  have hload := A.load_iterate n hx
  rw [hn] at hload
  exact hload.symm

theorem supportAveragedFactorizedLoad_of_supportRHatTransitive_and_factorization
    {ψ : LightPattern Λ}
    (hsupp : ψ.support.Nonempty)
    (A : SupportRHatAction ψ)
    (htrans : SupportRHatTransitive A)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    SupportAveragedFactorizedLoad ψ :=
  supportAveragedFactorizedLoad_of_uniform_and_factorization
    ψ hsupp (uniformSiteMeaningLoad_of_supportRHatTransitive A htrans) hfactor

What this page does not claim

The theorem does not prove that any real particle's support admits a transitive load-preserving symmetry. The theorem does not derive a numerical value for any particle mass. The theorem does not claim that the symmetry action is unique or canonical.

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