Pith. sign in

Relativity

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

41 modules · 220 thm/lemma · 5247 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.Compact.BlackHoleEntropy 7 0 2 83 -
Relativity.Cosmology.FRWComponentsProbe 0 3 3 87 -
Relativity.Cosmology.FRWFriedmann 17 8 8 370 -
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.Parameters 9 0 2 238 -
Relativity.GRLimit.ParametersTest 0 0 0 48 -
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.LocalAreaRaychaudhuri 2 0 0 96 -
Relativity.Geometry.LocalEquilibriumAreaVariation 11 0 2 194 -
Relativity.Geometry.LocalRaychaudhuriReduction 7 0 1 172 -
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.CosmologyDerived 0 0 0 24 -
Relativity.ILG.FRW 0 0 1 20 -
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.InformationConservation 4 0 1 75 -

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