Skip to content

8. Research queue: turn the ten stages into checkable work

The original plan proposes stages 0–10. This queue makes the prerequisites and the exit tests explicit. "Started" means a reader guide exists; it never means the corresponding mathematical claim is proved. Work on independent rows may proceed in parallel, but their results must meet the shared evidence rules in 00.

Stage Output and immediate task Depends on Exit test
0 — target 01: exact quantifiers, radical, examples None Reader can reproduce both directions of the finite-exception equivalence
1 — claim graph 04: paper-side node-and-arrow ledger Stage 0; primary PDFs Every arrow has a theorem locator, hypotheses, and an explicit status
2 — prerequisites 02: shortest useful study route Stage 0 Reader can perform the three calculations and identify deferred subjects
3 — dictionary 03 §1.4, 07: source-located working terms and reader questions Stages 1–2 Every entry states allowed maps and what cannot yet be compared
4 — IUT I 03: first-pass trace of data, theaters, and links Stages 1–3 Explain one concrete job of each construction using IUT I's own definitions
5 — IUT II 03, 04: reconstruction and quantitative inputs Stage 4 State the quantity, normalization, theorem, and its downstream consumer
6 — IUT III 03, 05: Theorem 3.11, Corollary 3.12, Step (xi) Stages 4–5; primary IUT III Independent expert can check each comparison or point to the exact gap
7 — dispute 05: Scholze–Stix objection and Mochizuki's answer Stage 6; both sides' primary texts Each disputed arrow has both interpretations and a testable obligation
8 — IUT IV and Lean 04, 06, 06a: downstream claims and conditional Lean assumptions Stages 0–1; IUT IV; pinned Lean snapshot Trace a formal declaration to abc without assuming its unproved input
9 — adversarial review Independent explainer, critic, and formalizer test one arrow Stages 6–8 Record a concrete correction, missing premise, or reviewed proof, not a vote
10 — exposition Connected reader guide and diagrams from checked edges Stages 0–9 Each explanation links back to the exact node, arrow, source, and remaining gaps

Next bounded investigations

  1. Check the full hypotheses and quantified objects in IUT III Theorem 3.11, Corollary 3.12, and especially Step (xi) against the first-pass claim ledger. An independent expert must validate the comparison domains and indeterminacies.
  2. Reconstruct IUT IV Propositions 1.1–1.8 and the separate [GenEll] Theorem 2.1(i) input behind Corollaries 2.2–2.3. Record which inequalities are for heights, conductors, or log-volumes, and the exact rule converting one to another.
  3. Compare the pinned Lean theorem types with the published Corollary 3.12. Supply and review the missing premise; audit external dependency sources instead of counting a successful conditional build as a proof of that premise.
  4. Give the disagreement to two human experts in its strongest source-linked formulations; ask each to identify the first arrow they would accept or reject. Do not turn differing verdicts into an invented consensus.

For every investigation, capture: node ID | source URL and PDF page/section or code SHA/lines | exact hypotheses | mathematical operation | claimed conclusion | objection if any | verification performed | unresolved item. PDF page numbers and printed page numbers can differ; record which is used. Prioritize stage 6, then stages 7 and 8, before producing a polished "IUT in 20 diagrams." A diagram is a deliverable only after its edges can be audited.

Stages 1 and 4–6 checkpoint (2026-10-05): The paper-side route and 15-node graph locate IUT I–IV's named propositions. They correct the plan's straight line: Theorem 1.10 specializes Corollary 3.12 with added hypotheses, and IUT IV uses the separate [GenEll] input. Step (xi) in IUT III remains DISPUTED; the [GenEll] proof and earlier reconstruction machinery have not been independently re-derived here.

Stage 7 checkpoint (2026-10-05): The source-paired dispute guide distinguishes Scholze–Stix's proposed linear identification, under which they say the critical estimate loses its force, from Mochizuki's reply that this identification is not an allowed comparison and would make Theorem 3.11 inapplicable. This states the disagreement; it does not decide whether the published comparison is justified.

Stage 8 checkpoint (2026-10-05): A pinned Lean source audit identifies a machine-readable conditional route toward classical abc. Its Corollary312Variant input is unproved there; the repository distinguishes that variant from the published Corollary 3.12. Auditing the missing premise, transcription, and external package sources is still open. The dependency ledger records a successful build at the pinned commit and separates unused challenge stubs from the audited implication chain; neither fact proves the missing premise.