diaz-modulus-lean: note v1.17 — a dilogarithm dichotomy, a barrier on generic data, three manuscript results

Version 1.17 of the Diaz companion note records what the 4 October batch machine-checks, taking the mirrored library to all 346 proved results on Lean’s three standard axioms (f91a531). Proposition 3.9 and Corollary 3.10 turn a rational relation a·t² + b·π² into a dichotomy: Li₂(1/2) = π²/12 − (log 2)²/2 is irrational, or e^(iγ/π) is transcendental for every rational γ ≠ 0 — both alternatives open, and the proposition is Brownawell’s Corollary 5 (1974) in general form. Theorem 5.4 is a barrier on generic data: no rank-one 2×3 configuration has its products in ℚ̄ + ℚ̄u + ℚ̄ū + Σℚ̄w_j, so Roy’s strong six exponentials theorem cannot refute a candidate on generic data, whatever logarithms are added. Corollaries 6.11 and 6.12 and Theorem 6.13 are Theorems 2.5, 2.3 and 3.9 of the manuscript, as direct instances of Waldschmidt’s 1973 Corollaire 4; Appendix A adds six rows (121 identifiers checked against the platform, 0 mismatches) and the README now credits M. Karatarakis’s Lean formalisation of Baker’s theorem, which the 1 October survey missed (5f940ac). The same day the library mirrored eight Diaz nodes contributed on Prove2Me by nickrobbins95, each module header naming the author (354 of 354, f0fde04).