Converge on a shared Mathlib and Tau Ceti pin. Move the imported baseline and every upstream consumer to one exact Lean/Mathlib dependency graph without weakening the kernel, linter, or source-policy gates.

Status: planned.

Canonical deliverables — these names are authoritative for this node:

• integration (proposed): MazurTheorem.Release.sharedDependencyGraph Pin Mazur and the tested Tau Ceti consumer workspace to one exact Lean, Mathlib, and transitive dependency graph.

• integration (proposed): MazurTheorem.Release.tauCetiConsumerBuild Build the Tau Ceti contracts as a downstream consumer without weakening either repository's quality gates.

Integrate finite and prime point-order APIs. Expose one unconditional statement saying that every rational torsion point has one of Mazur's allowed orders.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): MazurTorsion.rationalTorsion_orders_mem_cyclicOrders Combine all finite endpoints and the prime-order theorem into an unconditional allowed-order result.

Kernel-check Mazur's torsion bound. Feed the unconditional point-order theorem to the compiled cardinality reduction and prove that rational torsion has cardinality at most 16.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• theorem (proposed): Challenge.Mazur.torsion_ncard_le Prove the exact Lean Pool challenge statement that the rational torsion set has ncard at most 16.

Final exposition, provenance, and reproducibility audit. Verify every Blueprint arrow against the actual declaration graph, reproduce the build from the lockfiles, and publish source and axiom reports.

Status: blocked.

Canonical deliverables — these names are authoritative for this node:

• audit (proposed): MazurTheorem.Release.kernelAndProvenanceAudit Record the final axiom report, exact source pins, declaration provenance, and reproducible build evidence.

• integration (proposed): MazurTheorem.Release.versoBlueprint Publish a Verso blueprint whose labels and mathematical dependency edges exactly match the canonical programme.