torsion_differences

formal source

  34
  35/-! ## Torsion Schedule -/
  36
  37theorem torsion_differences :
  38    tau 1 - tau 0 = 11 ∧ tau 2 - tau 1 = 6 ∧ tau 2 - tau 0 = 17 := by
  39  simp only [tau, E_passive, W, passive_field_edges, cube_edges,
  40             active_edges_per_tick, D, wallpaper_groups]
  41  omega
  42
  43/-! ## CKM Structure from Torsion
  44
  45The Wolfenstein parametrization:
  46  |V_us| ~ λ ~ sin(θ_C)
  47  |V_cb| ~ λ²
  48  |V_ub| ~ λ³
  49
  50In RS, λ = φ^{-(τ₁ − τ₀)/some_scale}. The generation torsion
  51provides the hierarchy directly. -/
  52
  53noncomputable def cabibbo_parameter : ℝ := phi ^ (-(11 : ℤ))
  54
  55theorem cabibbo_parameter_pos : 0 < cabibbo_parameter := by
  56  unfold cabibbo_parameter
  57  exact zpow_pos phi_pos _
  58
  59noncomputable def rs_V_us : ℝ := cabibbo_parameter
  60noncomputable def rs_V_cb : ℝ := cabibbo_parameter ^ 2
  61noncomputable def rs_V_ub : ℝ := cabibbo_parameter ^ 3
  62
  63theorem ckm_hierarchy :
  64    rs_V_ub < rs_V_cb ∧ rs_V_cb < rs_V_us := by
  65  unfold rs_V_ub rs_V_cb rs_V_us
  66  have hc := cabibbo_parameter_pos
  67  have hc1 : cabibbo_parameter < 1 := by