Masses Mass Genesis Admissibility Construction Bottom Up Canonical Admissibility

The admissibility evidence

A light pattern is, in this framework, a discrete record of recognition events distributed across a lattice. The declaration BottomUpCanonicalAdmissibilityEvidence is a checklist: it names the two pieces of evidence a pattern must provide before the framework's mass theorems apply to it. The first is stability, meaning the pattern persists under the framework's evolution rule. The second is a factorization claim, that the local density of meaning read directly from the pattern sums, over the pattern's support, to the mass value the framework's topology-based law predicts.

The factorization is the load-bearing part. The framework's mass law is built from sector, rung, and Z factors selected by Q3 topology and Rhat closure. The declaration says the actual neutral load present in the light pattern must equal that factorized expression when summed. This is not asserted as true; it is stated as a condition. The declaration is a structure, a named type that downstream theorems can require as an explicit hypothesis rather than silently assume.

What the declaration establishes is a bridge. Given the two pieces of evidence, the framework's library proves a chain: the pattern's rest mass equals its predicted mass, its integrated meaning load is conserved under evolution, its mass is positive, it is PhiRung quantized, and its inertial and gravitational masses both equal the rest mass. These are results in the machine-checked library, each with its proof anchored to the evidence structure.

What the declaration does not claim is that any actual physical pattern satisfies the evidence. The hard result, that every stable pattern arising from the underlying Q3/Rhat/CP6 dynamics carries this evidence, is kept as a named type, not an axiom. It remains a target. The declaration also does not assert any reverse-fitted mass value; no mass table and no normalization target enters the primitive site load law. The canonical law simply reads the neutral load already defined on the pattern.

In plain terms: the declaration says "if a pattern is stable and its neutral load sums to the predicted mass, then all the mass results follow." It leaves open whether any real pattern meets those conditions. That separation is the point. The framework can build its mass theory on explicit, checkable evidence, and mark clearly where the physics still has work to do.

/-- Tighter evidence form: the only remaining nontrivial datum is the canonical
support-sum factorization of the actual neutral load. -/
structure BottomUpCanonicalAdmissibilityEvidence (ψ : LightPattern Λ) where
  stable : StableClosedLightPattern ψ
  load_factorizes : CanonicalPrimitiveLoadFactorizes ψ

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

/-- This is the next theorem to prove from Q3/Rhat/CP6 dynamics. It is kept as
a named type, not an axiom, so downstream files can depend on explicit evidence
instead of silently assuming the bridge. -/
def EveryPhysicalStablePatternHasBottomUpEvidence
    (PhysicalStable : LightPattern Λ → Prop) : Type _ :=
  ∀ ψ : LightPattern Λ,
    PhysicalStable ψ →
      BottomUpAdmissibilityEvidence ψ

What this page does not claim

No physical light pattern is asserted to satisfy the evidence. No reverse-fitted mass value is asserted or implied. The hard result that all stable patterns carry the evidence is not proved, only named as a target type.

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: