pith. machine review for the scientific record. sign in
def definition def or abbrev

pmns_weight

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  12noncomputable def pmns_weight (dτ : ℤ) : ℝ :=

proof body

Definition body.

  13  Real.exp (- (dτ : ℝ) * J_bit)
  14
  15/-- **DEFINITION: PMNS Unitarity Forcing**
  16    A matrix `U` satisfies `PMNSUnitarity U` if it is unitary and its Born-rule
  17    probabilities `‖U i j‖^2` match the framework’s predicted weight tensor.
  18
  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. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.