Checking

famulus-astra check says what can be said of each kind of text. Levels presuppose one another; the report names the level reached, every failed check with its reason and every gap. Nothing passes by default.

$ famulus-astra check

text	kind	check
fr:astra/euler-fig-3	figure	✓ labelled
fr:astra/euler-tide-force	model	✓ documented
fr:astra/euler-tide-force-emendation	derivation	✗ grounded
fr:astra/euler-tide-force-resolution	derivation	✓ conclusive
fr:astra/kepler-equant	model	✓ documented
fr:astra/kepler-equant-unequal-motion	derivation	✓ conclusive
fr:astra/kepler-fig-ch2-eccentric	figure	✓ labelled
fr:astra/kepler-fig-ch2-epicycle	figure	✓ labelled
fr:astra/kepler-fig-ch4	figure	✓ labelled
fr:astra/solar-eccentric	model	✓ documented
fr:astra/solar-eccentric-epicyclic	superposition	✓ consistent
fr:astra/solar-eccentric-epicyclic.equal-radii	parametrisation	✓ attested
fr:astra/solar-eccentric-epicyclic.proportional	parametrisation	✓ attested
fr:astra/solar-eccentric.battani	parametrisation	✗ well-formed
fr:astra/solar-eccentric.ptolemy	parametrisation	✓ attested
fr:astra/solar-epicyclic	model	✓ documented
fr:astra/solar-equation-of-centre	derivation	✓ conclusive
fr:astra/solar-equivalence-equal-radii	derivation	✓ conclusive
fr:astra/solar-equivalence-proportional	derivation	✓ conclusive
fr:astra/solar-fig-1-2	figure	✓ labelled
fr:astra/solar-fig-1-3	figure	✓ labelled
fr:astra/solar-fig-1-4	figure	✓ labelled
fr:astra/solar-fig-eccentric	figure	✓ labelled
fr:astra/solar-fig-epicyclic	figure	✓ labelled
fr:astra/solar-fig-equal-radii-steps	figure	✓ labelled
fr:astra/solar-fig-equation	figure	✓ labelled
fr:astra/solar-parameters-from-seasons	derivation	✓ conclusive

Model

level	what is checked
well-formed	the text parses; names are unique and defined before use; types match; no value, no source, no statement of another kind
constructible	every object has a solution in every sampled configuration of the parameter space and the states
astronomical	one observer; a body; an observable direction from the observer to the body; a declared frame
kinematic	a kinematic variable that reaches a body through the construction
consistent	the stated propositions hold in every sampled configuration
documented	attributed, witness, author; a meaning for every symbol and object

solar-eccentric: model, level documented (6/6)
  ✓ well-formed
  ✓ constructible
  ✓ astronomical
  ✓ kinematic
  ✓ consistent
  ✓ documented
  ✓ p1: equal(lam_bar, lamA + kappa_bar)  max residual 5.7e-14 over 3456 configurations
  ✓ p2: equal(kappa, kappa_bar - c)  max residual 1.1e-13 over 3456 configurations
  ✓ p5: equal(lam, lam_bar - c)  max residual 5.7e-14 over 3456 configurations
  ✓ p3: collinear(A, E, B)  max residual 1.5e-16 over 3456 configurations
  ✓ p4: collinear(A, O, B)  max residual 1.3e-16 over 3456 configurations

Parametrisation

level	what is checked
complete	every parameter of the model has a value
admissible	every value lies in its range
attested	every value has a source fr:… or a gap "…"; whose values they are and who wrote the text is said

solar-eccentric.battani: parametrisation, level well-formed (1/4)
  ✓ well-formed
  ✗ complete
      T (tropical year) has no value
      kappa_0 (mean anomaly at t = 0) has no value
  · admissible (not reached)
  · attested (not reached)
  gap: R = 60: the norm R = 60 is not repeated in the paragraph; e is given in its units

Superposition, figure

A superposition is checked as a model, with superposed in place of the astronomical levels: the members’ observers are identified. A figure is drawable when its values and state give every drawn object a place, and labelled when every drawn object has a meaning or a symbol.

Derivation

grounded · true · justified · conclusive — see Derivations.

