Masses Mass Genesis Integrated Load

The integrated load

In the Recognition Science framework, a ledger is a discrete record of recognition events, and a pattern is a finite configuration of such events on a substrate. The integrated meaning load is the total cost assigned to a pattern: it sums, over every site the pattern occupies, a local measure of how much meaning that site carries after neutralization. Neutralization here means removing the pattern's internal symmetries, so the load reflects only the irreducible content at each location.

The results show that this total load behaves exactly as a well-founded measure should. It is always nonnegative, it is zero precisely when no site carries positive load, and it is positive exactly when at least one site does. These three facts are established in the machine-checked library of formal theorems. The proofs are purely bottom-up: the site load is defined first, then the integrated load is the finite sum over the pattern's support, and the properties of the sum follow from the properties of the site loads.

The load is also invariant under a natural evolution operation. Shifting a pattern by any number of steps in its recognition cycle leaves both the site loads and the integrated load unchanged. This means the total meaning content of a pattern is a stable quantity, not an artifact of where the cycle happens to start. Two patterns with the same support and the same site loads on that support have the same integrated load, so the measure depends only on the local data, not on any global shape.

In Recognition Science, this integrated load is the algebraic foundation for the phi-ladder mass law. The results close the load layer cleanly: they establish the measure's basic properties without yet identifying the load with any specific mass value. That identification, the step from load to the golden-ratio ladder of particle masses, is a separate layer that this work deliberately does not touch.

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

theorem integratedMeaningLoad_zero_iff_not_nontrivial
    (ψ : LightPattern Λ) :
    integratedMeaningLoad ψ = 0 ↔ ¬ NontrivialNeutralLoad ψ := by
  constructor
  · exact not_nontrivial_of_integratedMeaningLoad_zero ψ
  · exact integratedMeaningLoad_zero_of_not_nontrivial ψ

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_of_evolvePattern
    (ψ : LightPattern Λ) (k : ℕ) :
    integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ :=
  integratedMeaningLoad_eq_of_sameLoadOnSupport
    (sameLoadOnSupport_evolvePattern ψ k)

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

What this page does not claim

This module does not identify the integrated load with any specific mass value on the phi-ladder. The module does not prove the phi-ladder mass law itself. The load is defined for finite-support patterns only, not for arbitrary infinite configurations.

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: