Arguments
A derivation is written to be checked. An argument is the same derivation written to be read: the model first, then what is given, then the steps as a numbered outline with sub-arguments and cases indented, the conclusion, and what the checks say. The format is astra-argument/1; one document, four renderings.
famulus-astra argument solar-equivalence-equal-radii --format html # a standalone page
famulus-astra argument kepler-equant-unequal-motion --format md # Markdown outline
famulus-astra argument euler-tide-force-resolution --format typst # the printed outline of the papers
famulus-astra argument <derivation> # the JSON documentThe pane
Overview · Steps · Full set the depth for the whole argument: the top-level sub-arguments and the conclusion; every step with claim, notation, premises and rule; and, at Full, the formal proposition, the binding of the rule’s variables, what the rule takes from the figure, degenerate states, and the wording of the proposition with its place in Heath. Every block opens and closes on its own. Selecting a step shows in the figure what it speaks of. A premise chip jumps to the step it names.
| mark | the step is |
|---|---|
| ✓ | an instance of the rule it names, or an equality by Common Notion 1 |
| ◦ | read off the construction: it holds without any hypothesis |
| ≈ | a calculation, or an expansion to a stated order |
| ? | true, but not licensed by its rule: a gap |
| ✗ | false |
| · | a supposition |
Three reconstructions
| argument | source | pane |
|---|---|---|
| The two forms of Ptolemy’s solar model place the sun at one point | Swerdlow 2026, p. 19 and Fig. 1.2 | open |
| About the centre of its circle the planet moves unequally | Kepler, Astronomia nova, ch. 4 (KGW 3, p. 73) | open |
| The tide-raising force to first order | Euler, E57, §§24–29 (Opera omnia II 31, pp. 35–39) | open |
| The same in direction, under proportional radii | Swerdlow 2026, p. 20 and Fig. 1.3 | open |
| The equation of centre | Swerdlow 2026, p. 21 and Fig. 1.4 | open |
Kepler: the equant
The hypothesis H1 (BC = BA) is stated by Kepler and needed by no step. The two inequalities hold in every position; the supposition of the right angle is needed only for the comparison of the two arcs.
# Kepler, Astronomia nova, Part I, ch. 4 (KGW 3, p. 73; kepler-prim/kgw-03, pidx 71, paragraph 4): the argument
# by which the equant model is charged with making the motion of the orb unequal.
# "Eligatur enim E punctum in circulo, quem Planeta corpore peragrat, connectaturque cum CBA : et sit jam DCE
# rectus, ut et ECF. Cum ergo sint anguli hi aequales, constituti nempe aequalibus temporibus, et DCE exterior
# aequet CBE, CEB interiores : ergo parte CEB ablata, residuus CBE vel DBE minor erit quam DCE. itaque FBE
# major quam DCE vel FCE. Sed DE arcus metitur DBE angulum, et EF arcus angulum EBF. minor ergo DE quam EF. et
# transit Planeta per eos aequalibus temporibus."
# Kepler cites no proposition of Euclid. The propositions that license his steps are supplied here.
derivation kepler-equant-unequal-motion in kepler-equant "About the centre of its circle the planet moves unequally: the arc DE is less than the arc EF, and both are passed in equal times"
witness fr:kepler-prim/kgw-03/0071/p05 "Astronomia nova ch. 4"
witness fr:kepler-sec/Kepler1992/0147/p02 "Donahue's translation"
author "Gerd Graßhoff"
given h1: equal(q, e) "the equant point lies as far above the centre as the eye lies below it: BC = BA"
show lag: less(angle(D, B, E), angle(D, C, E)) "the angle DBE at the centre is less than the angle DCE at the equant point"
derive k1: equal(angle(E, C, D), angle(C, E, B) + angle(E, B, C)) by Elements I.32 "DCE is the exterior angle of the triangle CBE, equal to the interior angles CBE and CEB"
derive k2: less(angle(E, B, C), angle(E, C, D)) from k1 by common notion 5 "the part CEB taken away, the remainder CBE is less than DCE"
derive k3: equal(angle(E, B, C), angle(D, B, E)) from def C, def D, def E by construction "CBE or DBE: C and D lie from B on one ray"
derive k4: less(angle(D, B, E), angle(D, C, E)) from k2, k3 by common notion 1
qed from k4
derive k5: equal(angle(D, B, E) + angle(E, B, F), 180°) by Elements I.13 "BE stands on the apsidal line at B: DBE and EBF make two right angles"
derive k6: equal(angle(D, C, E) + angle(E, C, F), 180°) by Elements I.13 "CE stands on the apsidal line at C: DCE and ECF make two right angles"
show lead: less(angle(E, C, F), angle(E, B, F)) "so the angle FBE is greater than the angle FCE"
derive k7: less(angle(E, C, F), angle(E, B, F)) from lag, k5, k6 by algebra
qed from k7
suppose quadrant: right_angle(D, C, E) "let DCE be a right angle, and so ECF: two quarters of the period"
show unequal: less(angle(D, B, E), angle(E, B, F)) "the arc DE, which measures the angle DBE, is less than the arc EF, which measures the angle EBF"
derive k8: equal(angle(D, C, E), angle(E, C, F)) from quadrant, k6 by algebra "the angles at C are equal: they are made in equal times"
derive k9: less(angle(D, B, E), angle(E, B, F)) from lag, lead, k8 by algebra "DBE < DCE = ECF < EBF"
qed from k9
conclude less(angle(D, B, E), angle(E, B, F)) from unequal "in equal times the planet passes the lesser arc DE and the greater arc EF: the orb is now slow, now fast"Euler: the tide-raising force
Steps 4 to 7 are approximations with a stated order. In step 5 the Opera omnia print an emended sign (4xx + yy for 4xx − yy). The emended formula, stated to second order, fails:
euler-tide-force-emendation: derivation in euler-tide-force, level grounded (2/5)
✓ well-formed
✓ grounded
✗ true
conclusion: approximately(tMR, 3 * Sf * x * y / (a * a * a * rho) + 3 * Sf * y * (4 * x * x + y * y) / (2 * a * a * a * a * rho)) fails (not of order 2: relative difference 2.0e-02 at ratio 0.01, 2.0e-03 at ratio 0.001, 2.0e-04 at ratio 0.0001)
· justified (not reached)
✗ conclusive
the conclusion does not hold
✓ exact: equal(tMR, Sf * a * y / (dist * dist * dist * rho) - Sf * y / (a * a * rho)) from def tMR, def fM, def fC, def dist, def x, def y, def M, def S by construction — read off the construction
✗ conclusion: approximately(tMR, 3 * Sf * x * y / (a * a * a * rho) + 3 * Sf * y * (4 * x * x + y * y) / (2 * a * a * a * a * rho)) from exact by expansion — false (not of order 2: relative difference 2.0e-02 at ratio 0.01, 2.0e-03 at ratio 0.001, 2.0e-04 at ratio 0.0001)In a viewer
The element is one script and one stylesheet (web/astra-argument/astra-argument.bundle.js, astra-argument.css):
<astra-argument src="argument.json" depth="steps"></astra-argument>or with the document inline, <script type="application/json" id="…-data">, as the HTML versions of the papers do. web/astra-argument/viewer/famulus-begruendung.js registers the element as a panel for ai-viewer (FamulusPanels.anmelden). It is delivered with the package and is not installed in the production viewer.
