All arrows below are planned, not checked proof dependencies. Blue: proposed definition expansion; gray: notation use; amber: mathematical prerequisite; purple: engineering gate. Overview arrows may summarize longer planned paths.
From the plan to checked proofs
Open the checked arithmetic DAG · Conservative definitions and theorem uses · All exact local evidence. These are supporting results; the full irrationality target remains open.