Pith. sign in

Astrophysics

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

137 modules · 548 thm/lemma · 6666 lines
module thm lemma def lines papers
Astrophysics 0 0 0 86 -
Astrophysics.AccretionDiskFromJCost 1 0 1 37 -
Astrophysics.AccretionLuminosityFromJCost 4 0 3 36 -
Astrophysics.Accretion_Disk_Stability3_FromJCost 4 0 3 36 -
Astrophysics.ActiveGalacticNucleiFromJCost 4 0 3 37 -
Astrophysics.AsteroidsFromPhiLadder_v2 3 0 3 25 -
Astrophysics.BinaryMergerRateFromJCost 4 0 3 36 -
Astrophysics.BinaryPulsarGW_FromJCost 4 0 3 37 -
Astrophysics.CMBTemperatureFromPhiLadder 4 0 3 37 -
Astrophysics.CMB_Lensing3_FromJCost 4 0 3 36 -
Astrophysics.ChandrasekharMassStructure 3 0 1 29 -
Astrophysics.Chandrasekhar_Exact_v2 4 0 3 36 -
Astrophysics.Chandrasekhar_Limit_RS 4 0 3 36 -
Astrophysics.Circumstellar3_FromJCost 4 0 3 36 -
Astrophysics.CoronalLyapunovTime 4 0 3 87 -
Astrophysics.CoronalTemperatureFromJCost 4 0 3 37 -
Astrophysics.CoronalTimescaleFromPhiLadder 2 0 2 49 -
Astrophysics.CosmicMagneticField_FromJCost 4 0 3 37 -
Astrophysics.CosmicMagneticFieldsStructure 2 0 1 22 -
Astrophysics.CosmicStrings_FromPhiLadder 4 0 3 47 -
Astrophysics.CosmicVoidSizeFromPhiLadder 4 0 3 51 -
Astrophysics.DarkEnergyDensityFromPhiLadder 4 0 3 47 -
Astrophysics.DarkMatterHaloFromJCost 4 0 3 37 -
Astrophysics.DustGrainSize3FromPhiLadder 4 0 3 36 -
Astrophysics.EventHorizonRadiusFromJCost 4 0 3 51 -
Astrophysics.ExoplanetAtmosphereFromJCost2 4 0 3 37 -
Astrophysics.ExoplanetDetection_BiasFromJCost 4 0 3 37 -
Astrophysics.ExoplanetHabitability 4 0 6 115 -
Astrophysics.ExoplanetOccurrenceFromJCost 4 0 3 37 -
Astrophysics.FRBStructure 2 0 1 21 -
Astrophysics.GRB5 4 0 3 36 -
Astrophysics.GRBJetAngle_FromJCost 4 0 3 36 -
Astrophysics.GRB_Afterglow3_FromJCost 4 0 3 36 -
Astrophysics.GRB_Duration_RS 4 0 3 36 -
Astrophysics.GalacticBarRotFromJCost 4 0 3 37 -
Astrophysics.GalacticFoundationFromJCost 4 0 3 37 -
Astrophysics.GalacticRotationCurveFromRS 3 0 2 51 -
Astrophysics.GalaxyClustering3_FromJCost 4 0 3 36 -
Astrophysics.GalaxyMorphologyTypesFromConfigDim 1 0 1 33 -
Astrophysics.GalaxySFR3_FromJCost 4 0 3 36 -
Astrophysics.Galaxy_Cluster_Mass3_FromJCost 4 0 3 36 -
Astrophysics.Galaxy_Formation3_FromJCost 4 0 3 36 -
Astrophysics.Galaxy_Metallicity3_FromJCost 4 0 3 36 -
Astrophysics.GammaBurstEnergyFromPhiLadder 4 0 3 37 -
Astrophysics.GammaRayBurstFromPhiLadder 4 0 3 47 -
Astrophysics.Gamma_Ray_Burst3_FromJCost 4 0 3 36 -
Astrophysics.Gamma_Ray_Line3_FromJCost 4 0 3 36 -
Astrophysics.GlobularClusterMetallicityFromJCost 4 0 3 37 -
Astrophysics.GravitationalLensingFromJCost 4 0 3 47 -
Astrophysics.GravitationalLensing_v2 3 0 3 25 -
Astrophysics.GravitationalWaveFromJCost 2 0 2 46 -
Astrophysics.Gravitational_Microlensing3 4 0 3 36 -
Astrophysics.GravitomagneticEffectFromJCost 4 0 3 37 -
Astrophysics.Hertzsprung_Russell_RS 4 0 3 36 -
Astrophysics.IntergalacticVoids_FromJCost 4 0 3 37 -
Astrophysics.InterstellarMolecules3FromJCost 4 0 3 36 -
Astrophysics.Jupiter_Orbital_Period_RS 4 0 3 36 -
Astrophysics.LenseThirringExactCert_v2 3 0 3 25 -
Astrophysics.Magnetar_Field_RS 4 0 3 36 -
Astrophysics.MagneticReconnectionFromJCost 1 0 1 39 -
Astrophysics.MassToLight 8 0 6 252 -
Astrophysics.MilliseconPulsarFromJCost 4 0 3 37 -
Astrophysics.NeutronStarCooling_FromJCost 4 0 3 36 -
Astrophysics.NeutronStarMassFromPhiLadder 4 0 3 51 -
Astrophysics.Neutron_Star_Mass3_FromJCost 4 0 3 36 -
Astrophysics.Neutron_Star_Max_Mass_RS 4 0 3 36 -
Astrophysics.Neutron_Star_Radius3_FromJCost 4 0 3 36 -
Astrophysics.Neutron_Star_Radius_RS 4 0 3 36 -
Astrophysics.Neutron_Star_Spin3_FromJCost 4 0 3 36 -
Astrophysics.NucleosynthesisTiers 7 1 8 210 -
Astrophysics.ObservabilityLimits 10 0 10 233 -
Astrophysics.PICSimulationLyapunov 3 0 3 72 -
Astrophysics.PlanckMassFromPhiLadder 4 0 3 47 -
Astrophysics.PlanetaryFormationFromJCost 11 0 3 232 -
Astrophysics.PlanetaryMigrationFromJCost 4 0 3 37 -
Astrophysics.ProtoplanetaryDiskMassFromJCost 4 0 3 37 -
Astrophysics.PulsarEmissionRegimesFromRS 3 0 2 50 -
Astrophysics.PulsarPeriodFromRung 11 0 7 257 -
Astrophysics.PulsarSpindownFromJCost 4 0 3 43 -
Astrophysics.Pulsar_Period_RS 4 0 3 36 -
Astrophysics.Pulsar_Timing3_FromJCost 4 0 3 36 -
Astrophysics.RS_AST_Structural_001 4 0 3 36 -
Astrophysics.RS_AST_Structural_002 4 0 3 36 -
Astrophysics.RS_AST_Structural_003 4 0 3 36 -
Astrophysics.RS_AST_Structural_004 4 0 3 36 -
Astrophysics.RS_AST_Structural_005 4 0 3 36 -
Astrophysics.RS_AST_Structural_006 4 0 3 36 -
Astrophysics.RS_AST_Structural_007 4 0 3 36 -
Astrophysics.RS_AST_Structural_008 4 0 3 36 -
Astrophysics.RS_AST_Structural_009 4 0 3 36 -
Astrophysics.RS_AST_Structural_010 4 0 3 36 -
Astrophysics.RS_Astro_Module_001 4 0 3 36 -
Astrophysics.RS_Astro_Module_002 4 0 3 36 -
Astrophysics.RS_Astro_Module_003 4 0 3 36 -
Astrophysics.RS_Astro_Module_004 4 0 3 36 -
Astrophysics.RS_Astro_Module_005 4 0 3 36 -
Astrophysics.RS_Astro_Module_006 4 0 3 36 -
Astrophysics.RS_Astro_Module_007 4 0 3 36 -
Astrophysics.RS_Astro_Module_008 4 0 3 36 -
Astrophysics.RS_Astro_Module_009 4 0 3 36 -
Astrophysics.RS_Astro_Module_010 4 0 3 36 -
Astrophysics.RS_Astro_Module_011 4 0 3 36 -
Astrophysics.RS_Astro_Module_012 4 0 3 36 -
Astrophysics.ReionizationEpochFromJCost 4 0 3 47 -
Astrophysics.Saturn_Ring_Radius_RS 4 0 3 36 -
Astrophysics.SolarWindFromPhiLadder 2 0 2 48 -
Astrophysics.Solar_Luminosity_RS 4 0 3 36 -
Astrophysics.Solar_Radius_RS 4 0 3 36 -
Astrophysics.StarClusterMassFromPhiLadder 4 0 3 47 -
Astrophysics.Star_Cluster3_FromJCost 4 0 3 36 -
Astrophysics.StarburstGalaxiesFromJCost 4 0 3 37 -
Astrophysics.StellarAssembly 6 3 11 193 -
Astrophysics.StellarEvolutionPhasesFromConfigDim 1 0 1 34 -
Astrophysics.StellarIMFStructure 2 0 1 21 -
Astrophysics.StellarMassFunction_FromPhiLadder 4 0 3 37 -
Astrophysics.StellarNucleosynthesisFromPhiLadder 4 0 3 47 -
Astrophysics.StellarPopulation_FromConfigDim 4 0 3 36 -
Astrophysics.StellarWind5 4 0 3 36 -
Astrophysics.StellarWindFromPhiLadder 4 0 3 51 -
Astrophysics.Stellar_Evolution3_FromJCost 4 0 3 34 -
Astrophysics.Stellar_Metallicity_Mean_RS 4 0 3 36 -
Astrophysics.Stellar_Oscillation3_FromJCost 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod31 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod41 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod51 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod61 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod71 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod81 4 0 3 36 -
Astrophysics.Structural_Astrophysics_mod91 4 0 3 36 -
Astrophysics.SupernovaMechanismStructure 2 0 1 22 -
Astrophysics.SupernovaNucleoFromPhiLadder 4 0 3 47 -
Astrophysics.Supernova_Kickvelocity2 4 0 3 36 -
Astrophysics.TidalLockingFromPhiResonance 10 0 6 247 -
Astrophysics.UHECRStructure 2 0 1 21 -
Astrophysics.UltraHighEnergyCosmicRay 4 0 3 37 -
Astrophysics.WhiteDwarfMassFromPhiLadder 4 0 3 47 -
Astrophysics.White_Dwarf_Radius_RS 4 0 3 36 -

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