Masses Mass Genesis Admissibility Construction

The admissibility bridge

In Recognition Science, the framework that derives physical structure from a ledger of recognition events, mass is not put in by hand. The framework's library, a machine-checked collection of formal theorems, builds particle masses from the cost of recognition. The admissibility construction is the bridge that connects a raw, stable light pattern to a mass-carrying particle. It states precisely what evidence is needed for that bridge to hold, and it proves that once the evidence is present, the rest mass equals the predicted mass.

The construction works bottom-up. It starts with a light pattern, a discrete record of meaning loads at sites. The first requirement is stability: the pattern must be a stable closed orbit under the evolution rule. The second requirement concerns the local density used for mass. The module defines a primitive site load law: the density at each site must be the neutral meaning load actually present in the pattern, with no mass table or normalization target entering. The canonical choice is simply the already-defined neutral load, and the module proves this choice is nonnegative and reads the neutral load correctly.

The hard part is the third requirement, a factorization claim. It says the primitive site loads, summed over the support of the pattern, equal the factorized sector/rung/Z mass-law load selected by Q3 topology and Rhat closure. This claim is stated as a named type, not as an axiom, so downstream files must depend on explicit evidence rather than silently assuming the bridge. The module defines two evidence structures: a full one requiring stability, a site load law, and factorization; and a tighter canonical one requiring only stability and the canonical factorization, since the site load law is then automatic.

From either evidence structure, the module constructs a MassAdmissibleStablePattern, the object that the Mass Genesis theorem needs. The key theorems then follow. Given bottom-up evidence, the rest mass equals the predicted mass, and the full chain holds: the integrated meaning load is invariant under evolution, the rest mass is positive, the pattern is Phi-rung quantized, and the inertial and gravitational masses both equal the rest mass. A certificate structure packages these closure results, and a theorem-level statement says that if every physical stable pattern has bottom-up evidence, then all physical stable patterns are mass admissible.

What this establishes in plain language: the module does not assert that any particular particle has a mass. It isolates the exact primitive evidence needed, and proves that once that evidence is supplied, the entire mass chain closes. The remaining open target is the factorization theorem itself, to be derived from Q3/Rhat/CP6 dynamics. Until then, the bridge is fully specified but not yet crossed for physical patterns.

theorem restMass_eq_predictedMass_of_bottomUpEvidence
    (ψ : LightPattern Λ)
    (E : BottomUpAdmissibilityEvidence ψ) :
    restMass ψ = predictedMass ψ :=
  restMass_eq_predictedMass_of_massAdmissible
    (massAdmissible_of_bottomUpEvidence ψ E)

theorem full_chain_for_bottomUpEvidence
    (readout : PatternMassReadout Λ)
    (ψ : LightPattern Λ)
    (E : BottomUpAdmissibilityEvidence ψ)
    (hreads : ReadsStablePatternLoad readout ψ) :
    (∀ k : ℕ,
      integratedMeaningLoad (evolvePattern k ψ) = integratedMeaningLoad ψ) ∧
    0 < restMass ψ ∧
    PhiRungQuantized ψ ∧
    restMass ψ = predictedMass ψ ∧
    readout.inertialMass ψ = restMass ψ ∧
    readout.gravitationalMass ψ = restMass ψ :=
  admissiblePatternMassConclusion readout ψ
    (massAdmissible_of_bottomUpEvidence ψ E) hreads

/-- The canonical primitive site law is just the neutral CP6/Rhat load already
defined on the pattern. No mass table or normalization target enters here. -/
def canonicalPrimitiveSiteLoadLaw
    (ψ : LightPattern Λ) : PrimitiveSiteLoadLaw ψ where
  density := siteMeaningLoad ψ
  nonneg := fun x _hx => siteMeaningLoad_nonneg ψ x
  reads_neutral_load := fun _x _hx => rfl

What this page does not claim

The module does not assert that any particular physical particle has a mass. The factorization theorem is not proved; it is stated as a named type. The module does not derive the mass values themselves from first principles.

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