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

IndisputableMonolith.Physics.CKM

show as:
view Lean formalization →

The CKM module collects phenomenological facts and constants for the CKM matrix demonstration. It pulls geometric derivations of mixing angles from ledger structure and the fine-structure constant via its imports. Researchers testing quark flavor predictions against data would cite these facts to close the loop from geometry to observables. The module consists of definitions and summaries with no new theorems.

claimPhenomenological inputs for the CKM matrix $V$ with elements $|V_{us}|$, $|V_{cb}|$, $|V_{ub}|$ and Jarlskog invariant $J$, drawn from ledger geometry and fine-structure constant.

background

The module sits inside Phase 7.2 on CKM and PMNS mixing. It imports CKMGeometry (T11), which states that the CKM elements are not arbitrary parameters but follow from ledger geometry and the fine-structure constant, and MixingDerivation, which derives the elements from cubic ledger structure via edge-dual coupling between generations. The supplied facts are documented in Assumptions.md and appear as sibling definitions such as V_us, V_cb, jarlskog and CKMPhenomenology.

proof idea

This is a definition module, no proofs. It imports the two upstream modules to expose the geometric derivations and then declares the required phenomenological constants and summary facts.

why it matters in Recognition Science

The module supplies the inputs required by sibling declarations CKMPhenomenology and jarlskog_summary, thereby supporting the CKM demonstration that follows T11. It closes the passage from the geometric derivation in MixingDerivation to observable values without adding new theorems.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)