Constructive arithmetic · 120 major campaign milestones · definitions · evidence boundaries

Constructive Number Theory: Grand Campaign

A dependency-aware research programme in intuitionistic first-order arithmetic.

A mathematical programme, not a theorem certificate

Loading the sealed campaign description…

A multiscale constructive research atlas

Move from five mathematical domains to twelve families, individual formal targets, actual proof prerequisites, and the separate network of proposed mathematical notation.

Actual proof dependencies between mathematical domains Every weighted directed edge counts genuine prerequisites from the 144-node constructive campaign DAG.

Calculating exact cross-domain proof-dependency weights…

Currently unlocked research targets

A target is ready only when every direct prerequisite is independently checked or explicitly available. Existing unverified foundations and anchor extensions remain blockers; readiness never means the target is proved.

The constructive dependency map

Rows are proof-development layers; columns are mathematical families. Arrows show actual construction prerequisites only; conceptual connections are listed separately.

Waiting for the campaign…

Constructive number-theory campaign dependency graph Select a theorem, tool, or research goal to inspect its formal statement and direct or transitive dependencies.
available tool or anchor body-checked anchor existing anchor extension open research objective selected prerequisite path downstream dependent path

Twelve connected mathematical families

Choose a family to retain its own milestones and every cross-family prerequisite milestone, constructive tool, and existing anchor they actually require.

Global definition-dependency network

These campaign entries are proposed blueprint vocabulary, not automatically compiled conservative kernel definitions. Only signature-compatible exact names or explicitly aligned aliases linked to an existing proof explorer have independently checked registry expansion evidence. Lexical notation edges confer no proof authority.

Download the audited, layered definition DAG · signature-compatible reviewed aliases include their exact argument permutation; incompatible homonyms never inherit checked evidence.

Solid arrows in the proof map denote actual checked-or-proposed theorem prerequisites. Definition-expansion and statement-usage links here are a separate derived lexical notation DAG.

Object language and conservative definitions

Loading the constructive-language contract…

Source documents and ambitious boundaries

Research goals are not claims of existing proof, Alpha membership, checked use, or Stable admission.