solar-equivalence-equal-radii: derivation in solar-eccentric-epicyclic, level conclusive (5/5)
  ✓ well-formed
  ✓ grounded
  ✓ true
  ✓ justified
  ✓ conclusive
  given     h1: equal(Epi.R', Ecc.R)
  given     h2: equal(Epi.r, Ecc.e)
  ✓ same: coincident(Ecc.S, Epi.S') by cases — justified by cases
    ✓ d3: equal(distance(Ecc.E, Ecc.S), Ecc.R) from def Ecc.S by construction — read off the construction
    ✓ d4: equal(distance(O, Epi.C), Epi.R') from def Epi.C by construction — read off the construction
    ✓ d8: equal(distance(O, Ecc.E), Ecc.e) from def Ecc.E by construction — read off the construction
    ✓ d9: equal(distance(Epi.C, Epi.S'), Epi.r) from def Epi.S' by construction — read off the construction
    ✓ generic: coincident(Ecc.S, Epi.S') from d12 — justified (it is d12)
      ✓ sides: parallel(line(Ecc.E, Ecc.S), line(O, Epi.C)) from d2 — justified (it is d2)
        ✓ d1: equal(angle(Ecc.A, Ecc.E, Ecc.S), angle(Epi.A', O, Epi.C)) from def Ecc.A, def Ecc.S, def Epi.A', def Epi.C by construction — read off the construction
        ✓ d2: parallel(line(Ecc.E, Ecc.S), line(O, Epi.C)) from d1 by Elements I.28 — justified
      ✓ d5: equal(distance(Ecc.E, Ecc.S), distance(O, Epi.C)) from d3, d4, h1 by common notion 1 — justified
      ✓ joins: parallel(line(O, Ecc.E), line(Epi.C, Ecc.S)) from d6 — justified (it is d6)
        ✓ d6: parallel(line(O, Ecc.E), line(Epi.C, Ecc.S)) from sides, d5 by Elements I.33 — justified
      ✓ d7: equal(distance(O, Ecc.E), distance(Epi.C, Ecc.S)) from sides, d5 by Elements I.33 — justified
      ✓ d10: equal(distance(Epi.C, Ecc.S), distance(Epi.C, Epi.S')) from d7, d8, h2, d9 by common notion 1 — justified
      ✓ d11: parallel(line(Epi.C, Epi.S'), line(O, Ecc.E)) from def Epi.S', def Ecc.E by construction — read off the construction
      ✓ d12: coincident(Ecc.S, Epi.S') from joins, d11, d10 by lemma same ray — justified
    ✓ apogee: coincident(Ecc.S, Epi.S') from a7 — justified (it is a7)
      ✓ a1: equal(distance(O, Ecc.S), distance(O, Ecc.E) + distance(Ecc.E, Ecc.S)) by lemma segment addition — justified
      ✓ a2: equal(distance(O, Epi.S'), distance(O, Epi.C) + distance(Epi.C, Epi.S')) by lemma segment addition — justified
      ✓ a3: equal(distance(O, Ecc.S), distance(O, Epi.S')) from a1, a2, d3, d4, d8, d9, h1, h2 by algebra — by calculation
      ✓ a4: parallel(line(O, Ecc.S), line(O, Ecc.E)) from apogee by lemma one line — justified
      ✓ a5: collinear(O, Ecc.E, Epi.S') from def Epi.C, def Epi.S', def Ecc.E by construction — read off the construction
      ✓ a6: parallel(line(O, Epi.S'), line(O, Ecc.E)) from a5 by lemma one line — justified
      ✓ a7: coincident(Ecc.S, Epi.S') from a4, a6, a3 by lemma same ray — justified
    ✓ perigee: coincident(Ecc.S, Epi.S') from p7 — justified (it is p7)
      ✓ p1: equal(distance(Ecc.E, Ecc.S), distance(Ecc.E, O) + distance(O, Ecc.S)) by lemma segment addition — justified
      ✓ p2: equal(distance(Epi.C, O), distance(Epi.C, Epi.S') + distance(Epi.S', O)) by lemma segment addition — justified
      ✓ p3: equal(distance(O, Ecc.S), distance(O, Epi.S')) from p1, p2, d3, d4, d8, d9, h1, h2 by algebra — by calculation
      ✓ p4: parallel(line(O, Ecc.S), line(O, Ecc.E)) from perigee by lemma one line — justified
      ✓ p5: collinear(O, Ecc.E, Epi.S') from def Epi.C, def Epi.S', def Ecc.E by construction — read off the construction
      ✓ p6: parallel(line(O, Epi.S'), line(O, Ecc.E)) from p5 by lemma one line — justified
      ✓ p7: coincident(Ecc.S, Epi.S') from p4, p6, p3 by lemma same ray — justified
  ✓ conclusion: coincident(Ecc.S, Epi.S') from same — justified (it is same)

Exit code

famulus-astra check <id> exits 1 unless the text passes all its levels (--allow-incomplete lifts that), so it can gate a build. --json gives the report as data (build/<id>/check.json).