10. XI-001: does the native \(q\)-value reach the bounded output?

Result of the bounded experiment (2026-10-06). In IUT III, Step (xi), the output hull and its log-volumes are constructed, and (xi-f) asserts that the fixed, native \(q\)-pilot value belongs to the bounded output half-line. Independent readings and separate source and mathematical checks have not established, from the passages audited here, the choice-compatible numerical comparison that would derive this particular membership. That locates an obligation; it does not show that no argument elsewhere in IUT could discharge it, prove abc, or refute the published claim. The two interpretations still differ on whether the Scholze--Stix diagram is a required path for this comparison.

This page follows the experiment protocol and the typed object ledger. It reports what sources say, what follows from explicit premises, and what remains disputed as three separate results. ACCEPTED_FOR_SYNTHESIS licenses a faithful, source-located description, not the mathematical truth of a disputed inference.

Graduate-level walkthrough (intuition only)

Separate the output-side estimate from input-side selection. Let \(s=-|\log(\Theta)|\) denote the claimed output threshold. For each allowed choice \(\beta\), imagine an output value \(t_\beta\) certified by a hull construction, with \(t_\beta\le s\). To bound the fixed \(r=-|\log(q)|\), one still needs a compatible \(r\le t_\beta\) for at least one such \(\beta\) in the same normalization. This would imply \(r\le s\). It is a checklist of sufficient premises, not a restatement of what the checked passages prove. In particular, neither inclusion of possible output regions nor a vertical bijection of hull volumes alone supplies the required native-to-output comparison.

Use the frozen packet to ask which theorem, map, and quantified choice would justify that inequality. An ACCEPTED_FOR_SYNTHESIS source attribution only establishes what a passage says; it does not promote (xi-f)'s printed membership to an independently verified deduction.

Preparation, not evidence: the typed ledger, prerequisite route, and Vaaler's abc lecture for the conjecture's broader motivation.

One edge, in ordinary language

Fix the paper's initial data and the native \(q\)-pilot. Write \(Q=|\log(q)|\) and \(T=|\log(\Theta)|\) after specifying their respective normalizations. In the currently hosted IUT III, (xi-c)--(xi-f), PDF pp. 182--184, the output possibilities \(U\) are included in a visibly overlined holomorphic hull \(\overline U\); (xi-d) constructs the output ray \(B_T=\mathbb R_{\le -T}\). Separately, the input supplies the native number \(-Q\). The target in (xi-f) is

\[ -Q\in B_T, \qquad\text{equivalently}\qquad Q\ge T. \]

Set inclusion \(U\subseteq\overline U\) concerns possible output regions. It does not, by itself, order the separately given native number. Remark 3.9.5 (Ob8)/(Ob9), PDF pp. 137--139, additionally compares hull log-volumes across a vertical log-link; this is substantive positive content, not an omitted step. What must still be checked is the numerical relationship of the particular native input to an admissible output, with the same choices, log-link iterates, determinant normalization, and relevant (Ind1)--(Ind3) permissions. These requirements are questions about the paper's quantifiers, not new hypotheses asserted to hold in IUT.

Frozen packet and independent gates

The source register records the SHA-256 fingerprints, official links, pinned report revision, and pinned Lean commit. The hosted IUT III and the official Bonn Scholze--Stix PDF dated July 16, 2018 were freshly matched to the reading copies. Mochizuki's Comments, PDF pp. 1 and 5, refer to a distinct August 2018 Scholze--Stix version that was not compared; the IUT III text cited in the 2018 exchange was not separately matched to the currently hosted edition either. PDF page numbers below count from the first PDF page.

Independent first reading	Its limited question	Earliest unresolved point it reported
`N`, IUT-native	Read IUT III (xi-c)--(xi-f), including (Ob8)/(Ob9), without choosing a partisan diagram	The operation that bounds the native \(q\)-value by one choice-compatible output
`S`, Scholze--Stix	Read the six-node real-line drawing, \(j^2\) discussion, and IUT III's different hull	Whether the actual IUT route must factor through those real-line composites
`P`, Mochizuki	Give the strongest source-grounded reply, including the nonlinear hull and vertical corrections	Whether those operations select and bound the fixed native value
`L`, Project LANA / Lean	Check the proposed two-map comparison and the pinned theorem signatures	A proof of the proposed map compatibility and the further output-bound premises

None of these first readers used another's draft as evidence. An evidence gate separately checked attribution, rendered glyphs, pages, and code signatures; a mathematical referee independently checked the conditional logic and countermodels. Those are different checks. A gate can accept a description of what an author asserts while marking the asserted inference NOT_ESTABLISHED.

