Masses Mass Genesis Integrated Load Integrated Meaning Load Zero Iff Support Sit

The zero-load test

A pattern's total meaning-load, a discrete record of how much semantic weight it carries, is the sum of the loads at each of its occupied sites. The theorem integratedMeaningLoad_zero_iff_support_site_zero establishes the natural bridge between the whole and its parts: the total is zero if and only if every occupied site's load is zero. Because each site load is nonnegative, no cancellation can hide a positive site behind a negative neighbor; the sum vanishes exactly when each term vanishes.

The proof is purely bottom-up. A site load is defined as the squared norm of a neutralized window, and the total is the finite sum over the pattern's support. The theorem then follows from a standard lemma about sums of nonnegative numbers. This closes the algebraic load layer of Mass Genesis, the framework's account of how masses arise from recognition events.

In Recognition Science, this result does not yet speak about mass. The docstring is explicit: it does not identify the load with the phi-ladder mass law. The theorem certifies that the load functional behaves coherently, that zero total load means zero everywhere on the support, and that the load is invariant under the pattern evolution map. Those are structural facts about the ledger, not yet a derivation of particle masses.

What the result changes is the vocabulary available to later steps. Any pattern with positive total load must have at least one site with positive load, and any pattern with no positive site has zero total. That equivalence is now a proved tool, ready for the next layer of the mass-genesis construction.

theorem integratedMeaningLoad_zero_iff_support_site_zero
    (ψ : LightPattern Λ) :
    integratedMeaningLoad ψ = 0 ↔
      ∀ x ∈ ψ.support, siteMeaningLoad ψ x = 0 := by
  rw [integratedMeaningLoad_eq_support_sum ψ]
  exact Finset.sum_eq_zero_iff_of_nonneg
    (fun x _ => siteMeaningLoad_nonneg ψ x)

theorem siteMeaningLoad_nonneg (ψ : LightPattern Λ) (x : Λ) :
    0 ≤ siteMeaningLoad ψ x := by
  unfold siteMeaningLoad
  exact normSq8_nonneg_local (neutralize (ψ.window x))

theorem integratedMeaningLoad_eq_of_evolvePattern
    (ψ : LightPattern Λ) (k : ℕ) :
    integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ :=
  integratedMeaningLoad_eq_of_sameLoadOnSupport
    (sameLoadOnSupport_evolvePattern ψ k)

What this page does not claim

The load functional is not identified with the phi-ladder mass law. The theorem does not assign numerical masses to any pattern. The result does not depend on the specific form of the neutralization map.

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