The gap between the two walls is positive: a closed form for the (Ind2)-terms of lana-agents/iut

The public Lean formalization lana-agents/iut writes the comparison step in the proof of Corollary 3.12 of inter-universal Teichmüller theory (IUT) III — the "wall" — in two forms: a variant of Corollary 3.12, (Var), and the Scholze–Stix inequality, (SS). The difference Δ(D) of their right-hand sides is a weighted average of (Ind2)-terms at the bad residue characteristics. The repository proves Δ(D) ≥ 0 and records as open whether these terms are zero or positive. We determine these terms in closed form. The (Ind2)-term equals (ordp θ − κv(θ))·log p, where θ = q̲vj² is the theta value and κv(θ) is the largest integer k with θ·𝓘v ⊆ pk·𝓘v, 𝓘v being the log-shell. Consequently the term is always at least frac(ordp θ)·log p, with equality when p is odd and ev ≤ p − 2 (there the log-shell is a fractional ideal). At a bad place ordp θ is never an integer, because ℓ does not divide the order of q. Hence Δ(D) > 0 for every initial Θ-datum, and in this formalization (SS) is strictly stronger than (Var). On the other hand Δ(D) is bounded above by a quantity that does not involve the size of the q-orders (the values log p at the bad places and the ramification indices). The two walls are height inequalities of the same shape that differ by a term of conductor type. The average over the labels is given by the class number of Q(√−ℓ). We compute the values for six explicit initial Θ-data. The ultimate aim of this work is to understand exactly the algorithm by which IUT computes the height inequality; the (Ind2)-term is one of its steps whose value was open. The object of the note is the definitions of lana-agents/iut as they stand, whose (Ind2) group is a deliberate enlargement containing the image of Ism; for the group of the original papers the value lies between 0 and the value found here. The proofs are on paper and have not been checked in Lean. No claim is made about the truth of (Var), (SS), Corollary 3.12, or the abc conjecture. This is a preprint. Use of generative AI. The question studied in this note — to determine the value of the (Ind2)-terms that lana-agents/iut leaves open — arose in the author's discussions with generative AI tools; the author judged it important and decided to make it the subject of this note. Its ultimate aim, to understand exactly the algorithm by which IUT computes the height inequality, is the author's research direction. Generative AI tools (large language models) were used extensively, under the author's direction, in finding the proofs, in the computations and in the writing. The author takes full responsibility for the contents of this note. The deposit contains the note and an archive of the folder ind2-gap/ (the LaTeX source and the scripts with their outputs), together with the program iut-walkthrough/program/iut_compute.py that two of the scripts use, made from tag v0.15.0 of github.com/turahigashi/iut-explicit-initial-theta. The files are licensed under CC BY 4.0.