Transcendence theory in Lean 4

14 Results not found in the sources read

This chapter lists the library’s results that were not found in the literature checked, sorted by how much they add. “Not found” means not found in about 110 sources (the papers and books of Diaz, Roy, Waldschmidt and Brownawell, and those they build on) nor in the works citing the key papers, as of 5 October 2026. It never means “new”: each claim can fall to a source not yet read. “Not routine” means that the proof is not a substitution into a printed theorem. The source line of each statement says what is printed nearby. In the dependency graph, the results of the first list have a double border.

Not found, and not routine.

  • Theorem 10.6: the four-dimensional extensions \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z\) of a point of a circle that carry a \(2\times 3\) configuration are exactly those containing \(u^{2}\), \(\bar u^{2}\) or some \(1/(u-a)\). Its key step, Lemma 10.2, is the converse of a printed observation.

  • Theorem 10.1: no \(2\times 3\) configuration on generic data, whatever numbers are added. Its case \(m=0\) is Roy’s.

  • Theorem 10.14: in the power hulls \(\overline{\mathbb {Q}}u^{-k}+\overline{\mathbb {Q}}u^{-1}+\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}u^{k}\) a configuration exists only for \(k=2,3\), so the strong six exponentials route at a candidate stops at \(u^{3}\).

  • Theorems 12.2 and 12.3: on generic data every quadratic relation is a multiple of the norm form, and the period never enters.

  • Theorems 12.5 and 12.6: a counterexample has no vanishing coefficient, and its only singular pencil is the norm form.

  • Theorems 10.16, 10.22 and 10.28: separation over any field, the normal form of \(2\times 2\) configurations near a point of a circle, and configurations in Laurent hulls.

Not found, but short: one substitution into a printed theorem, or a few lines.

  • Theorem 10.9: five-dimensional spaces \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u+\overline{\mathbb {Q}}z+\overline{\mathbb {Q}}\bar z\), with \(z=u/(u^{2}-a)\) or \(u/(u^{2}-a)^{2}\), carry a configuration that no four-dimensional extension of \(\overline{\mathbb {Q}}+\overline{\mathbb {Q}}u+\overline{\mathbb {Q}}\bar u\) inside them carries; and Proposition 10.10, the conjugation-stable case, which carries none. Their consequences at a candidate are printed (Corollary 10.13).

  • Corollary 11.2: \(\mathrm{Li}_2(1/2)\) is irrational, or \(e^{i\gamma /\pi }\) is transcendental for every rational \(\gamma \neq 0\); and its general form, Proposition 11.1, which is Brownawell’s Corollary 5 [ Bro74 ] with rational scaling.

  • Theorem 13.3: Diaz’s (Qr2) in transcendence degree one; and Theorem 13.4, pair rigidity in transcendence degree one.

  • Corollaries 13.6 and 13.7: \((\log 2)^{2}+\pi ^{2}\) and \((\log 3)^{2}+\pi ^{2}\) are not both rational; and Corollary 13.10: the two open boundary statements cannot both fail at rational data.

  • Theorem 13.11: the strong five exponentials conjecture implies Diaz’s.

  • Corollaries 10.21, 10.23 and 10.26: generic configurations are \(2\times 2\) over any field, their constant terms form an invertible matrix, and at a candidate they are never matrices of logarithms. Propositions 10.30 and 10.31: which pairs of powers a Laurent hull lets Roy’s theorem exclude, and the powers \(u^{4^j}\), which it cannot.

  • Theorem 10.35: two poles carry a configuration invisible to four-dimensional extensions, with no conjugation condition. Proposition 13.20 and Corollary 13.21: under the case \(n=2\) of Kirby’s weak Schanuel conjecture, a candidate has \(\operatorname {Im}u\in \pi \mathbb {Q}\), and Diaz’s conjecture reduces to one relation.

The companion note in the repository states and attributes all of these, with the passages read.