module module

`IndisputableMonolith.Physics.NeutrinoMassScaleScoreCard`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Physics.NeutrinoSector module_import
IndisputableMonolith.Support.RungFractions module_import

declarations in this module (8)

theorem row_nu3_frac L32
theorem row_nu2_frac L36
theorem row_nu1_frac L40
theorem row_dm2_21_nufit L44
theorem row_dm2_31_nufit L48
theorem row_sqmass_ratio_phi7 L52
structure NeutrinoMassScaleScoreCardCert L57
theorem neutrinoMassScaleScoreCardCert_holds L76