Masses Mass Genesis Support Symmetry Topology Scaled Cp6 Load Of Support Rhat Tr

The symmetry reduction

The declaration is a theorem in the framework's machine-checked library of formal theorems. It states a conditional result about a recognition pattern, a discrete record of events on a finite substrate. The theorem says: if the pattern's support is nonempty, if a symmetry action moves every occupied site to every other occupied site, if that action preserves the site load, and if the primitive load factorizes, then the topology-scaled CP6 load holds. The proof chains two earlier theorems: transitivity forces uniform load, and uniform load plus factorization gives the averaged factorized load, which then gives the topology-scaled load.

The content is a reduction. It splits one large obligation, the amplitude theorem's load factorization, into two independent conditions. The first condition is the symmetry surface: the Rhat-generated action is transitive on occupied sites and preserves neutral site load along its orbits. The second is the factorization condition on the primitive load. The theorem shows that these two conditions together suffice. It does not show that either condition actually holds for a physical pattern. The docstring says plainly that instantiating the support action from the actual Q3 carrier, rather than postulating it for a generic finite substrate, is hard future work.

The theorem also carries a companion result: for a stable closed light pattern, the same symmetry and factorization conditions imply that the rest mass equals the predicted mass. That conclusion inherits the same caveat. The symmetry action and the factorization are assumptions, not derived facts. The theorem's value is structural: it identifies the exact shape of the missing work. A reader should see that the framework has reduced a mass-genesis claim to a concrete, checkable obligation about the Q3 carrier and the primitive load.

theorem topologyScaledCP6Load_of_supportRHatTransitive_and_factorization
    {ψ : LightPattern Λ}
    (hsupp : ψ.support.Nonempty)
    (A : SupportRHatAction ψ)
    (htrans : SupportRHatTransitive A)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    TopologyScaledCP6Load ψ :=
  topologyScaledCP6Load_of_supportAveragedFactorizedLoad ψ
    (supportAveragedFactorizedLoad_of_supportRHatTransitive_and_factorization
      hsupp A htrans hfactor)

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

theorem restMass_eq_predictedMass_of_supportRHatSymmetry_and_factorization
    {ψ : LightPattern Λ}
    (hstable : StableClosedLightPattern ψ)
    (_A : SupportRHatAction ψ)
    (_htrans : SupportRHatTransitive _A)
    (hfactor : CanonicalPrimitiveLoadFactorizes ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_stable_and_canonicalPrimitiveLoadFactorizes
    ψ hstable hfactor

What this page does not claim

The theorem does not prove that any physical pattern satisfies the symmetry or factorization assumptions. The theorem does not derive the support action from the Q3 carrier; that instantiation remains open. The theorem does not state that the rest mass equals the predicted mass for all patterns, only for those meeting the stated conditions.

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: