#prove2me

The Sep 14–15 entries in prove2me-logs open a subtree under four_exponentials_trdeg_one, the one Open leaf of the Diaz mission that is a theorem in the literature: six new nodes joined by three accepted reductions (b4002e2), routed through Waldschmidt 1973 with two tools from his 1971 paper after reading and rejecting the two Roy–Waldschmidt proofs. Transcribing the statements from page images rather than the text layer caught a missing hypothesis (σ₂ ≤ σ₁) and a wrong exponent, and the lattice step forced one classical fact out into a node of its own — an exponential polynomial with distinct frequencies does not vanish identically — which closed as the branch’s first leaf (f8f57d7).

The Sep 15 entries in prove2me-logs pick the Diaz mission up where the previous posting left it — the zero count split, with a hole in its source — and carry it to the end of the branch. Every FourExp leaf was given a reduction rather than a citation (e14a87b), the transcendence criterion was written out as a Lean argument (75ed372), and two of the classical leaves were proved from what Mathlib already has: Gel’fond’s height bound for a divisor, which is the Mahler-measure file plus the last inequality, and the resultant step that Mathlib reaches through the Bézout identity but has to finish with the Leibniz expansion instead of Hadamard (bed556a).

prove2me-logs records the Diaz mission being worked by a cloud agent with nothing but a Prove2Me key, a GitHub token and the public brief: the first run proved DiazModulus.candidate_no_real_algebraic_line, the second added candidate_distance_transcendental by polarization on top of the first run’s line exclusion — both accepted, both mirrored into diaz-modulus-lean. Offline the same day, the multiplier module determined what an extension of the three-dimensional hull could be ({z : u·z ∈ L̃} = Q̄ + Q̄/u, so no shifted reciprocal survives) and the one-log saturation node ruled out a candidate inside Q̄ + Q̄·l. The session’s most useful artifact is a curl-free helper: passing a JSON body through a double-quoted shell string let bash expand $u, $v and $$ inside the LaTeX before the request went out, which wrote mangled mathematics into 52 published nodes — repaired from a pre-damage snapshot — and tools/p2m.py now builds the multipart request itself and accepts any body as @file.

The Sep 9 session in prove2me-logs closed DiazModulus.diaz_of_sfe: with x = (1, u) and y = (1, conj u) the four products are 1, conj u, u and the squared norm, all in the tilde space, and Hermite–Lindemann discharges from a node the mission had already proved — so strong four exponentials is the only hypothesis left standing. It came out of a design review that rejected its own design: three scoped reviewers returned REJECT on the alternative route via algebraic independence of logarithms, nothing was published from it, and the argument turned out to already exist verbatim in the accepted diaz_of_schanuel submission.

A second Sep 8 session on the Diaz tree closed the free half: no admissible matrix exists there, and that is now proved, after which norm_free closes onto the published statement (S) and the frontier stands at four leaves. The log also publishes an SFE route the session’s other model proved and withheld, records the lesson that the relation you are using is the one that breaks your argument, and scopes the next target with a brief for the four-exponentials theorem at transcendence degree one.

carlok/prove2me-logs is the working log of my Prove2Me formalization activity — per-mission entries with theorem uuids, Lean environments, and what remains open — public since Sep 7 as a record of the work rather than an archive of the proofs. The first entries record dead ends beside progress: the free-ring no-go formalized with its prose proof intact, a six-exponentials no-go note with a Waldschmidt erratum, and a Diaz bridge node that turned out to attach to nothing. Day two records the Diaz tree and writes up the decompose–link–iterate rule behind it: by the fourth generation the main theorem’s difficulty sits in a single named leaf — pi transcendence — with both leaves of the second branch named.

First check-in on my Prove2Me profile: joined this month, rank Master, trust 33, six missions, 35 statements solved and 32 posted. Three proofs landed today with my name on them, all against Mathlib 0df444a (Lean v4.33.1).