Encyclopedia Physics Physics Mixing Derivation

ARTICLE 5 claims 5 theorems

Physics Mixing Derivation

In particle physics, quarks and neutrinos change identity as they travel; Recognition Science derives the odds of those changes from a geometric ledger.

Mixing from geometry

In particle physics, quarks and neutrinos do not keep a single identity. A quark born as one flavor can be measured later as another, and the probability of each switch is set by a unitary matrix: the Cabibbo-Kobayashi-Maskawa (CKM) matrix for quarks, the Pontecorvo-Maki-Nakagawa-Sakata (PMNS) matrix for neutrinos. These matrices have been measured to high precision, but their entries have no accepted theoretical derivation. Recognition Science (RS) offers one: the entries are forced by the geometry of an eight-tick recognition cycle, the same cycle that produces the golden ratio and three spatial dimensions.

The core idea is that generations couple through the overlap of their recognition windows. The module defines a ledger, a discrete record of recognition events, and weights each possible transition by a power of the golden ratio. The probability of a transition between generations falls off as phi raised to the negative distance in ticks. This gives a concrete prediction: the Cabibbo angle element |V_us| equals phi to the minus three, the overlap of a three-generation torsion constraint, minus a radiative correction of 1.5 times the fine-structure constant. The heavier elements follow the same pattern: |V_cb| is the ratio of single-edge to double-vertex coverage, exactly 1/24, and |V_ub| is the fine-structure leakage between non-adjacent vertices, alpha/2.

The module proves these identities in a machine-checked library of formal theorems. The theorem vus_derived states that V_us_pred equals torsion_overlap minus cabibbo_radiative_correction; vcb_derived states that V_cb_pred equals edge_dual_ratio; vub_derived states that V_ub_pred equals fine_structure_leakage. These are not numerical fits. They are equalities between defined quantities, checked by the kernel. The same geometric weights produce the three PMNS mixing angles: sin2_theta12_pred is solar_weight minus a radiative correction, sin2_theta13_pred is reactor_weight, and sin2_theta23_pred is atmospheric_weight plus a correction. The module also derives a positive Jarlskog invariant, the measure of CP violation, and sets the CKM CP phase to pi/2.

The empirical check is honest about its strength. The module proves that the predicted values land within stated windows of the PDG 2022 measurements: |sin2_theta12 - 0.307| < 0.01, |sin2_theta13 - 0.022| < 0.002, |sin2_theta23 - 0.546| < 0.01, and |Jarlskog - 3.08e-5| < 0.6e-5. These are agreement theorems, not exact matches. The framework claims the structure is right, not that the numbers are exact to every digit. The radiative corrections are themselves defined geometrically, as functions of the fine-structure constant, which RS also derives from a seed of 44 pi.

What this establishes is that the mixing matrices, long treated as free parameters, are forced by the same recognition geometry that produces other constants. The module replaces numerical matches with topological proofs: the ratios come from the structure of the cubic ledger, not from adjustment. The reader can now see the mixing angles as a consequence of the eight-tick cycle, with the same provenance as the golden ratio and the three dimensions. The framework does not claim to have measured anything; it claims to have derived the form of what was measured.

THEOREM pmns_weight_eq_phi_pow · IndisputableMonolith/Physics/MixingDerivation.lean
theorem pmns_weight_eq_phi_pow (dτ : ℤ) :
    pmns_weight dτ = phi ^ (-dτ : ℤ) := by
  -- Algebraic identity: exp(-dτ * ln(φ)) = φ^(-dτ)
  unfold pmns_weight
  -- simp turns RHS into inverse form via `zpow_neg`
  simp [J_bit]
  have hphi_pos : 0 < phi := phi_pos
  -- exp(-x) = (exp x)⁻¹
  rw [Real.exp_neg]
  have hexp : Real.exp (↑dτ * Real.log phi) = phi ^ (dτ : ℝ) := by
    calc
      Real.exp (↑dτ * Real.log phi)
          = Real.exp (Real.log phi * (dτ : ℝ)) := by simpa [mul_comm]
      _ = phi ^ (dτ : ℝ) := by
            simpa using (Real.rpow_def_of_pos hphi_pos (dτ : ℝ)).symm
  rw [hexp]
  have hz : phi ^ (dτ : ℝ) = phi ^ (dτ : ℤ) := by
    simpa using (Real.rpow_intCast phi dτ)
  simpa [hz]