Atomic claims after source and inference review

For the I- and SS- object IDs, see the crosswalk. PASS in the source column confirms the specified passage, not every lemma on which it may depend.

ID, author and exact locator	Objects, operation, and choice scope	Source gate	Mathematical gate, publication status, first unknown
`XI-I1` -- Mochizuki, IUT III (xi-c), PDF p. 182	The unbarred \(U\) of possible outputs satisfies \(U\subseteq\overline U\) in the \((1,\circ)\) ambient container (`I-4`); the native \(q\) representation is described separately.	`PASS`, including the overline lost by text extraction.	Inclusion is elementary; `ACCEPTED_FOR_SYNTHESIS` for the paper's set claim. No native numerical membership follows without an additional comparison.
`XI-I2` -- Mochizuki, IUT III Rem. 3.9.5 (Ob8)/(Ob9), PDF pp. 137--139	Log-Kummer corrects a vertical shift, and realified semisimplification gives a bijection of hull log-volumes across the log-link (`I-5v`), allowing specified iterate/quotient indeterminacies.	`PASS`.	`ACCEPTED_FOR_SYNTHESIS` as a source statement; a particular native-\(q\) selector and its order law were not extracted from these passages alone.
`XI-I3` -- Mochizuki, IUT III Rem. 3.9.5(ix), PDF pp. 141--144	A prime-strip comparison loop is said to close before taking log-volume, up to formal quotient indeterminacies.	`PASS` with that qualifier.	`ACCEPTED_FOR_SYNTHESIS` as a reported operation, not an equality of the fixed native and an output log-volume. The latter is the first unknown.
`XI-I4` -- Mochizuki, IUT III (xi-d), PDF p. 183	Determinant and normalized log-volume yield the output ray \(B_T\) (`I-5`); its boundary \(-T\) is, by definition there, the negative log-volume of \(\overline U\). The native \(-Q\) (`I-6`) is listed separately as comparable.	`PASS`.	Being on a comparable real line supplies no order relation. `ACCEPTED_FOR_SYNTHESIS` for the construction, `BLOCKED` for an inequality from comparability alone.
`XI-I5` -- Mochizuki, IUT III (xi-e)/(xi-f), PDF pp. 183--184	(xi-e) describes operations executable with native input fixed; (xi-f) describes constructing the input log-volume perhaps up to approximation from indeterminacies, then prints the exact membership \(-Q\in B_T\) (`I-7`).	`PASS`; (xi-f) gives no quantified error bound there.	The membership is `ASSERTED_IN_IUT`; deriving it from the checked preceding operations is `DISPUTED`, not source-proved by this audit. First unknown: an admissible output/value law with specified choices and, if needed, approximation control.
`XI-S1` -- Scholze--Stix, §2.2, PDF pp. 9--10; eq. (1.5), p. 4	Six real-line nodes include an indexed concrete \(\Theta\) family; top isomorphism, bottom equality, four unlabelled diagonals. \(j^2\) rescaling is in prose, not on an arrow; no hull arrow is drawn.	`PASS` against the rendered official-matched PDF.	A noncommuting all-linear loop is a conditional calculation, not an IUT counterexample. `ACCEPTED_FOR_SYNTHESIS` as their objection; whether `I-1`--`I-7` factor through its particular composites remains `DISPUTED`.
`XI-P1` -- Mochizuki, Comments (C12)--(C14), PDF pp. 3--4; Report (LVEx), pp. 24--26	His response distinguishes a prime-strip real-line relation from nonlinear, indeterminacy-dependent hull relations. His region-and-area model uses restricted, chosen parameters.	`PASS`.	`ACCEPTED_FOR_SYNTHESIS` as his response, not as a verified native-\(q\) output law. The model is an analogy, not a literal IUT construction or a substitute for `I-7`.
`XI-L1` -- Project LANA, interim report §9.2, (9-1), PDF p. 46; §10.5, p. 49	For a given \(q\)-BPS and identified \(\Theta\)-BPS, it seeks some suitable admissible \(S\) with \(\eta_q=\eta^{\mathrm{anab}}_S:R_{\mathrm{val}}\to R_{\mathrm{ss}}\) as identified maps. The team says it has no proof of this condition.	`PASS`; not a claim for every \(S\).	`BLOCKED` as a source-proved bridge. Even a proof of map equality still needs an admissible reconstructed output, an actual bound, and compatible normalization; see below.
`XI-L2` -- `lana-agents/iut` at `d9465c1`, `Statement.lean:78--97` and `ClassicalAbcGenuineCanLift.lean:37--46`	`Corollary312Variant` is an unproved `Prop` definition; the latter theorem concludes `ClassicalABC` given a universally quantified `h312` over its listed concrete instances.	`PASS` on pinned signatures; no external dependency audit in XI-001.	`CONDITIONAL_FORMALIZATION` and `ACCEPTED_FOR_SYNTHESIS` as such. It does not verify published Step (xi), (9-1), or the unproved variant.

