pith. sign in
module module high

IndisputableMonolith.Physics.ParticleSummary

show as:
view Lean formalization →

This module aggregates derivations of all Standard Model parameters from Recognition Science. It collects lepton masses, quark masses, mixing matrices, anomalous moments, and neutrino scales into one reference. Physicists testing RS predictions against data would cite it. The module contains no proofs and serves only as an aggregator of its eight imported submodules.

claimStandard Model parameters (lepton masses $m_e, m_μ, m_τ$, quark masses, CKM/PMNS matrices, anomalous moments $a_l$, neutrino mass scale) derived from the Recognition Science $φ$-ladder, J-cost function, and cubic geometry constraints.

background

The module imports eight specialized submodules. AnomalousMoments derives $a_l = (g-2)/2$ via $φ$-ladder residue corrections with a universal RS term for all charged leptons sharing $Z=1332$. Hadrons supplies hadron mass relations and Regge slopes from composite rungs and eight-beat binding. LeptonGenerations.Necessity proves muon and tau masses forced from the electron mass via T9 and geometric constants. MixingDerivation and MixingGeometry formalize CKM and PMNS elements from cubic ledger topology and edge-dual coupling. NeutrinoSector places neutrinos on the deep ladder at even integers near rung $-50$. QuarkMasses and RunningCouplings complete the parameter set.

proof idea

This is a definition module, no proofs. It structures the particle summary solely by importing and organizing results from the eight listed modules without adding new theorems or reductions.

why it matters in Recognition Science

This module completes the particle-physics section of the Recognition Science framework by collecting every derived Standard Model quantity. It realizes the module doc-comment goal of obtaining SM parameters from the $φ$-ladder and geometric constraints. It supplies the reference object for downstream comparisons such as those in sibling SMDerivation and derived_parameters.

scope and limits

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (2)