def
definition
experiments
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.StandardModel.PMNSMatrix on GitHub at line 321.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
curvature_defect_strength -
defect_site_prediction -
dama_not_dark_matter_in_rs -
substrate_model -
energy_conservation -
m_coh_positive -
equivalence_implies_ratio_one -
H_GravitationalRunning_certificate -
experimentalStatus -
quantum_requires_complex -
BellFalsifier -
loopholeFreeExperiment -
rsPredictions -
experimentalStatus -
experiments -
predictions -
experiments -
experimentalTests -
possibleTests -
relativity_preserved -
experiments -
experimentalEvidence -
quadratic_from_symmetry -
shadow_diameter_correction -
deltaCP_pmns_range -
experimentalStatus
formal source
318 2. **Hyper-K**: Precision θ₂₃ measurement
319 3. **JUNO**: θ₁₂ precision, mass ordering
320 4. **0νββ**: Majorana nature test -/
321def experiments : List String := [
322 "DUNE: δ_CP precision",
323 "Hyper-Kamiokande: θ₂₃, CP violation",
324 "JUNO: θ₁₂, mass ordering",
325 "Neutrinoless double beta decay"
326]
327
328/-! ## Falsification Criteria -/
329
330/-- The derivation would be falsified if:
331 1. No φ-connection to any mixing angle
332 2. Inverted mass ordering confirmed
333 3. δ_CP far from π (e.g., ~0 or π/2) -/
334structure PMNSFalsifier where
335 no_phi_connection : Prop
336 inverted_ordering : Prop
337 deltaCP_not_near_pi : Prop
338 falsified : no_phi_connection ∧ inverted_ordering ∧ deltaCP_not_near_pi → False
339
340end PMNSMatrix
341end StandardModel
342end IndisputableMonolith