Companion note, version 1.12

Waldschmidt's 1973 theorem in its algebraic-independence form is now machine-checked: if x₁, x₂ and y₁, y₂ are linearly independent over ℚ and e^{x₁y₂}, e^{x₂y₂} are algebraic, two of the eight numbers x_i, y_j, e^{x_iy_j} are algebraically independent. It is formalised as a one-column extension of the four exponentials development, and with it Schneider's eighth problem (at least one of e^e and e^{e²} is transcendental) and the e^{π²} statement (if e^{π²} is algebraic, then e and π are algebraically independent; Corollaire 1 at α = −1). Section 4 no longer says the theorem is not formalised, the consequence added in v1.11 is unconditional, and the status "Proved, assuming Waldschmidt 1973" is gone from Appendix A. No new mathematics is claimed. The mirrored library holds 283 results.