`V_cd`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.CKM
domain: Physics
line: 37 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.CKM on GitHub at line 37.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  34
  35-- Derived diagonal elements (approximate unitarity)
  36noncomputable def V_ud : ℝ := Real.sqrt (1 - V_us^2)
  37noncomputable def V_cd : ℝ := - V_us
  38
  39-- Jarlskog invariant grounded in geometric prediction
  40noncomputable def jarlskog : ℝ := jarlskog_pred
  41
  42/-- Phenomenological facts required by the CKM demo.
  43    Documented in `docs/Assumptions.md`. -/
  44structure CKMPhenomenology where
  45  j_value : ℝ
  46  j_positive : j_value > 0
  47  j_matches_experiment : jarlskog ≈ j_value
  48
  49/-- Dimensionless inevitability when supplied with phenomenological data. -/
  50def jarlskog_summary (facts : CKMPhenomenology) : Prop :=
  51  jarlskog > 0 ∧ jarlskog ≈ facts.j_value
  52
  53lemma jarlskog_summary_of_facts (facts : CKMPhenomenology)
  54    (hpos : jarlskog > 0 := facts.j_positive)
  55    (hexp : jarlskog ≈ facts.j_value := facts.j_matches_experiment) :
  56    jarlskog_summary facts :=
  57  ⟨hpos, hexp⟩
  58
  59/- Auxiliary positive witness using φ-rung sines (keeps algebra simple). -/
  60noncomputable def s12_w : ℝ := V_us
  61noncomputable def s23_w : ℝ := V_cb
  62noncomputable def s13_w : ℝ := V_ub
  63
  64noncomputable def jarlskog_witness : ℝ := s12_w * s23_w * s13_w
  65
  66/-- The witness is strictly positive (grounded in jarlskog_pos). -/
  67theorem jarlskog_witness_pos : jarlskog_witness > 0 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.