def
definition
pmns_unitarity_exists
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.PMNS.Construction on GitHub at line 13.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
10
11This is *not* used for any of the hard‑falsifiable angle / mass‑splitting claims
12in `IndisputableMonolith.Physics.MixingDerivation`. -/
13def pmns_unitarity_exists : Prop :=
14 ∃ U : Matrix (Fin 3) (Fin 3) ℂ, PMNSUnitarity U
15
16end IndisputableMonolith.Physics.PMNS