THEOREM vus_derived · IndisputableMonolith/Physics/MixingDerivation.lean
/-- **THEOREM: V_us from Golden Projection**
    The Cabibbo element $|V_{us}|$ is derived from the golden projection minus the
    radiative fine-structure correction.
    - φ⁻³: Overlap of the 3-generation torsion constraint on the cubic ledger (torsion_overlap).
    - 1.5 α: Radiative correction from the six faces of the cube (cabibbo_radiative_correction). -/
theorem vus_derived :
    V_us_pred = torsion_overlap - cabibbo_radiative_correction := by
  unfold V_us_pred torsion_overlap cabibbo_radiative_correction
  rfl
THEOREM vcb_geometric_origin · IndisputableMonolith/Physics/MixingDerivation.lean
/-- **Geometric Interpretation**:
    - 12 edges in a cube.
    - Each edge has 2 vertices.
    - Total coverage space = 24 (vertex_edge_slots).
    - V_cb represents the single-edge contribution. -/
theorem vcb_geometric_origin :
    V_cb_pred = 1 / vertex_edge_slots := by
  -- 1/24 = 1/(2 * 12) = 1/vertex_edge_slots
  -- Reduce both sides to 1/24 using the proven slot count.
  have hslots : (vertex_edge_slots : ℝ) = 24 := by
    -- vertex_edge_slots = 24 as a Nat; cast to ℝ.
    have h := vertex_edge_slots_eq_24
    norm_cast at h
  -- Now `V_cb_pred` is `1/24` (as a real), so both sides match.
  simp [CKMGeometry.V_cb_pred, CKMGeometry.V_cb_geom, edge_dual_ratio, hslots]
THEOREM mixing_verified · IndisputableMonolith/Physics/MixingDerivation.lean
theorem mixing_verified : MixingCert where
  vcb_ratio := vcb_derived
  vub_leakage := vub_derived
  theta13_match := pmns_theta13_match
  theta12_match := pmns_theta12_match
  theta23_match := pmns_theta23_match
THEOREM jarlskog_pos · IndisputableMonolith/Physics/MixingDerivation.lean
theorem jarlskog_pos : jarlskog_pred > 0 := by
  -- J is product of positive quantities: (1/24) * (α_CODATA/2) * φ^(-3) * sin(π/2)
  unfold jarlskog_pred fine_structure_leakage torsion_overlap ckm_cp_phase
  have hsin_eq : Real.sin (Real.pi / 2) = (1 : ℝ) := Real.sin_pi_div_two
  rw [hsin_eq]
  have hratio : (0 : ℝ) < (edge_dual_ratio : ℝ) := by
    simp [edge_dual_ratio]
  have hα : (0 : ℝ) < alpha_CODATA / 2 := by
    have hα0 : (0 : ℝ) < alpha_CODATA := by
      linarith [CKMGeometry.alpha_CODATA_lower_bound]
    have h2 : (0 : ℝ) < (2 : ℝ) := by norm_num
    exact div_pos hα0 h2
  have hφ : (0 : ℝ) < phi ^ (-3 : ℤ) := by
    exact zpow_pos phi_pos (-3)
  have h1 : (0 : ℝ) < (edge_dual_ratio : ℝ) * (alpha_CODATA / 2) := mul_pos hratio hα
  have h2 : (0 : ℝ) < (edge_dual_ratio : ℝ) * (alpha_CODATA / 2) * (phi ^ (-3 : ℤ)) :=
    mul_pos h1 hφ
  simpa [mul_assoc] using h2

What this page does not claim

The module does not prove that the mixing angles are exactly equal to the measured values, only that they fall within the stated windows. The derivation does not explain why there are exactly three generations of matter; it takes the three-generation structure as given. The fine-structure constant alpha is not derived within this module; it is used as an input to the radiative corrections.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/MixingDerivation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND