Astrophysics

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

29 modules · 128 thm/lemma · 3014 lines

module	thm	lemma	def	lines	papers
`Astrophysics`	0	0	0	86	—
`Astrophysics.AccretionDiskFromJCost`	1	0	1	37	—
`Astrophysics.ChandrasekharMassStructure`	3	0	1	29	—
`Astrophysics.CoronalLyapunovTime`	4	0	3	87	—
`Astrophysics.CoronalTimescaleFromPhiLadder`	2	0	2	49	—
`Astrophysics.CosmicMagneticFieldsStructure`	2	0	1	22	—
`Astrophysics.ExoplanetHabitability`	4	0	6	115	—
`Astrophysics.FRBStructure`	2	0	1	21	—
`Astrophysics.FastRadioBurstFromBIT`	7	0	4	231	—
`Astrophysics.GalacticRotationCurveFromRS`	3	0	2	51	—
`Astrophysics.GalaxyMorphologyTypesFromConfigDim`	1	0	1	33	—
`Astrophysics.GravitationalWaveFromJCost`	2	0	2	46	—
`Astrophysics.MagneticReconnectionFromJCost`	1	0	1	39	—
`Astrophysics.MassToLight`	8	0	6	252	—
`Astrophysics.NucleosynthesisTiers`	7	1	8	210	—
`Astrophysics.ObservabilityLimits`	10	0	10	233	—
`Astrophysics.PICSimulationLyapunov`	3	0	3	72	—
`Astrophysics.PlanetaryFormationFromJCost`	11	0	3	232	—
`Astrophysics.PulsarEmissionRegimesFromRS`	3	0	2	50	—
`Astrophysics.PulsarPeriodFromRung`	11	0	7	257	—
`Astrophysics.SchumannResonanceFromBIT`	8	0	4	186	—
`Astrophysics.SolarWindFromMHD`	6	0	4	90	—
`Astrophysics.SolarWindFromPhiLadder`	2	0	2	48	—
`Astrophysics.StellarAssembly`	6	3	11	193	—
`Astrophysics.StellarEvolutionPhasesFromConfigDim`	1	0	1	34	—
`Astrophysics.StellarIMFStructure`	2	0	1	21	—
`Astrophysics.SupernovaMechanismStructure`	2	0	1	22	—
`Astrophysics.TidalLockingFromPhiResonance`	10	0	6	247	—
`Astrophysics.UHECRStructure`	2	0	1	21	—