astra/1

A model has no values

model solar-eccentric "Ptolemy's solar model, eccentric form"
attributed "Ptolemy"
witness fr:kepler-sec/Swerdlow2026/0049/p04 "the construction, p. 19"
witness fr:kepler-sec/Swerdlow2026/0050/p03 "longitudes, anomalies and the
      equation, p. 20"
witness fr:kepler-sec/Swerdlow2026/0051/fig02 "Fig. 1.4"
author "Gerd Graßhoff"
tradition ptolemaic
frame geocentric
param R  : length "radius of the eccentric"  in (1, 1000)
param e  : length "eccentricity, the distance OE"  in (0, R / 2)
param lamA  : angle  "longitude of the apogee"
param T  : time  "tropical year"  in (300, 400)
param kappa_0 : angle  "mean anomaly at t = 0"
display lamA "λ_A"
display kappa_0 "κ̄_0"
variable kappa_bar : angle "mean anomaly about E, counted from the apogee"
law kappa_bar = uniform(period: T, epoch: kappa_0) "the sun moves uniformly
      about E"
display kappa_bar "κ̄"
O  = observer  "earth"
E  = O + polar(e, lamA)  "centre of the eccentric"
ecc = circle(E, R)  "the eccentric"
A  = E + polar(R, lamA)  "apogee"
B  = E - polar(R, lamA)  "perigee"
S  = E + polar(R, lamA + kappa_bar)  "sun"
body sun at S
observe lam_bar = direction(E, S)  "mean longitude"
observe lam  = direction(O, S)  "true longitude"
observe kappa  = lam - lamA  "true anomaly about O"
observe c  = lam_bar - lam  "equation of centre, mean minus true longitude"
display lam_bar "λ̄_S"
display lam "λ_S"
display kappa "κ"
proposition p1: equal(lam_bar, lamA + kappa_bar) "the mean longitude is the
      longitude of the apogee plus the mean anomaly"
proposition p2: equal(kappa, kappa_bar - c)  "the true anomaly is the mean
      anomaly less the equation"
proposition p5: equal(lam, lam_bar - c)  "the true longitude is the mean
      longitude less the equation"
proposition p3: collinear(A, E, B)  "the apsidal line passes through E"
proposition p4: collinear(A, O, B)  "and through O"

The equivalence as an argument

When something is wrong

# the wrong proposition is cited
✗ d6: parallel(line(O, Ecc.E), line(Epi.C, Ecc.S)) from sides, d5 by Elements
      I.29
      — true, not justified (the proposition is not a conclusion of the rule)
      level reached: true

# a hypothesis of the proposition is not cited
✗ d6: parallel(line(O, Ecc.E), line(Epi.C, Ecc.S)) from sides by Elements I.33
      — true, not justified (a hypothesis of the rule is not among the cited
            premises)

# a false proposition
✗ d12: coincident(Ecc.S, Epi.C) from joins, d11, d10 by lemma same ray
      — false (residual 0.462 of the scale at kappa_bar = 10° for Ecc.R = 224.2,
            Ecc.e = 103.5, lamA = 80.62, T = 372.7, kappa_0 = 33.21, Epi.R' =
            224.2, Epi.r = 103.5)
      level reached: grounded

# a hypothesis is used without being cited
✗ conclusive: d10 holds only under h2, which is not cited on the way to it (a
      tacit premise)

# a proposition that needs a hypothesis is passed off as read off the
      construction
✗ d5: equal(distance(Ecc.E, Ecc.S), distance(O, Epi.C)) from def Ecc.S, def
      Epi.C by construction
      — true, not justified (it does not hold without the hypotheses (residual
            0.899 of the scale at kappa_bar = 15° for Ecc.R = 59.08, Ecc.e =
            21.37, lamA = 192, T = 393.8, kappa_0 = 119.4, Epi.R' = 585.3, Epi.r
            = 266.6), so it is not read off the constructions alone)

# a case is left out: the perigee
✗ justified: same: coincident(Ecc.S, Epi.S') by cases: no case covers kappa_bar
      = 180°
      level reached: true