module module high

`IndisputableMonolith.Physics.MixingDerivation`

Module derives the Cabibbo element |V_us| as the golden projection φ^{-3} minus the (3/2)α radiative correction from cubic ledger torsion. CKM and particle spectrum researchers cite it to obtain mixing parameters from geometry rather than free inputs. Argument assembles torsion_overlap and cabibbo_radiative_correction terms imported from CKMGeometry and MixingGeometry.

claim$|V_{us}| = \phi^{-3} - \frac{3}{2}\alpha$, where $\phi^{-3}$ encodes the 3-generation torsion overlap on the cubic ledger and $\frac{3}{2}\alpha$ encodes the six-face radiative correction.

background

The module operates inside the Recognition Science treatment of mixing matrices as forced outputs of cubic voxel topology. MixingGeometry introduces the cubic ledger constraints that enforce torsion overlap for three generations. CKMGeometry supplies the T11 framework that links those constraints to the fine-structure constant α, while PMNSCorrections supplies the integer coefficients (6, 10, 3/2) for radiative adjustments. Constants fixes the base unit τ₀ = 1 tick.

proof idea

This module collects sibling derivations without a central proof body. Each declaration (vus_derived, vcb_derived, vub_derived, pmns_weight, sin2_theta*_pred) applies one geometric projection step drawn from the imported CKMGeometry and MixingGeometry modules. The structure is a sequence of independent algebraic reductions, each using torsion_overlap or cabibbo_radiative_correction.

why it matters in Recognition Science

Supplies the explicit geometric formulas for CKM elements that the downstream CKM module assembles into the full matrix and Jarlskog invariant. It also populates CKMElementScoreCard and PMNSScoreCard with RS-native predictions. It realizes the T11 hypothesis that CKM elements arise from ledger geometry and the D=3 cubic structure rather than free parameters.

scope and limits

Does not derive the full CKM matrix or Jarlskog invariant.
Does not compute numerical values or error bands.
Does not address CP violation phases or higher-order corrections.
Does not derive PMNS mixing angles, only weights and probabilities.

used by (4)

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

IndisputableMonolith.Physics.CKM module_import
IndisputableMonolith.Physics.CKMElementScoreCard module_import
IndisputableMonolith.Physics.ParticleSummary module_import
IndisputableMonolith.Physics.PMNSScoreCard module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.MixingGeometry module_import
IndisputableMonolith.Physics.PMNSCorrections module_import

declarations in this module (25)

theorem vus_derived L37
theorem cabibbo_correction_geometric L43
theorem vcb_derived L56
theorem vub_derived L68
theorem vcb_geometric_origin L78
def pmns_weight L93
theorem pmns_weight_eq_phi_pow L96
def pmns_prob L119
def sin2_theta12_pred L127
def sin2_theta23_pred L128
def sin2_theta13_pred L129
theorem pmns_theta23_match L133
theorem atmospheric_correction_geometric L144
theorem pmns_theta13_match L151
theorem pmns_theta12_match L191
theorem solar_correction_geometric L223
structure MixingCert L229
theorem mixing_verified L236
theorem pmns_theta12_born_forced L246
theorem pmns_theta23_born_forced L251
theorem pmns_theta13_born_forced L256
def ckm_cp_phase L269
def jarlskog_pred L277
theorem jarlskog_match L284
theorem jarlskog_pos L331