structure definition def or abbrev

`PMNSElement`

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

formal statement (Lean)

 168structure PMNSElement where
 169  /-- From flavor (e, μ, τ). -/
 170  fromFlavor : Fin 3
 171  /-- To mass eigenstate (1, 2, 3). -/
 172  toMass : Fin 3
 173  /-- Mixing amplitude. -/
 174  amplitude : ℂ
 175
 176/-- **THEOREM (Neutrino Generations = Charged Lepton Generations)**:
 177    Both are 3 because both arise from the same 8-tick × 3D structure. -/

depends on (7)

Lean names referenced from this declaration's body.

tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
Lepton in IndisputableMonolith.CrossDomain.CubeFaceUniversality decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
Lepton in IndisputableMonolith.Physics.AnomalousMoments decl_use
amplitude in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
amplitude in IndisputableMonolith.Quantum.DoubleSlit decl_use