Masses Mass Genesis Admissibility Construction Admissibility Construction Cert

The admissibility certificate

In the Recognition Science framework, a particle's mass is not a free parameter. It is a quantity that must be read off a stable pattern of light, the framework's term for a discrete record of events. The declaration AdmissibilityConstructionCert is a formal certificate, a machine-checked collection of theorems, that packages the precise evidence needed to make that reading legitimate. It does not assert that any particular particle exists. It states what would have to be true for a pattern to be admissible as a massive particle.

The certificate assembles three pieces of evidence. First, the pattern must be stable, meaning it persists under the framework's evolution rule. Second, there must be a site density, a number assigned to each location in the pattern, that reads the neutral meaning load actually present there. Third, and hardest, the sum of those local loads over the pattern's support must equal the factorized mass law load, the expression that the framework's topology and closure conditions select. The certificate's central theorem proves that when all three hold, the pattern's rest mass equals its predicted mass, and its inertial and gravitational masses agree with that rest mass.

The certificate also records a tighter form of evidence. In that form, the only nontrivial datum left is the factorization claim itself: the actual neutral site loads, read directly from the pattern, must sum to the factorized mass law expression. The certificate shows that this canonical evidence suffices to close the full chain, yielding a stable, quantized pattern whose readout masses match its predicted mass.

What the certificate does not claim is equally important. It does not prove that every physical stable pattern has this evidence. That universal statement is kept as a named type, a target for future derivation from the framework's dynamics, not as an axiom. The certificate also does not fit any mass to data. It isolates the primitive evidence needed, so that downstream results can depend on explicit assumptions rather than silently assuming a bridge that has not been built.

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

/-- 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

The certificate does not prove that any particular particle exists. The certificate does not fit any mass value to experimental data. The certificate does not assert that every physical stable pattern is admissible; that remains a target.

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: