For an integer base N ≥ 2, positive increasing exponents uj with liminf uj+1/uj ≥ 2, and nonzero rational coefficients λj with log H(λj) = o(uj), the paper proves that x = Σj≥1 λjN−uj is irrational and μ(x) = limsup uj+1/uj, including infinity. This page draws the Lean proof's dependencies: every project declaration used directly or indirectly by the main theorem, with its axioms. The drawing explains the proof structure; the release verification records are linked below.
Figure. Dependency graph of the Lean proof.
Three levels. Overview: the parts of the proof. Modules: the Lean files of one part, grouped by folder when there are many. Declarations: one declaration with what it uses and what uses it. Click a node for details; double-click, or use the button in the panel, to open it one level deeper. Arrows point from a user to what it uses. Without a mouse, use the search box and the links in the panel, which reach every node; the parts are also listed in text further down.
Statement
In the paper
H(a/b) = max(|a|, b) for reduced a/b with b > 0.
Theorem 1.If N ≥ 2, the uj are positive increasing integers, λj are nonzero rationals, log H(λj) = o(uj) and liminf uj+1/uj ≥ 2, then the series converges absolutely, its sum x is irrational, and μ(x) = limsup uj+1/uj ∈ [2, +∞].
theorem Paper4.theorem_1
(N : ℕ) (hN : 2 ≤ N)
(u : ℕ → ℕ) (hu_pos : ∀ j, 0 < u j) (hu_strict : StrictMono u)
(coeff : ℕ → ℚ) (hcoeff : ∀ j, coeff j ≠ 0)
(hheight : Tendsto
(fun j => Real.log (rationalHeight (coeff j) : ℝ) / (u j : ℝ))
atTop (𝓝 0))
(hgap : ∀ ε : ℝ, 0 < ε → ∀ᶠ j : ℕ in atTop,
2 - ε ≤ exponentRatio u j) :
Summable (fun j => |term N u coeff j|) ∧
Irrational (∑' j, term N u coeff j) ∧
(2 : EReal) ≤ irrationalityExponent (∑' j, term N u coeff j) ∧
irrationalityExponent (∑' j, term N u coeff j) =
Filter.limsup (fun j => (exponentRatio u j : EReal)) atTop
Lean index j = 0 represents paper index 1. EReal retains an infinite exponent. The hypotheses are the paper's assumptions; no cited result or profile theorem is assumed. The displayed statement is from the tagged Solution.lean; Challenge.lean is its comparison statement.
Axioms
The actual #print axioms output contains exactly Lean's three standard axioms: propositional extensionality, choice and quotient soundness. No sorryAx or project-specific axiom occurs in the main proof. The frozen release receipts record a clean build, axiom check, stock nanoda 0.4.19 accepting 30,847 declarations with no typechecker errors, and comparators at ca04cfc and via lake comparator without a sandbox, all on 2026-11-09 EST. The Palomar sandboxed mechanical run 42737481615 accepted the Lean kernel, nanoda and con-ron checks on 2026-11-10 UTC. PALOMAR-2026-11-10-000002 records automated review with no problems identified; this is automated review, not human peer review. These are historical release checks. This map was built only to extract the graph; those checkers were not rerun for the drawing.
How the parts are formed
The parts follow the completion of Theorem 1 in §8, using §5's arithmetic and truncation lower bound, the continued-fraction exponent identity from §§2 and 8, and the upper-profile argument from §§3–7. The latter includes finite reversal, the five perturbation gap classes, reduced-denominator scales, the uniform finite-profile induction and transfer to the actual infinite continued fraction. These are one dependent chain, so they stay in one input part and remain individually visible in Modules and Declarations. The paper-to-Lean notes describe intermediate export differences: the main theorem has the same hypotheses and conclusions, while the five-way relation exports the gap information needed by induction, and some stronger auxiliary asymptotics are not separate Lean exports. Section 9 examples are outside this main-theorem map.
Each input part is the dependency closure of its named anchors. One closure gives that part; two or more give Shared declarations; declarations in none give final assembly. Parts belong to declarations, not files; one file may appear in several module views. The anchors isolate the three inputs used at completion, so a lower-level theorem already consumed by the profile chain is shown in Shared when another input also needs it. No generated certificate-data or vendored-source family was found in this package. The lack of edges between exclusive input parts follows from this rule and is not an acceptance check. Overview counts the main theorem separately: Final has 10 other declarations in 4 files. Its module and detail panels include the main theorem and label the total as 11 including main theorem.
Most-used declarations
Counted by direct uses in the extracted project graph.