DEF0224canonicalv1Tower Decidable Check
At each finite primorial level, all three conjectures are decidable. Gap types, forbidden moves, and scope labels all defined.
Payload
Tower Decidable Check
At each finite primorial level, all three conjectures are decidable. Gap types, forbidden moves, and scope labels all defined.
Tower Decidable Check
Summary
At each finite primorial level, all three conjectures are decidable. Gap types, forbidden moves, and scope labels all defined.
Statement
\label{def:tower-decidable}
At each finite primorial level, every instance of all three conjectures
is decidable: Goldbach($n$) for specific~$n$, $\pi_2(N)$ for specific~$N$,
and ABC$(a,b)$ for specific pairs.
\textbf{Lean:} \texttt{tower\_decidable\_check}.\quad
\textbf{Registry:} III.D111.
Proof / Justification
This item is definitional. No manuscript proof is required.
Source Context
- Registry source:
book-03.jsonlline 283 - Manuscript source:
2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part10/ch81-additive-conjectures-deep.texlines 423-430
Lean / Formalization Notes
- Formalization:
formalized - Module:
TauLib.BookIII.Bridge.ConjectureGaps - Name:
tower_decidable_check
Dependencies
- Canonical: III.D112, III.D113
Related Results
Generated by later projection phases.
Related Publications
Generated by later projection phases.
Revision Notes
- 2026-04-24: Initial pilot migration.
Identifiers
Aliases & legacy IDs
III.D111tower-decidable-checkdef:tower-decidableRelease lines
corpus_v3_workingcorpus_v2Relations
Appears in (1)
Sources
Version & History
Status disclaimer
A Corpus Item page reports the program's current internal record for this item. It does not imply external verification, scientific consensus, or final proof unless explicitly stated. Read it together with its dependencies, formalization status, and the program's overall stance.