pith. machine review for the scientific record. sign in

Action

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

8 modules · 39 thm/lemma · 1287 lines
module thm lemma def lines papers
Action.EnergyConservationDomainCert 2 0 1 86
Action.EulerLagrange 6 1 5 211
Action.FunctionalConvexity 6 1 1 318
Action.Hamiltonian 2 0 6 169
Action.NewtonSecondLawDomainCert 1 0 1 68
Action.Noether 3 0 7 130
Action.PathSpace 0 12 5 166
Action.QuadraticLimit 5 0 4 139

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