pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Masses.Basic

show as:
view Lean formalization →

This module supplies exponent definitions for surrogate mass ladder differences as paper placeholders within the Recognition Science framework. Physicists comparing predicted particle masses to PDG data would reference these when auditing the phi-ladder structure. The module consists of three sibling declarations that encode rung differences and matching predicates without committing to numerical evaluation or full proofs.

claimThe module defines the rung exponent map $rung_exponent : rung → exponent$ together with the predicates $mass_ladder_matches_pdg$ and $mass_ladder_holds$ that encode surrogate ladder differences under the mass_ladder_assumption.

background

Recognition Science computes masses via the phi-ladder formula yardstick × ϕ^(rung − 8 + gap(Z)). The module imports the RS time quantum τ₀ = 1 tick from Constants and the lightweight mass_ladder_assumption placeholder from Assumptions, which centralises phenomenological predicates for the model layer. These definitions sit upstream of any concrete mass audit and remain intentionally non-committal.

proof idea

This is a definition module, no proofs. It declares the exponent function and two matching predicates as direct scaffolding objects that later modules can instantiate or discharge.

why it matters in Recognition Science

The module feeds the mass ladder audit steps that verify predictions against experimental data in the Recognition Science masses domain. It supplies the placeholder rung differences required by the overall mass formula and connects to the phi-ladder construction. It touches the open question of exact numerical agreement with PDG values.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (3)