Companion note, version 1.16

Version 1.16 records what the batches of 2 October 2026 machine-check.

• Baker's theorem, in its qualitative inhomogeneous form, is now proved in the formal development, along the route of Bertrand and Masser in Chapter 4 of Waldschmidt's book: the criterion of Schneider–Lang for ℂ^{d₀} × (ℂ^×)^{d₁}, d₀ ≤ 1, with a Schwarz lemma for Cartesian products. Section 1 says so, and the four appendix rows that had read "Proved, assuming Baker" now name unconditional forms and read Proved.
• A new subsection, "Products on the axes", adds Proposition 6.11, Theorem 6.12 and Corollary 6.13: Diaz's conjecture (Qr2) of 2007 in transcendence degree one, with the classification of real and purely imaginary products of two logarithms behind it, and the case of a candidate. They are immediate from Diaz's own argument with the four exponentials theorem in transcendence degree one in place of the conjecture; that combination was not found in the sources read.
• The title of Brownawell's 1974 paper is corrected.

The appendix was checked against the live board (115 identifiers, no mismatch); the Lean project holds all 340 proved results.