module module high

`IndisputableMonolith.Physics.MixingDerivation`

MixingDerivation derives the Cabibbo element |V_us| as the golden projection φ^{-3} minus the radiative correction (3/2)α from cubic ledger faces. Physicists extracting CKM parameters from Recognition Science geometry cite it to ground the observed value in torsion overlap. The module composes upstream geometry results into the explicit formula without new axioms.

claim$|V_{us}| = \phi^{-3} - rac{3}{2}\\,\alpha$, where $\phi^{-3}$ is the 3-generation torsion overlap on the cubic ledger and $\frac{3}{2}\\,\alpha$ is the fine-structure correction from the six cube faces.

background

The module operates in the Physics domain and imports Constants (RS time quantum τ₀ = 1 tick), CKMGeometry, MixingGeometry, and PMNSCorrections. CKMGeometry states: 'The CKM matrix elements |V_us|, |V_cb|, |V_ub| are not arbitrary parameters.' MixingGeometry supplies the cubic voxel topology that forces mixing parameters, while PMNSCorrections supplies the integer coefficients (6, 10, 3/2) for radiative terms.

The local setting is the Recognition Science ledger geometry in which mixing angles arise from φ-ladder rung differences and 8-tick octave closure rather than free parameters. The module doc-comment identifies the two ingredients of the V_us formula: torsion_overlap for the φ^{-3} term and cabibbo_radiative_correction for the α term.

proof idea

This is a definition and assembly module. It imports the geometric lemmas from CKMGeometry and MixingGeometry, then packages them into the explicit V_us statement given in the module doc-comment.

why it matters in Recognition Science

The module supplies the concrete V_us formula that CKM uses to derive the full matrix from rung differences τ_g = 0,11,17 and that CKMElementScoreCard compares to PDG data via V_us_pred = φ^{-3} - (3/2)α. It also feeds ParticleSummary and PMNSScoreCard. It closes the T11 hypothesis in CKMGeometry by converting the abstract ledger constraint into the numerical prediction.

scope and limits

Does not derive the full CKM matrix or Jarlskog invariant.
Does not compute numerical values or experimental error bands.
Does not address higher-order radiative corrections beyond the stated α term.
Does not treat PMNS mixing angles beyond the imported corrections.

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