Scope of the status statement. Project LANA's July 2026 institutional announcement explicitly suspends judgment on whether IUT proves abc. Its interim report, §§10.2--10.5, PDF pp. 47--49 accepts that the Scholze--Stix hexagon does not commute while declining to infer from that alone that a proposed same-side comparison fails. Neither position is a vote that settles Step (xi). The code snapshot from October 2026 is a later conditional result, not a replacement for a proof of (9-1).

The small inference we could actually check

This is our ordinary-mathematics schema, not a theorem of IUT or Project LANA. For one paper-required input and a coherent choice \(S\), let \(V=R_{\mathrm{val}}\) and \(W=R_{\mathrm{ss}}\) be distinct spaces. After supplying the necessary identifications, take \(f=\eta_q,g=\eta^{\mathrm{anab}}_S:V\to W\), the designated input \(x\in V\), an admissible set of reconstructed output classes \(A_S\subseteq W\), and one normalized evaluation \(\nu:W\to\mathbb R\). Suppose independently that

\(\nu(f(x))=-Q\) and \(g(x)\in A_S\);
every \(z\in A_S\) satisfies \(\nu(z)\le -T\); and
either \(f=g\) as identified maps (the report's proposed, unproved (9-1)) or the weaker, correctly oriented numerical law \(\nu(f(x))\le\nu(g(x))\) holds at this input.

Then substitution or transitivity gives

\[ -Q=\nu(f(x))\le\nu(g(x))\le -T, \qquad\text{so }Q\ge T. \]

The mathematical referee checked this deduction and independently recomputed the exact rational countermodels below. This toy deduction proves none of the unverified source-side premises for IUT. The paper describes a native input value and an output ray, but the shared comparison, reconstructed membership, actual bound, and compatible choice/normalization still have to be checked together. Equality alone does not yield reconstructed membership, and neither membership nor an output bound may be inferred just by naming \(A_S\). The one-sided law can even be stronger than the desired bound at a particular output; calling it a weaker map requirement does not make it easier to source. For each required initial input, an admissible \(S\) depending on that input can suffice for a pointwise conclusion if \(Q,T\) and their normalization are stable under that choice. This is not the stronger demand for one \(S\) for all inputs, nor a conclusion for every \(S\); the exact IUT choice quantifiers remain to be checked.

Nor is raw containment of the native geometric region in the hull a necessary logical condition for a numerical bound. The raw intervals \([2,3]\) and \([0,1]\) have the same length but neither is contained in the other. If a source actually identifies their normalized volume classes in \(W\) and bounds the selected output class, a degree comparison could work without raw containment. Project LANA's \(R_{\mathrm{ss}}\) uses volume-equivalence classes (§9.2, PDF pp. 45--46); the equality needed for this argument is a goal, not a conclusion from the existence of those classes. This keeps the audit from asking for an unnecessarily strong geometric inclusion in place of the numerical law.

Rejected shortcuts and recorded repairs

These tests reject candidate inferences, not IUT itself. They preserve the mistake and the missing premise instead of silently deleting an agent's or the synthesizer's unsuccessful proposal.

Candidate / error class	Independently checked obstruction	Status and possible repair
`R1` -- hull inclusion alone implies native membership; `CONCLUSION_STRONGER_THAN_PREMISES`	\(U\subseteq\overline U\) does not put a separate number or region into either set. The earlier typed example gives a bounded hull and an external \(q_0=-1/2\) outside it.	`REJECTED` as a standalone inference; add a source-proved, choice-compatible numeric connection to the native input.
`R2` -- abstract isomorphisms suffice; `UNJUSTIFIED_IDENTIFICATION`	Put \(A=(-\infty,-1]\), \(x=-1\), \(\nu=\mathrm{id}\), \(g(v)=v\), \(f(v)=v/2\). Both are order-preserving linear isomorphisms, and \(g(x)=-1\in A\), but \(f(x)=-1/2\notin A\).	`REJECTED`. A specified equality, normalization, or correctly directed evaluated comparison is needed. These maps are toy maps, not IUT's maps.
`R3` -- report (9-1) alone implies the bound; `MISSING_MEMBERSHIP` / `MISSING_BOUND` / `HIDDEN_NORMALIZATION`	With \(f=g=\mathrm{id}\) and \(x=-1/2\), \(A=(-\infty,-1]\) does not contain \(g(x)\); replacing it by \(A=(-\infty,0]\) loses the bound at \(T=1\). With \(x=-1\) and equal maps, output evaluation \(\nu(z)=z\) but native evaluation \(z/2\) gives native \(-1/2>-1\).	`REJECTED` in each weakened setup, not a counterexample when all three premises above hold. Establish membership, output bound, and a common evaluation independently.
`R4` -- merely bijective SS-style paths force a \(j^2\) loop; `HIDDEN_LINEARITY`	An initial toy formula omitted linearity. For \(j=8\), let \(h=L_8=\mathrm{id}\), \(k(t)=t^3\), \(e(t)=64t^3\). All four maps are bijections and \(eL_8=64kh\), but \((kh)^{-1}eL_8(t)=4t\), not \(64t\).	`REJECTED_AS_STATED` by the mathematical referee. Adding real-linearity of the composites repairs the elementary identity, not its application to IUT: the SS figure does not define these composites or label a \(j^2\) edge.
`R5` -- one unspecified approximation implies exact membership; `QUANTIFIER_DROPPED`	At \(T=1\), \(-999/1000\) is \(1/1000\) from \(-1\in B_T\) but lies outside \(B_T\). If, instead, a point is arbitrarily close to this same closed ray for every positive \(\varepsilon\), it does lie in the ray: otherwise choose \(\varepsilon=q+T>0\).	`REJECTED` for a single finite error. The all-\(\varepsilon\) condition would itself require an independent source proof, and (xi-f) does not state such a metric quantifier there.
`R6` -- require the raw \(q\)-region to be a subset of the hull; `UNNECESSARY_STRONG_PREMISE`	Equal-length \([2,3]\) and \([0,1]\) illustrate equal numerical classes without raw containment.	`REJECTED_AS_REQUIREMENT` for a numeric inequality; this does not establish that IUT has the needed equality of classes.
`P07` -- an unqualified proponent-reading concession; `ATTRIBUTION_SCOPE`	Mochizuki's Report (AD/IUAD), PDF p. 22, discusses a degree inconsistency within one holomorphic structure, subject to its \(j^2\)-indeterminacy alternative; it is not a concession about his distinct-structure route.	`CORRECTED` after source review; retain the narrower attribution and do not claim he accepts the SS model of IUT.
`L04` -- no Lean declaration even assumes the variant; `SOURCE_OVERSTATEMENT`	The pinned `Statement.lean` docstring uses overbroad wording, while `classicalABC_of_variant_genuine'` visibly has a hypothesis `h312`.	`CORRECTED` in the Lean guide: the variant is not proved there; it is assumed as an explicit theorem input.

This ledger intentionally includes the failed universal toy identity R4: checking a few linear examples was not a proof that the formula held for arbitrary bijections. With real-linearity explicitly assumed, the corrected conditional identity follows by moving the \(j^2\) scalar through \((kh)^{-1}\). Neither the extra toy assumption nor the composites are printed as such on an SS diagram arrow.

Stop here; request one testable lemma

The bounded source-and-inference gates locate the first useful expert question: For the paper's required inputs and allowed choices, which numbered passage identifies, or correctly bounds, the normalized value of the fixed native \(q\)-pilot by a member of the output construction in (xi-d), with any approximation's direction and quantifiers specified? Account for the prime-strip comparison, the vertical (Ob8)/(Ob9) bijection, Rem. 3.9.5(ix)'s pre-volume loop, determinant normalization, and (Ind1)--(Ind3). An alternative that does not use Project LANA's (9-1) is welcome if its typed numerical law is source-proved. Conversely, a countermodel would have to satisfy the actual paper hypotheses, not just the weakened toy premises above.

Until that edge is independently checked by a human expert, the experiment stops here: publication of IUT III, the SS loop, Mochizuki's analogy, a Project LANA research goal, and a Lean implication conditional on an unproved variant do not individually settle the standing proof or the truth of abc.

The subsequent XI-002 source trace attempts this narrower test against a frozen eight-PDF packet; it does not reinterpret XI-001 as a proof or a refutation.