pith. machine review for the scientific record. sign in

Physics

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

224 modules · 1094 thm/lemma · 20013 lines
module thm lemma def lines papers
Physics.AcousticsFromRS 2 0 2 43
Physics.AerodynamicsFromRS 2 0 1 39
Physics.AlphaHighPrecision 1 0 1 32
Physics.AnchorPolicy 11 0 6 290
Physics.AnchorPolicyCertified 2 0 0 75
Physics.AnchorPolicyModel 4 0 1 66
Physics.AnomalousMagneticMoment 9 0 4 78
Physics.AnomalousMagneticMomentFromRS 2 0 2 46
Physics.AnomalousMoments 1 0 7 47
Physics.AnomalousTransportFromJCost 2 0 2 43
Physics.AstrophysicsStarFormationFromRS 2 0 2 49
Physics.AtmosphericPhysicsFromRS 3 0 1 51
Physics.BAO 12 0 8 148
Physics.BlackBodyRadiationFromJCost 3 0 1 48
Physics.BlackHoleInformationParadoxFromRS 1 0 1 37
Physics.BlackHoleThermodynamicsFromRS 3 0 2 46
Physics.BottomMSBarScoreCard 5 0 6 69
Physics.CKM 1 1 12 91
Physics.CKMElementScoreCard 7 0 0 65
Physics.CKMGeometry 8 0 11 201
Physics.CMBTemperature 12 0 8 157
Physics.CPViolationFromRS 1 0 1 35
Physics.CasimirEffectFromRS 3 0 1 49
Physics.CharmMSBarScoreCard 5 0 6 106
Physics.ClassicalMechanicsDepthFromRS 3 0 2 47
Physics.ClimatePhysicsFromRS 2 0 1 42
Physics.CombustionFromJCost 3 0 1 48
Physics.CondensedMatterPhasesFromConfigDim 1 0 1 36
Physics.CondensedMatterPhasesFromRS 3 0 2 52
Physics.ConservationLawsFromRS 3 0 2 51
Physics.CooperPair 10 0 3 161
Physics.CosmicMicrowaveBackgroundTemperatureFromRS 2 0 3 46
Physics.CosmicRaysFromPhiLadder 2 0 2 47
Physics.CosmologicalConstantFromRS 3 0 2 68
Physics.CosmologicalPerturbationFromRS 1 0 1 38
Physics.CosmologyDepthFromRS 1 0 1 34
Physics.CouplingLockIn 2 0 4 115
Physics.CriticalPhenomenaFromJCost 1 0 1 36
Physics.CrystalSystemsFromConfigDim 3 0 2 49
Physics.CubeSpectrum 12 0 12 126
Physics.DarkMatterAbsoluteCrossSectionScoreCard 3 0 2 67
Physics.DarkMatterCrossSectionBandScoreCard 3 0 1 61
Physics.DarkMatterHaloProfileFromRS 3 0 2 55
Physics.DarkMatterMassFromGap45 3 0 5 50
Physics.DarkMatterWeakReferenceCrossSectionScoreCard 3 0 4 94
Physics.DecaySpectrumFromPhiLadder 3 0 2 49
Physics.DimensionalAnalysisFromConfigDim 2 0 1 41
Physics.DiracEquationFromRS 5 0 3 48
Physics.EarthBrainResonance 31 2 5 378
Physics.EightTickPeriodicityFromD 8 0 6 61
Physics.ElectrochemistryFromRS 2 0 1 39
Physics.ElectromagneticSpectrumFromPhiLadder 3 0 3 59
Physics.ElectronGMinus2ScoreCard 9 0 2 141
Physics.ElectronMass 3 0 0 79
Physics.ElectronMass.BaselineDerivation 4 0 1 54
Physics.ElectronMass.Defs 10 0 17 245
Physics.ElectronMass.Necessity 9 22 14 562
Physics.ElectroweakBosons 16 0 20 252
Physics.ElectrowealUnificationFromRS 3 0 4 49
Physics.EntanglementEntropyFromRS 4 0 2 58
Physics.EntropyArrowFromJCost 4 0 1 55
Physics.FeynmanDiagramsFromRS 3 0 3 49
Physics.FineStructureConstantFromRS 4 0 3 48
Physics.GammaRayBursts 9 0 6 72
Physics.GaugeBosonMassesFromRS 4 0 3 62
Physics.GeneralRelativityFromRS 3 0 2 53
Physics.GeophysicsFromRS 2 0 1 43
Physics.GluonSelfInteractionFromRS 4 0 1 52
Physics.GrandUnificationFromRS 4 0 3 49
Physics.GravitationalConstantPrecision 1 0 1 30
Physics.GravitationalWaveEchoFromRS 3 0 3 56
Physics.GravitationalWaveInterferometryFromJCost 1 0 1 36
Physics.GravitationalWaveSourcesFromConfigDim 1 0 1 35
Physics.Hadrons 3 0 5 83
Physics.HawkingRadiationFromRS 3 0 2 56
Physics.Hierarchy 1 0 2 60
Physics.HiggsBosonFromJCost 3 0 1 46
Physics.HiggsFieldFromRecognitionVacuum 4 0 1 53
Physics.HiggsMassScoreCard 4 0 1 54
Physics.HiggsVEVFromJCost 2 0 2 43
Physics.HolographicPrincipleFromRS 2 0 2 44
Physics.HydrodynamicsFromRS 3 0 1 48
Physics.InflationEfoldsFromGap45 4 0 4 50
Physics.InflationaryCosmologyFromRS 1 0 2 42
Physics.Ising2D 9 1 8 128
Physics.IsospinSymmetryFromRS 3 0 3 47
Physics.KaonMasses 9 0 18 185
Physics.LeptonGenerations 4 0 0 110
Physics.LeptonGenerations.Defs 0 0 8 69
Physics.LeptonGenerations.FractionalStepDerivation 9 0 6 231
Physics.LeptonGenerations.Necessity 41 47 21 1275
Physics.LeptonGenerations.TauStepDeltaDerivation 22 0 11 421
Physics.LeptonGenerations.TauStepDerivation 3 0 5 108
Physics.LeptonGenerations.TauStepExclusivity 15 0 6 251
Physics.LightConeCausalityFromRS 1 0 1 33
Physics.LoopQuantumGravityFromRS 2 0 1 42
Physics.LorentzSymmetryFromRecognition 4 0 1 57
Physics.LorentzViolationBoundFromRS 2 0 2 41
Physics.MagneticMonopoleFromPhiLattice 2 0 3 40
Physics.MagnetismFromRS 3 0 1 48
Physics.MassHierarchy 8 0 8 240
Physics.MassResidueNoGo 4 0 0 76
Physics.MassTopology 0 0 9 77
Physics.MaterialsScienceFromRS 2 0 2 41
Physics.MatterAntimatterAsymmetryFromRS 1 0 1 36
Physics.MatterWaveFromRS 2 0 2 47
Physics.MaxwellEquationsFromRS 3 0 3 47
Physics.MeasurementTheoryFromRS 1 0 1 35
Physics.MesonSpectrumFromPhiLadder 3 0 2 50
Physics.MixingDerivation 17 0 7 359
Physics.MixingGeometry 4 0 13 100
Physics.MolecularPhysicsFromRS 3 0 3 53
Physics.Muon_g-2_FromJCost 4 0 3 36
Physics.NanoScienceFromRS 2 0 1 44
Physics.NeutrinoMassExactness 0 0 1 31
Physics.NeutrinoMassFromPhiLadder 2 0 2 50
Physics.NeutrinoMassScaleScoreCard 7 0 0 88
Physics.NeutrinoSector 6 21 24 759
Physics.NeutronStarCrustalRegimesFromRS 3 0 2 49
Physics.NeutronStarTOV 8 0 6 136
Physics.NoHairTheorem 11 0 5 178
Physics.NonlinearDynamicsFromRS 3 0 2 48
Physics.NuclearMagicNumbersFromRS 5 0 2 51
Physics.NuclearPhysicsDepthFromRS 2 0 3 46
Physics.OceanographyFromRS 1 0 1 35
Physics.OpticalTrapRegimesFromJCost 1 0 1 33
Physics.OpticsSnellsLawFromRS 4 0 1 52
Physics.PMNS.Construction 0 0 1 17
Physics.PMNS.Types 0 0 1 29
Physics.PMNSCorrections 14 0 9 191
Physics.PMNSMixingAnglesFromRS 3 0 2 63
Physics.PMNSScoreCard 7 0 0 76
Physics.ParticlePhysicsDepthFromRS 3 0 3 45
Physics.ParticlePhysicsGenerationsFromRS 5 0 5 51
Physics.ParticleSummary 0 0 1 44
Physics.PathIntegralFromRS 3 0 1 47
Physics.PhiVsUniformPulseSpacingCert 5 0 3 87
Physics.PhotoelectricEffectFromJCost 3 0 1 47
Physics.PhotonStatisticsFromRS 2 0 1 43
Physics.PhotonicsMetamaterialFromPhi 2 0 2 45
Physics.PionMasses 8 0 21 203
Physics.PlanckConstantFromRS 4 0 5 71
Physics.PlanetStrataC2 2 0 5 92
Physics.PlasmonicModesFromPhiLadder 3 0 2 51
Physics.ProtonRadius 9 0 3 75
Physics.QCDRGE.AlphaRunning 7 0 6 82
Physics.QCDRGE.MassAnomalousDimension 9 0 5 138
Physics.QCDRGE.PoleToMSbar 5 0 6 112
Physics.QCDRGE.ThresholdMatching 5 0 5 132
Physics.QCDRGE.TwoLoopAlphaS 7 0 5 140
Physics.QuantumChromodynamicsFromRS 5 0 3 52
Physics.QuantumCoherenceTimeFromJCost 4 0 2 72
Physics.QuantumComputingDepthFromRS 3 0 3 46
Physics.QuantumComputingGatesFromRS 2 0 2 43
Physics.QuantumDecoherenceFromJCost 2 0 2 53
Physics.QuantumEntanglementEntropyAreaLaw 1 0 1 37
Physics.QuantumErrorCorrectionFromJCost 4 0 2 57
Physics.QuantumFieldOperatorsFromRS 2 0 2 44
Physics.QuantumFieldTheoryDepthFromRS 2 0 2 43
Physics.QuantumGravityFromRS 4 0 3 67
Physics.QuantumHallEffect 15 0 5 177
Physics.QuantumMolecularDesignDepthC4 3 0 2 57
Physics.QuantumOpticsFromRS 3 0 1 48
Physics.QuantumTeleportationFromRS 2 0 1 38
Physics.QuantumTunnelingFromJCost 1 0 1 38
Physics.QuarkCoordinateReconciliation 8 0 11 260
Physics.QuarkMassHierarchyFromPhiLadder 4 0 2 55
Physics.QuarkMasses 2 0 16 118
Physics.RGTransport 12 0 16 339
Physics.RGTransportCertificate 4 0 5 85
Physics.RadioactiveDecayTypesFromConfigDim 1 0 1 32
Physics.RecognitionCompositionLawCert 4 0 1 56
Physics.RecognitionCoupling 2 0 6 114
Physics.RecognitionHamiltonianSpectrum 4 0 2 65
Physics.RelativisticQuantumFieldTheoryFromRS 2 0 1 43
Physics.RoboticsFromRS 2 0 2 40
Physics.RunningCouplings 18 0 13 326
Physics.SchroedingerEquationFromRS 3 0 1 50
Physics.SchwarzchildRadiusFromRS 2 0 3 51
Physics.SectorYardsticks 1 0 4 90
Physics.SemiconductorBandStructureFromConfigDim 3 0 2 50
Physics.SemiconductorPhysicsFromRS 3 0 3 49
Physics.SineSqThetaWFromPhiLadder 2 0 3 64
Physics.SolidStatePhysicsFromRS 2 0 3 44
Physics.SolitonClassesFromRS 1 0 1 35
Physics.SpecialRelativityFromRS 4 0 1 54
Physics.SpinFoamFromRS 3 0 2 45
Physics.StandardModelGroupStructure 5 0 7 61
Physics.StandardModelLagrangianStructure 5 0 3 51
Physics.StatisticalMechanicsFromRS 3 0 1 47
Physics.StellarEvolution 11 0 9 173
Physics.SterileExclusion 1 2 3 87
Physics.StringCompactificationFromRS 3 0 1 46
Physics.StringTheoryFromJCost 2 0 1 41
Physics.StrongForce 5 0 5 104
Physics.StrongNuclearForceFromRS 4 0 3 57
Physics.SuperconductingCircuitsFromRS 3 0 2 41
Physics.SuperconductingQubitFromJCost 2 0 2 48
Physics.Superfluidity 11 1 7 155
Physics.SupernovaClassificationFromRS 1 0 1 34
Physics.SuperstringTheoryFromRS 3 0 4 48
Physics.SurfaceScienceFromRS 1 0 1 35
Physics.SymmetryBreakingFromRS 3 0 1 48
Physics.TachyonFreeTachyonFromRS 3 0 1 50
Physics.TauZeroCalibratorFromConstants 3 0 3 62
Physics.ThermalFixedPoint 16 0 6 194
Physics.ThermalPhysicsFromRS 2 0 1 39
Physics.ThermochemistryFromRS 3 0 1 46
Physics.ThermodynamicLawsFromRS 5 0 1 59
Physics.ThermoelectricEffectFromJCost 1 0 1 41
Physics.ThreeGenerations 8 0 9 218
Physics.TopMSBarScoreCard 5 0 6 79
Physics.TopologicalChargesFromConfigDim 1 0 1 34
Physics.TopologicalDefectsFromRS 2 0 1 39
Physics.TopologicalPhaseTransitionFromJCost 1 0 1 40
Physics.UniversalityClasses 7 0 8 109
Physics.VacuumDecayFromJCost 3 0 2 51
Physics.WEndoForcing 11 0 1 98
Physics.WZBosonRatioScoreCard 3 0 0 44
Physics.WaveFunctionCollapseFromJCost 3 0 1 49
Physics.WeakForceEmergence 10 0 18 243
Physics.WeakNuclearForceFromRS 3 0 1 52
Physics.WeinbergAngleScoreCard 4 0 1 59
Physics.YangMillsLatticeFromRS 4 0 1 62

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