diaz-modulus-lean and prove2me-logs: a misread exponent, and the 1973 construction split in four

With the transcendence criterion and the zero count closed, the last thing between the four exponentials theorem in transcendence degree one and a full proof is Waldschmidt’s 1973 construction — and re-deriving it against the published statement before splitting its core turned up a sign lost when the formula was read off a noisy text layer: the order of differentiation is S = ⌊N²(log N)^(−1/2)⌋, not the published S = ⌊N²√log N⌋. It matters — the construction’s polynomial has degree about r·S and log-height about S·log S, both of which must stay under a fixed multiple of N²/√log N and N²√log N; with the paper’s S the ratios stay bounded (1.00 and about 1.9 at every size checked), with the published one they grow to 27.6 and 56.9 at N = 10¹².

Nodes cannot be edited, so the repair in diaz-modulus-lean is additive: restated construction_core_1973 and construction_count_1973, a second reduction of the construction step citing them, and the old pair left on the board as a dead branch — not false, since its hypotheses are exactly what the subtree proves impossible, but unreachable by the only route anyone has. The restated core reduces to four children, one per step of the paper’s proof: the field, Siegel’s lemma for the auxiliary function, extrapolation through the maximum principle, and the norm. Two things are simpler here than in the paper, since all four exponentials already lie in the field generated by ω and ω₁: plain integers suffice instead of a number field, and the field norm becomes a resultant. All four children are Open, along with the three elementary leaves that were already there, and the journal entry carries what is not proved as loudly as what is.