module module high

`IndisputableMonolith.Physics.MixingDerivation`

MixingDerivation derives the Cabibbo element as |V_us| = φ^{-3} minus the (3/2)α radiative correction from cubic ledger torsion overlap. Flavor physicists cite it for parameter-free CKM predictions inside Recognition Science. The module assembles upstream results from CKMGeometry and MixingGeometry into explicit sibling formulas such as vus_derived.

claim$|V_{us}| = φ^{-3} - (3/2)α$, where φ^{-3} is the overlap of the 3-generation torsion constraint on the cubic ledger and (3/2)α is the radiative correction from the six faces of the cube.

background

Recognition Science derives all physics from one functional equation, forcing D=3 via the eight-tick octave and the Recognition Composition Law. Constants supplies the fundamental time quantum τ₀ = 1 tick. CKMGeometry states that the CKM matrix elements are not arbitrary parameters but follow from ledger geometry. MixingGeometry encodes the cubic voxel topology constraints that force the mixing parameters. PMNSCorrections supplies the geometric origin of the integer coefficients (6, 10, 3/2) appearing in radiative corrections.

proof idea

This is a derivation module. It defines vus_derived by direct subtraction of the cabibbo_radiative_correction from the golden projection φ^{-3} supplied by torsion_overlap. Parallel siblings (vcb_derived, vub_derived, pmns_weight) apply the same geometric projection pattern using results imported from CKMGeometry and MixingGeometry.

why it matters in Recognition Science

The module supplies the explicit element formulas consumed by the CKM module, which derives the full CKM matrix and Jarlskog invariant from φ-ladder rung differences. It also populates the predictions in CKMElementScoreCard and PMNSScoreCard, and supports ParticleSummary. It realizes the T11 hypothesis that CKM elements are geometrically determined rather than free parameters.

scope and limits

Does not derive the full CKM matrix or Jarlskog invariant.
Does not perform numerical evaluation or PDG comparison.
Does not address CP phases or Jarlskog construction.
Does not prove the underlying cubic ledger lemmas.

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