Where Theorem 3.11 sits: the log-volume content of the results cited in the proof of IUT III, Corollary 3.12, does not imply its conclusion

The inequality of Corollary 3.12 of IUT III is obtained in Step (xi) of its proof, where the author states that he will be concerned only with certain qualitative properties of the multiradial algorithm of Theorem 3.11, "temporarily forgetting" its internal structure. This note lists every result that the corollary and its proof cite (152 citations of 61 targets), keeps the 22 that the proof uses as definitions or premises, and states their content as axioms about normalized log-volumes of regions in tensor packets with Haar measure, at the strength of the source. A weak reading of the property (SHE) of Remark 3.11.1(iii) follows from these axioms. The note gives models of the axioms in which the conclusion of Corollary 3.12 fails; one of them is built from the actual local objects at a finite extension of Qp that carries the local data of a theta function, and the models survive the addition of any finite set of further places. Two strong readings of (SHE), and the equality (9-1) that the interim report of Project LANA identifies as the missing step, read at the level of log-volumes, each imply the conclusion, and none of them follows from the axioms. A Venn diagram displays this position, drawing each statement as the class of structures in which it holds: the models of the cited theory lie inside the class of weak (SHE) and not inside that of the conclusion, and among them the conclusion holds exactly where strong (SHE) holds. The statement "3.11.5" that Mochizuki isolates in his report on formalization corresponds to that intersection. The conclusion does follow if the images of the Θ-pilot and the q-pilot are identified, but then the degree scale of the Θ-link is 1. For the same passage, the public repository lana-agents/iut of Project LANA proves in Lean non-derivability from a package collecting what it proves at the level of Theorem 3.11; the results here were obtained independently of it, and it was made public first. We do not claim that Corollary 3.12 is false, nor anything about abc. The result concerns what follows from the statements that the proof cites, including what Theorem 3.11 states about the output of its algorithm; whether the construction of the algorithm itself supplies the missing membership is not decided here. All statements proved in the note are checked in Lean 4 (v4.30) with Mathlib, with no axioms beyond the standard three; the Lean sources are in the folder where-311-sits/lean. Lean does not check that the axioms state the cited results correctly; that correspondence is checked against the source and is described in the note. The proofs were found with generative AI tools (large language models) under the author's direction, and these tools were also used for the computations, the formalisation, the writing and the code that draws Figure 1. Every statement marked [P] is checked in Lean 4 with Mathlib. The correspondence between the axioms and the cited results is checked against the source texts, as described in the note, and is not checked by Lean. The author's own reading of the proofs is still in progress. The author takes full responsibility for the note. Changes in 1.0.1. The disclosure now says what was done. Version 1.0.0 said instead that the author had checked every proof, computation and reference, and that the author had checked each inclusion of Figure 1; those sentences are removed. Section 10 now states that only Theorem 1 of the first report (the initial Θ-datum) is used, and not the source application of its Theorems 5 and 6, which version 0.1.7 of that report withdrew. Nothing else changed; the Lean sources are identical. The deposit contains the note and an archive of the folder where-311-sits/ (the LaTeX source and the Lean sources), made from tag v0.23.1 of github.com/turahigashi/iut-explicit-initial-theta. The note is licensed under CC BY 4.0 and the Lean sources under the Apache License 2.0.