Companion note, version 1.9

Appendix A checked statement by statement against the formal nodes. Proposition 5.9, Theorems 6.1 and 6.12 and Corollary 6.13 are now marked "Proved, assuming Baker": their nodes take Baker's theorem on linear forms in logarithms, or its instance at u and ū, as an explicit hypothesis, and Section 1 now lists Baker's theorem as a third input used without proof. Corollary 3.4 is marked Not formalised: it follows from Diaz.period_plane_norm, but no node states it. Proposition 3.2 is restated as Diaz.quantisation_orbit_iff_re_ne_zero proves it. The mirrored library holds 254 results.