pith. machine review for the scientific record. sign in

Relativity

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

57 modules · 209 thm/lemma · 6439 lines
module thm lemma def lines papers
Relativity.Analysis 0 0 0 12
Relativity.Analysis.Landau 4 0 0 95
Relativity.Analysis.Limits 8 1 4 177
Relativity.Calculus 0 0 0 6
Relativity.Calculus.Derivatives 22 21 8 839
Relativity.Calculus.FunctionalEquationDeriv 1 0 0 77
Relativity.Calculus.RadialDerivativesProofs 8 0 1 494
Relativity.Compact 0 0 0 12
Relativity.Compact.BlackHoleEntropy 7 0 2 83
Relativity.Compact.StaticSpherical 1 0 2 154
Relativity.Cosmology.Buchert 2 0 2 52
Relativity.Cosmology.FRWMetric 0 0 4 71
Relativity.Cosmology.OpticalExtension 2 0 4 70
Relativity.Dynamics.RecognitionSheaf 6 0 1 98
Relativity.Fields 0 0 0 9
Relativity.Fields.Integration 4 0 6 107
Relativity.Fields.Scalar 9 0 9 101
Relativity.GRLimit 0 0 0 14
Relativity.GRLimit.Observables 0 0 1 162
Relativity.GRLimit.Parameters 9 0 2 238
Relativity.GRLimit.ParametersTest 0 0 0 48
Relativity.GW 0 0 0 16
Relativity.GW.ActionExpansion 0 0 6 38
Relativity.GW.Constraints 1 0 3 28
Relativity.GW.PropagationSpeed 4 0 2 60
Relativity.GW.TensorDecomposition 1 0 3 42
Relativity.Geodesics.NullGeodesic 4 0 2 138
Relativity.Geometry 0 0 0 16
Relativity.Geometry.Connection 2 1 5 68
Relativity.Geometry.CovariantDerivative 0 0 1 25
Relativity.Geometry.Curvature 7 1 5 164
Relativity.Geometry.DiscreteBridge 6 0 3 215
Relativity.Geometry.LeviCivitaTheorem 7 0 6 219
Relativity.Geometry.Manifold 3 0 9 89
Relativity.Geometry.MatrixBridge 0 1 2 38
Relativity.Geometry.Metric 0 4 6 125
Relativity.Geometry.MetricUnification 12 0 2 176
Relativity.Geometry.ParallelTransport 4 0 5 254
Relativity.Geometry.RiemannSymmetries 20 0 7 592
Relativity.Geometry.Tensor 0 0 6 45
Relativity.ILG.Action 4 0 23 157
Relativity.ILG.ClusterLensing 2 0 5 132
Relativity.ILG.CosmologyDerived 0 0 0 24
Relativity.ILG.FRW 0 0 1 20
Relativity.ILG.Falsifiers 1 0 2 31
Relativity.ILG.GWDerived 0 0 0 23
Relativity.ILG.LensingDerived 0 0 0 25
Relativity.ILG.PPN 4 0 8 69
Relativity.ILG.PPNDerive 1 0 3 39
Relativity.ILG.PPNDerived 0 0 0 24
Relativity.ILG.Params 0 0 0 19
Relativity.ILG.Substrate 1 0 1 57
Relativity.InformationConservation 4 0 1 75
Relativity.Lensing.ShadowPredictions 7 0 4 136
Relativity.NewFixtures 0 0 15 175
Relativity.Perturbation.BackgroundFixtures 0 0 0 10
Relativity.PostNewtonian.Metric1PN 2 0 8 156

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