pith. sign in
module module high

IndisputableMonolith.Physics.MixingDerivation

show as:
view Lean formalization →

MixingDerivation derives the leading CKM element |V_us| as the golden-ratio projection phi^{-3} minus a 3/2 alpha radiative term fixed by cubic-face counting, together with parallel expressions for |V_cb|, |V_ub| and the three PMNS sin^2 theta predictions. A physicist fitting quark or neutrino mixing data would cite the module for its parameter-free outputs that land inside PDG bands. The derivations are assembled from geometric overlap rules imported from CKMGeometry and MixingGeometry rather than from free parameters or numerical fits.

claim|V_{us}| = phi^{-3} - (3/2) alpha, with |V_{cb}| = 1/24 and |V_{ub}| = alpha/2 obtained from rung differences on the phi-ladder; sin^2 theta_{12}, sin^2 theta_{23}, sin^2 theta_{13} likewise fixed by torsion weights and eight-tick closure.

background

The module operates inside the Recognition Science setting in which mixing matrices are forced by cubic voxel topology and the phi-ladder. Core objects are the golden projection phi^{-3} (torsion overlap of the three-generation constraint on the cubic ledger) and the cabibbo_radiative_correction (1.5 alpha arising from the six faces of the cube). It imports the RS time quantum tau_0 = 1 tick from Constants and the hypothesis from CKMGeometry that CKM elements are not arbitrary parameters but outputs of ledger geometry. PMNSCorrections supplies the integer coefficients (6, 10, 3/2) that appear in the PMNS angle formulae, including the reactor prediction sin^2 theta_{13} = phi^{-8}.

proof idea

The module is a derivation module whose structure consists of a sequence of named definitions: vus_derived applies the golden projection minus the radiative term; cabibbo_correction_geometric isolates the 1.5 alpha factor; vcb_derived and vub_derived repeat the pattern for the heavier elements; pmns_weight, pmns_prob and the three sin2_theta*_pred definitions encode the neutrino-sector weights from eight-tick octave closure. No tactic scripts are shown; each line is a direct algebraic transcription of the geometric rules supplied by the imported modules.

why it matters in Recognition Science

The derivations supply the explicit expressions consumed by the CKM module for the Jarlskog invariant and by CKMElementScoreCard for the Phase-2 scorecard that compares V_us_pred = phi^{-3} - (3/2)alpha against the PDG value 0.22500. They also feed ParticleSummary and PMNSScoreCard for the full set of mixing predictions. The module therefore closes the T11 step of the CKM Matrix Geometry hypothesis and supplies the concrete phi-ladder and torsion-overlap content required by the eight-tick octave and D=3 spatial constraints of the Recognition Science chain.

scope and limits

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (25)