Masses Mass Genesis Integrated Load Integrated Meaning Load Pos Iff Nontrivial

Meaning load and its positivity

In the Recognition Science framework, a ledger (a discrete record of events) assigns to each pattern a number called its integrated meaning load. The declaration integratedMeaningLoad_pos_iff_nontrivial proves a simple equivalence: a pattern has a positive total load if and only if it has at least one site with a positive load. The theorem is a formal statement in the framework's machine-checked library of formal theorems, and it is proved from the definitions of the load function and the nontriviality predicate.

The load at a single site is defined as the squared norm of a neutralized window, a real number that is always nonnegative. The integrated load is the finite sum of these site loads over the pattern's support, the set of sites where the pattern is active. Because every term in the sum is nonnegative, the sum can be zero only when every term is zero, and it is positive exactly when at least one term is positive. The theorem packages this reasoning: positive total load and the existence of a positive site load are logically equivalent.

The result is a structural fact about the load layer of the framework's mass genesis account. It does not by itself identify the load with any physical mass value, and it does not invoke the phi-ladder mass law that connects loads to particle masses elsewhere in the framework. The theorem is a certificate that the load layer is internally consistent: the definition of nontriviality matches the behavior of the integrated load, and the load is invariant under the framework's pattern evolution operation, so the same pattern at a later tick carries the same total load.

theorem integratedMeaningLoad_pos_iff_nontrivial
    (ψ : LightPattern Λ) :
    0 < integratedMeaningLoad ψ ↔ NontrivialNeutralLoad ψ := by
  constructor
  · intro hpos
    by_contra hnot
    have hzero := integratedMeaningLoad_zero_of_not_nontrivial ψ hnot
    rw [hzero] at hpos
    exact (lt_irrefl (0 : ℝ)) hpos
  · exact integratedMeaningLoad_pos_of_nontrivial ψ

theorem integratedMeaningLoad_eq_support_sum (ψ : LightPattern Λ) :
    integratedMeaningLoad ψ =
      ψ.support.sum (fun x => siteMeaningLoad ψ x) := by
  rfl

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 theorem does not identify the load with any physical mass value. The theorem does not invoke the phi-ladder mass law. The theorem does not say anything about the framework's derivation of three spatial dimensions.

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: