Revision #1866 → #2380 · back to history
modifiedKepler's first law (lead)d11c0d0e46f3
| Field | From #1866 | To #2380 |
|---|
| note | Mathlib has no formalization of Kepler orbits or ellipse-shaped planetary trajectories. | Mathlib has no Kepler-orbit or ellipse-shaped trajectory formalization (no hits for Kepler/ellipse). |
modifiedKepler's second law (lead)609ca4c98bd1
| Field | From #1866 | To #2380 |
|---|
| note | Mathlib has no formalization of the equal-areas / areal-velocity law. | No equal-areas / areal-velocity law: no angular-momentum or central-force machinery in Mathlib. |
modifiedKepler's third law (lead)4d7c22fc24b9
| Field | From #1866 | To #2380 |
|---|
| note | Mathlib has no formalization of the period-semimajor axis relation. | T²∝a³ is not in Mathlib (no Kepler hits at all). |
modifiedEccentricity of Earth's orbit from equinox times40453952d069
| Field | From #1866 | To #2380 |
|---|
| note | No astronomical computations exist in Mathlib. | No astronomical / orbital-mechanics computations in Mathlib. |
modifiedKepler's first law9fd1ad12017b
| Field | From #1866 | To #2380 |
|---|
| note | Mathlib does not define ellipses as conics or formalize Kepler's first law. | Mathlib lacks both ellipses-as-conics and Kepler's first law. |
modifiedEllipse in polar form7fcef9838324
| Field | From #1866 | To #2380 |
|---|
| note | No definition of an ellipse (polar or otherwise) exists in Mathlib; only elliptic curves in algebraic geometry. | No definition of an ellipse exists in Mathlib (only convex 'cones' and elliptic curves, neither relevant). |
modifiedSemi-major axis as arithmetic meana9eab7073c52
| Field | From #1866 | To #2380 |
|---|
| note | Arithmetic mean exists but no ellipse semi-major axis identity to instantiate it. | Arithmetic mean exists but no ellipse semi-major axis to relate to it. |
modifiedSemi-latus rectum as harmonic mean62460cbbe676
| Field | From #1866 | To #2380 |
|---|
| note | Harmonic mean infrastructure absent and no ellipse parameter to relate. | No ellipse semi-latus rectum in Mathlib to express via harmonic mean. |
modifiedEccentricity as coefficient of variation2f3bf1a4b644
| Field | From #1866 | To #2380 |
|---|
| note | No ellipse eccentricity defined; the only 'eccentricity' is graph-theoretic. | No ellipse eccentricity defined; the only 'eccentricity' in Mathlib is graph-theoretic. |
modifiedArea of the ellipseda73af8d37cc
| Field | From #1866 | To #2380 |
|---|
| note | Mathlib has no ellipse and no πab area formula. | Mathlib has no ellipse object and no πab area formula. |
modifiedSolutions to the inverse square law include conic orbitsa1bfce007460
| Field | From #1866 | To #2380 |
|---|
| note | Conic-section solutions of central-force ODE absent from Mathlib. | Conic-section solutions of the central-force ODE absent from Mathlib. |
modifiedKepler's equation0d85fd02cd14
| Field | From #1866 | To #2380 |
|---|
| note | M = E − ε sin E is not formalized in Mathlib. | M = E − ε sin E is not formalized in Mathlib (no Kepler hits). |