Pith. sign in
module module high

IndisputableMonolith.Physics.CKMGeometry

show as:
view Lean formalization →

The CKMGeometry module supplies geometric definitions for CKM matrix elements, centering on the relation that sets V_ub equal to half the fine-structure constant via leakage from the cubic ledger. Particle physicists deriving quark mixing parameters from RS geometry without empirical fits would cite these expressions. The module consists of targeted definitions that link alpha-derived quantities to specific CKM predictions.

claim$V_{ub} = \alpha/2$ (fine-structure leakage); $V_{cb}^{\rm pred} = 1/24$; $V_{us}^{\rm pred} = \phi^{-3} - (3/2)\alpha$

background

The module sits inside the Recognition Science derivation of physics from the cubic ledger Q3. It imports the RS time quantum τ₀ = 1 tick from Constants, the constructive derivation of α⁻¹ via Gauss-Bonnet vertex deficits from AlphaDerivation, and rigorous interval bounds on φ and α from the Numerics.Interval modules. PhiSupport supplies the identity φ² = φ + 1 that underpins the phi-ladder rung assignments.

Local notation follows MixingGeometry for edge-dual couplings between generations. The module therefore translates ledger geometry directly into CKM element magnitudes without additional fitting parameters.

proof idea

This is a definition module, no proofs. It assembles the listed sibling definitions (V_ub_pred, V_cb_pred, V_us_pred, V_cb_geom, V_cb_match) by direct substitution of the alpha and phi expressions already established in the imported Alpha and PhiBounds modules.

why it matters in Recognition Science

The definitions feed CKMElementScoreCard for direct comparison of geometric predictions against PDG values, CKM for the Jarlskog invariant construction, MixingDerivation for the full topological proof of the mixing matrix, and HubbleTension for the dark-energy density link. The module thereby supplies the explicit V_ub = α/2 step required by the phi-ladder application to quark generations.

scope and limits

used by (4)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (20)