pith. sign in
module module high

IndisputableMonolith.Physics.CKMGeometry

show as:
view Lean formalization →

This module supplies geometric definitions for CKM matrix elements using the phi-ladder and fine-structure leakage from the cubic ledger. Quark-mixing researchers and cosmologists would cite its predictions for |V_us|, |V_cb|, |V_ub|. It assembles constant definitions from AlphaDerivation and MixingGeometry imports with no internal proofs.

claimThe module defines $V_{ub} = α/2$ (fine-structure leakage), $V_{us, pred} = φ^{-3} - (3/2)α$, $V_{cb, pred} = 1/24$, together with experimental values $V_{us, exp}$, $V_{cb, exp}$, $V_{ub, exp}$ and error bands.

background

This module operates in the Physics domain and imports the RS time quantum τ₀ = 1 tick, the phi equation φ² = φ + 1, and the complete constructive derivation of α⁻¹ from cubic-vertex deficits (Gauss-Bonnet) in AlphaDerivation. It further imports interval bounds on φ and α⁻¹ plus the MixingGeometry layer that encodes edge-dual couplings on the cubic ledger. The central relation supplied here is that V_ub arises directly as fine_structure_leakage, i.e., half the fine-structure constant.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the RS-native CKM predictions V_us_pred = φ^{-3} - (3/2)α, V_cb_pred = 1/24, V_ub_pred = α/2 that are referenced verbatim in CKMElementScoreCard and feed the full CKM matrix construction in Physics.CKM and MixingDerivation. It realizes the fine_structure_leakage step that connects the cubic ledger geometry to observed quark mixing and is imported by HubbleTension analyses.

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)