Pith. sign in

Nuclear

Nuclear modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.

27 modules · 119 thm/lemma · 1133 lines
module thm lemma def lines papers
Nuclear.AlphaDecayGeiger2FromJCost 4 0 3 36 -
Nuclear.Alpha_Decay_RS5 4 0 3 36 -
Nuclear.BindingEnergy 12 0 4 167 -
Nuclear.FissionEnergyFromJCost 4 0 3 36 -
Nuclear.Iron_Peak_Binding_v2 4 0 3 36 -
Nuclear.NeutronLifetimeStructure 7 0 3 66 -
Nuclear.Neutron_EDM_v3 4 0 3 36 -
Nuclear.Neutron_Magnetic_Moment_RS 4 0 3 36 -
Nuclear.Nuclear 4 0 3 36 -
Nuclear.NuclearMagicNumbers2FromJCost 4 0 3 36 -
Nuclear.NuclearShell3FromJCost 4 0 3 36 -
Nuclear.Nuclear_Shell_Gap_RS 4 0 3 36 -
Nuclear.Nuclear_Symmetry_Energy_RS 4 0 3 36 -
Nuclear.Proton_Electric_Dipole_v3 4 0 3 36 -
Nuclear.Proton_Lifetime_Bound_RS 4 0 3 36 -
Nuclear.RS_NUC_Structural_001 4 0 3 36 -
Nuclear.RS_NUC_Structural_002 4 0 3 36 -
Nuclear.RS_NUC_Structural_003 4 0 3 36 -
Nuclear.RS_NUC_Structural_004 4 0 3 36 -
Nuclear.RS_NUC_Structural_005 4 0 3 36 -
Nuclear.RS_NUC_Structural_006 4 0 3 36 -
Nuclear.RS_NUC_Structural_007 4 0 3 36 -
Nuclear.RS_NUC_Structural_008 4 0 3 36 -
Nuclear.RS_NUC_Structural_009 4 0 3 36 -
Nuclear.RS_NUC_Structural_010 4 0 3 36 -
Nuclear.RadioactiveHalflife3FromJCost 4 0 3 36 -
Nuclear.SpontFission3FromJCost 4 0 3 36 -

full source mirrored from github.com/jonwashburn/shape-of-logic