Pith. sign in

Cosmology

Cosmological identities. The η_B baryon asymmetry as the φ-rung 44 result, prefactor derivations.

159 modules · 1340 thm/lemma · 24000 lines
module thm lemma def lines papers
Cosmology.Alcock5 4 0 3 36
Cosmology.BBNHeliiumExact3FromJCost 4 0 3 36
Cosmology.BITKernelFamilies 7 0 5 123
Cosmology.BITKernelShapeForcing 20 1 12 343
Cosmology.Baryogenesis3_FromJCost 4 0 3 36
Cosmology.BaryogenesisFromJCost 3 0 1 49
Cosmology.BaryogenesisStaging 124 0 46 1564
Cosmology.BaryogenesisTrajectoryFromPhiLadder 4 0 2 73
Cosmology.BaryonAsymmetryDerivation 5 0 5 260
Cosmology.BaryonAsymmetryExact 14 0 8 288
Cosmology.BaryonAsymmetryFromPhiLadder 8 0 3 82
Cosmology.BaryonDensityExact2FromJCost 4 0 3 36
Cosmology.BaryonHigherOrder 17 0 4 219
Cosmology.Baryon_Density_RS 4 0 3 36
Cosmology.CDMDensityParameterFromRS 2 0 2 41
Cosmology.CMBAcousticPeakRatios 9 0 5 200
Cosmology.CMBOpticalDepth3FromJCost 4 0 3 36
Cosmology.CMBPolarization3_FromJCost 4 0 3 36
Cosmology.CMBPolarizationRatio3FromJCost 4 0 3 36
Cosmology.CMBTemp3_FromJCost 4 0 3 36
Cosmology.CMB_Damping_Scale_v3 4 0 3 36
Cosmology.CMB_Power_Spectrum_Peaks_v3 4 0 3 36
Cosmology.CosmicInflationFromJCost 2 0 1 43
Cosmology.CosmicMicrowaveBackgroundFromRS 3 0 6 57
Cosmology.CosmicStrings4_FromJCost 4 0 3 36
Cosmology.CosmicZHistory 10 0 4 171
Cosmology.CosmicZScaleLaw 7 0 4 168
Cosmology.CosmogenesisSim 17 0 10 237
Cosmology.CosmologicalConstant 4 0 15 236
Cosmology.CosmologicalConstantDerivation 10 4 4 248
Cosmology.Cosmology 4 0 3 36
Cosmology.DarkEnergy 9 0 15 229
Cosmology.DarkEnergy5 4 0 3 36
Cosmology.DarkEnergyDensity4FromJCost 4 0 3 36
Cosmology.DarkEnergyEOS 3 0 3 100
Cosmology.DarkEnergyEquation3_FromJCost 4 0 3 36
Cosmology.DarkEnergyEquationOfState 1 0 3 47
Cosmology.DarkEnergyEquationOfStateDepth 4 0 2 66
Cosmology.DarkEnergyEvolutionStructure 6 0 1 55
Cosmology.DarkEnergyScaleAffinityDerivation 5 0 3 150
Cosmology.DarkEnergyWofZStructural 22 0 7 346
Cosmology.DarkMatterXENONPrediction 2 0 3 52
Cosmology.Dark_Matter_Density_RS 4 0 3 36
Cosmology.DomainCoarsening 7 0 2 106
Cosmology.DomainCoarsening2D 7 0 2 97
Cosmology.DomainCoarsening3D 6 0 1 127
Cosmology.EWPhaseTransition 9 0 8 202
Cosmology.EarlyUniverse 5 0 1 104
Cosmology.EntropyConservationFRW 10 0 0 344
Cosmology.EntropyPerPhoton 13 18 12 361
Cosmology.EtaBExactRungDerivation 17 0 3 322 2
Cosmology.EtaBIntervalCert 8 4 1 170
Cosmology.EtaBPrefactorDerivation 24 2 2 348 1
Cosmology.FermionWeight 3 6 0 165
Cosmology.FermionWeightIntegral 4 13 2 302
Cosmology.FiniteCellBoundary 1 0 0 34
Cosmology.FlatnessProblem 6 0 9 252
Cosmology.FoamTopology 11 0 1 225
Cosmology.GStarDerivation 9 0 18 199
Cosmology.GStarThresholds 9 0 25 227
Cosmology.GalaxyRotation 7 0 9 249
Cosmology.GradedRungCost 10 0 5 221
Cosmology.GrandPotential 14 0 3 342
Cosmology.GravitationalLensingFromRS 3 0 2 50
Cosmology.GravitationalWaveBackground3 4 0 3 36
Cosmology.HeliumAbundance3_FromJCost 4 0 3 36
Cosmology.HorizonProblem 3 0 9 229
Cosmology.HorizonProblem3_FromJCost 4 0 3 36
Cosmology.HubbleConstantPrecise2FromJCost 4 0 3 36
Cosmology.HubbleTension 8 0 9 192
Cosmology.HubbleTensionBound 4 0 6 89
Cosmology.HubbleTensionFromBIT 3 0 2 54
Cosmology.HubbleTensionPipelineFromZAging 6 0 2 82
Cosmology.Inflation 11 0 10 234
Cosmology.InflationModelsFromConfigDim 1 0 1 35
Cosmology.InflationReheatTemperature 0 0 1 30
Cosmology.InflationSpectralIndexFromJCost 5 0 4 67
Cosmology.Inflation_Parameters5 4 0 3 36
Cosmology.InflatonMass3_FromPhiLadder 4 0 3 36
Cosmology.InflatonPotentialStructural 6 0 4 81
Cosmology.InterfaceComponentBound 25 0 11 573
Cosmology.LargeScaleStructureFromRS 3 0 2 50
Cosmology.LatticeBallEdges 18 0 4 613
Cosmology.LatticeBallVolume 5 0 0 281
Cosmology.MatterPert4 4 0 3 36
Cosmology.Matter_Radiation_Equality_RS 4 0 3 36
Cosmology.NeutrinoDilution 7 0 1 199
Cosmology.NeutrinoHierarchyFromPhiLadder 3 0 2 48
Cosmology.NeutrinoMass3_FromPhiLadder 4 0 3 36
Cosmology.NumberDensityIntegral 7 18 0 386
Cosmology.OccupationEnergy 4 0 0 94
Cosmology.OmegaBaryon3_FromJCost 4 0 3 36
Cosmology.OmegaBaryon4 4 0 3 36
Cosmology.OmegaLambdaBITKernelBand 3 0 2 68
Cosmology.OmegaLambdaDerivation 14 0 9 237
Cosmology.OmegaMatter3_FromJCost 4 0 3 36
Cosmology.PTAStochasticGWStructural 5 0 4 156
Cosmology.PartitionKernels 10 0 0 166
Cosmology.PhaseSaturationVacuum 25 5 11 331
Cosmology.PhaseSpaceReduction 10 0 5 282
Cosmology.PhiRungLadder 6 0 2 81
Cosmology.PolarizedBirthDomains 10 0 4 419
Cosmology.PolarizedBirthInterface 6 0 1 219
Cosmology.PolarizedBirthInterfaceCost 12 5 5 367
Cosmology.PolarizedBirthInterfaceCount 10 0 4 453
Cosmology.PrimordialGW3_FromJCost 4 0 3 36
Cosmology.PrimordialSpectrum 4 0 13 244
Cosmology.RS_COS_Structural_001 4 0 3 36
Cosmology.RS_COS_Structural_002 4 0 3 36
Cosmology.RS_COS_Structural_003 4 0 3 36
Cosmology.RS_COS_Structural_004 4 0 3 36
Cosmology.RS_COS_Structural_005 4 0 3 36
Cosmology.RS_COS_Structural_006 4 0 3 36
Cosmology.RS_COS_Structural_007 4 0 3 36
Cosmology.RS_COS_Structural_008 4 0 3 36
Cosmology.RS_COS_Structural_009 4 0 3 36
Cosmology.RS_COS_Structural_010 4 0 3 36
Cosmology.RS_Cosmo_Module_001 4 0 3 36
Cosmology.RS_Cosmo_Module_002 4 0 3 36
Cosmology.RS_Cosmo_Module_003 4 0 3 36
Cosmology.RS_Cosmo_Module_004 4 0 3 36
Cosmology.RS_Cosmo_Module_005 4 0 3 36
Cosmology.RS_Cosmo_Module_006 4 0 3 36
Cosmology.RS_Cosmo_Module_007 4 0 3 36
Cosmology.RS_Cosmo_Module_008 4 0 3 36
Cosmology.RS_Cosmo_Module_009 4 0 3 36
Cosmology.RS_Cosmo_Module_010 4 0 3 36
Cosmology.RS_Cosmo_Module_011 4 0 3 36
Cosmology.RS_Cosmo_Module_012 4 0 3 36
Cosmology.RadiationEntropyRelation 9 16 4 468
Cosmology.RecognitionEquilibrium 14 4 6 260
Cosmology.RecognitionEventHorizon 11 8 4 249
Cosmology.RecognitionUnitStepPreservation 4 4 7 146
Cosmology.RecognitionWorkBound 5 0 2 105
Cosmology.RecombinationRedshift3_FromJCost 4 0 3 36
Cosmology.RefineTrigger 11 0 5 240
Cosmology.RegularNeighborhoodBoundary 86 0 81 1494
Cosmology.ReionizationEndpoint3_FromJCost 4 0 3 36
Cosmology.ReionizationHistoryFromRS 3 0 2 53
Cosmology.Reionization_Redshift_RS 4 0 3 36
Cosmology.RungCoarsen 13 0 11 234
Cosmology.RungDescentUnitStep 7 6 5 231
Cosmology.SIConversion 5 0 16 136
Cosmology.SakharovFromLedger 6 0 4 173
Cosmology.ScaleInvarianceSelectionCert 4 0 1 79
Cosmology.Sigma8Tension3_FromJCost 4 0 3 36
Cosmology.SoundHorizon5 4 0 3 36
Cosmology.Spectral_Index3_FromJCost 4 0 3 36
Cosmology.SphaleronRate 6 0 4 123
Cosmology.StatisticsKernels 20 6 5 387
Cosmology.StructureFormationFromBIT 6 0 2 113
Cosmology.TensorToScalarRatioFromRS 4 0 2 58
Cosmology.ThermodynamicSelectionCert 5 0 1 113
Cosmology.Track4ACert 2 0 1 152
Cosmology.VacuumFluctuationStructural 4 0 3 213
Cosmology.VacuumHorizonForcing 9 0 7 254
Cosmology.VacuumUniformity 5 0 4 72
Cosmology.VoidTopologyFromConfigDim 1 0 1 33
Cosmology.WMassAnomalyStructure 13 0 1 272

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