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

IndisputableMonolith.Physics.CKMGeometry

show as:
view Lean formalization →

The CKMGeometry module supplies geometric definitions for the leading CKM matrix elements in the Recognition Science framework, with the up-bottom element fixed at half the fine-structure constant. Quark-mixing researchers and cosmologists would cite these when matching phi-ladder predictions to PDG values or resolving Hubble tension. The module consists of direct definitions assembled from upstream alpha and phi interval bounds.

claimThe predicted CKM elements satisfy $V_{ub}^{pred} = α/2$, $V_{cb}^{pred} = 1/24$, $V_{us}^{pred} = φ^{-3} - (3/2)α$, together with experimental counterparts $V_{us}^{exp}$, $V_{cb}^{exp}$, $V_{ub}^{exp}$ and geometric constructions such as $V_{cb}^{geom}$ and $V_{cb}^{from cube edges}$.

background

This module sits inside the Recognition Science derivation of physics from the cubic ledger, importing the RS time quantum τ₀ = 1 tick, the constructive derivation of α^{-1} via Gauss-Bonnet vertex deficits on Q₃, and rigorous interval bounds on both φ and α^{-1}. It defines the CKM predictions that later modules use to obtain mixing angles θ_{ij} ~ φ^{-Δτ/2} from rung differences τ_g = 0, 11, 17. The local setting therefore treats the fine-structure constant as a geometric leakage term that directly sets the smallest mixing element.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

CKMGeometry supplies the concrete geometric expressions imported by Physics.CKM and MixingDerivation to obtain the full CKM matrix and Jarlskog invariant J as a forced dimensionless output. It also feeds the CKMElementScoreCard for phase-2 magnitude comparisons and the HubbleTension module for cosmological applications. The central relation V_ub = α/2 closes the fine-structure leakage step in the T0-T8 forcing chain.

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)