`PMNSUnitarity`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.PMNS.Types
domain: Physics
line: 22 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.PMNS.Types on GitHub at line 22.

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

  19    Note: existence of such a `U` is currently treated as a quarantined conjecture
  20    (`IndisputableMonolith/Physics/PMNS/Construction.lean`). The certified particle
  21    claims do **not** depend on that existence statement. -/
  22structure PMNSUnitarity (U : Matrix (Fin 3) (Fin 3) ℂ) : Prop where
  23  unitary : Matrix.IsUnitary U
  24  matches_weights : ∀ i j, ‖U i j‖ ^ 2 =
  25    pmns_weight (IndisputableMonolith.RSBridge.rung (match i with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3) -
  26                 IndisputableMonolith.RSBridge.rung (match j with | 0 => .nu1 | 1 => .nu2 | 2 => .nu3)) / 3
  27
  28end IndisputableMonolith.Physics.PMNS

papers checked against this theorem

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