`Generation`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.CKM on GitHub at line 21.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  18namespace Physics
  19
  20-- Generations from τ_g in Anchor.rung
  21inductive Generation | first | second | third
  22deriving DecidableEq, Repr
  23
  24def tau_g (g : Generation) : ℤ :=
  25  match g with
  26  | .first => 0
  27  | .second => 11
  28  | .third => 17
  29
  30-- Grounded CKM elements from geometric predictions
  31noncomputable def V_us : ℝ := V_us_pred
  32noncomputable def V_cb : ℝ := V_cb_pred
  33noncomputable def V_ub : ℝ := V_ub_pred
  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

papers checked against this theorem

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