Blueprint Summary🔗

Overview

Total entries48completed: 0; deps incomplete: 0; sorries: 0; no proof: 48

Ready now1Entries with an actionable next formalization step.

Fully closed0Local code and prerequisite closure are both complete.

Actionable priorities1Entries ready now and already unlocking downstream work.

Actionable priorities (1)

«MT-BASE-INTEGRATED»(Theorem)

Ready for proof work.

tag: milestonetag: donetag: integratedtag: mazurstage: proofstatement: ready to formalizedirect uses: 14downstream unlocks: 47proof: ready to formalize

Entry index (48)

Theorems48completed: 0; deps incomplete: 0; sorries: 0; no proof: 48

Informal-only entries48

Theorem / Proposition / Lemma / Corollary Index (48)

«MT-NERON-BASE»(Theorem)
«MT-API-INTEGRATION»(Theorem)
«MT-NERON-SPECIALIZATION»(Theorem)
«MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
«MT-FFGS-CONNECTED-ETALE»(Theorem)
«MT-X11-JOIN»(Theorem)
«MT-FINITE-JOIN»(Theorem)
«MT-TC-D1-PICARD-FUNCTOR»(Theorem)
«MT-TC-B2-RR-SERRE»(Theorem)
«MT-PIN-MIGRATION»(Theorem)
«MT-X13-NONCUSP»(Theorem)
«MT-EXPOSITION-AUDIT»(Theorem)
«MT-X0-JACOBIAN»(Theorem)
«MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
«MT-X0-HECKE»(Theorem)
«MT-TC-E0-PRODUCT-DIM»(Theorem)
«MT-EC-ISOGENY-WEIL»(Theorem)
«MT-X0-EISENSTEIN-ALGEBRA»(Theorem)
«MT-X0-MODULI»(Theorem)
«MT-O35-EXCLUDE»(Theorem)
«MT-PRIME-DIVISION-FIELD»(Theorem)
«MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
«MT-O49-TOWER»(Theorem)
«MT-TC-A2-PRODUCT-FORMULA»(Theorem)
«MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)
«MT-X0-CUSPS»(Theorem)
«MT-TC-E1-JACOBIAN-VARIETY»(Theorem)
«MT-TC-A1-ORDER-SUPPORT»(Theorem)
«MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
«MT-FINAL-ASSEMBLY»(Theorem)
«MT-PRIME-ISOGENY-CHAIN»(Theorem)
«MT-X11-COSET»(Theorem)
«MT-PRIME-SHAFAREVICH»(Theorem)
«MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
«MT-X18-NONCUSP»(Theorem)
«MT-PRIME-HERBRAND-KUMMER»(Theorem)
«MT-FFGS-OORT-RAYNAUD»(Theorem)
«MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)
«MT-TC-F1-ABEL-JACOBI»(Theorem)
«MT-O25-EXCLUDE»(Theorem)
«MT-X0-INTEGRAL»(Theorem)
«MT-PRIME-SPLIT-SEQUENCE»(Theorem)
«MT-NERON-COMPONENTS»(Theorem)
«MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)
«MT-BASE-INTEGRATED»(Theorem)
«MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
«MT-FFGS-BASIC»(Theorem)
«MT-PRIME-SEMISTABLE»(Theorem)

By parent groups (5)

Integral X₀(N), its Jacobian and Hecke action, a private Eisenstein witness constructor, and the exact Néron/finite-flat specialization needed at 5. Stage weight: 400 points. (14)

Assemble allowed point orders with height-descent torsion finiteness and finite-abelian shape to prove the full fifteen-group classification, then derive the ncard challenge and audit the release. Stage weight: 50 points. (4)

Canonical coherent cohomology, relative Picard, Jacobian, Abel–Jacobi, Néron prerequisites, and elliptic isogenies, split into startable work packages. Stage weight: 300 points. (13)

«MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)
«MT-TC-F1-ABEL-JACOBI»(Theorem)
«MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)
«MT-TC-A1-ORDER-SUPPORT»(Theorem)
«MT-TC-E1-JACOBIAN-VARIETY»(Theorem)
«MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)
«MT-TC-A2-PRODUCT-FORMULA»(Theorem)
«MT-EC-ISOGENY-WEIL»(Theorem)
«MT-TC-E0-PRODUCT-DIM»(Theorem)
«MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
«MT-TC-B2-RR-SERRE»(Theorem)
«MT-TC-D1-PICARD-FUNCTOR»(Theorem)
«MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)

Close level 13 and orders 18, 25, 35, and 49; obtain order 11 from the uniform formal-immersion route, reuse the same engine for squarefree level 35, and reduce order 49 directly to the checked X_0(49) cusp classification. Stage weight: 100 points. (8)

A route-neutral degree-one formal-immersion collision at 5, followed by the checked minimal-model additive exclusion, prime-to-five specialization, and ten-point enumeration. Stage weight: 100 points. (8)

«MT-PRIME-SEMISTABLE»(Theorem)
«MT-PRIME-SPLIT-SEQUENCE»(Theorem)
«MT-PRIME-HERBRAND-KUMMER»(Theorem)
«MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
«MT-PRIME-SHAFAREVICH»(Theorem)
«MT-PRIME-ISOGENY-CHAIN»(Theorem)
«MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
«MT-PRIME-DIVISION-FIELD»(Theorem)

Dependency insights

Statement-used entries47Entries reused in statement dependencies.

Tracked parent groups5Grouped health rollups for parents with more than one child entry.

Most used in statements (47)

«MT-BASE-INTEGRATED»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 14proof uses: 0direct uses: 14downstream unlocks: 47
«MT-X0-MODULI»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 22
«MT-EC-ISOGENY-WEIL»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
«MT-TC-E1-JACOBIAN-VARIETY»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 20
«MT-X0-INTEGRAL»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 20
«MT-X0-EISENSTEIN-ALGEBRA»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
«MT-X0-CUSPS»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 12
«MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 25
«MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 24
«MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 23
Show all 37 more statement-used entries
- «MT-NERON-COMPONENTS»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 14
- «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
- «MT-NERON-SPECIALIZATION»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
- «MT-PRIME-ISOGENY-CHAIN»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
- «MT-X11-JOIN»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
- «MT-TC-A1-ORDER-SUPPORT»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 26
- «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 25
- «MT-TC-B2-RR-SERRE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
- «MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
- «MT-TC-D1-PICARD-FUNCTOR»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 22
- «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
- «MT-TC-E0-PRODUCT-DIM»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
- «MT-TC-F1-ABEL-JACOBI»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
- «MT-X0-JACOBIAN»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
- «MT-X0-HECKE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 17
- «MT-NERON-BASE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
- «MT-FFGS-BASIC»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
- «MT-FFGS-CONNECTED-ETALE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
- «MT-FFGS-OORT-RAYNAUD»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
- «MT-PRIME-SEMISTABLE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
- «MT-PRIME-HERBRAND-KUMMER»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
- «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
- «MT-PRIME-DIVISION-FIELD»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
- «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
- «MT-PRIME-SHAFAREVICH»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
- «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
- «MT-O25-EXCLUDE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
- «MT-O35-EXCLUDE»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
- «MT-O49-TOWER»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
- «MT-X13-NONCUSP»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
- «MT-X18-NONCUSP»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
- «MT-FINITE-JOIN»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
- «MT-PIN-MIGRATION»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
- «MT-API-INTEGRATION»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
- «MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- «MT-FINAL-ASSEMBLY»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
- «MT-X11-COSET»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1

Group health (5)

Canonical coherent cohomology, relative Picard, Jacobian, Abel–Jacobi, Néron prerequisites, and elliptic isogenies, split into startable work packages. Stage weight: 300 points.shared_geometry

Grouped view over entries sharing the same parent.

total: 13closed: 0local-only: 0ready: 0blocked: 13incomplete Lean: 0unlock score: 293

Next: no ready child currently unlocks downstream work.
Integral X₀(N), its Jacobian and Hecke action, a private Eisenstein witness constructor, and the exact Néron/finite-flat specialization needed at 5. Stage weight: 400 points.prime_infrastructure

Grouped view over entries sharing the same parent.

total: 14closed: 0local-only: 0ready: 0blocked: 14incomplete Lean: 0unlock score: 190

Next: no ready child currently unlocks downstream work.
A route-neutral degree-one formal-immersion collision at 5, followed by the checked minimal-model additive exclusion, prime-to-five specialization, and ten-point enumeration. Stage weight: 100 points.prime_argument

Grouped view over entries sharing the same parent.

total: 8closed: 0local-only: 0ready: 0blocked: 8incomplete Lean: 0unlock score: 59

Next: no ready child currently unlocks downstream work.
Close level 13 and orders 18, 25, 35, and 49; obtain order 11 from the uniform formal-immersion route, reuse the same engine for squarefree level 35, and reduce order 49 directly to the checked X_0(49) cusp classification. Stage weight: 100 points.finite_endpoints

Grouped view over entries sharing the same parent.

total: 8closed: 0local-only: 0ready: 0blocked: 8incomplete Lean: 0unlock score: 29

Next: no ready child currently unlocks downstream work.
Assemble allowed point orders with height-descent torsion finiteness and finite-abelian shape to prove the full fifteen-group classification, then derive the ncard challenge and audit the release. Stage weight: 50 points.integration

Grouped view over entries sharing the same parent.

total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 6

Next: no ready child currently unlocks downstream work.

Metadata

Tags in use18Distinct tags currently attached to blueprint entries.

Tag rollups (18)

tag: mazur

entries: 16actionable: 1quick wins: 0linked PRs: 0
tag: done

entries: 10actionable: 1quick wins: 0linked PRs: 0
tag: integrated

entries: 10actionable: 1quick wins: 0linked PRs: 0
tag: milestone

entries: 1actionable: 1quick wins: 0linked PRs: 0
tag: blocked

entries: 30actionable: 0quick wins: 0linked PRs: 0
tag: nouns-missing

entries: 24actionable: 0quick wins: 0linked PRs: 0
tag: mixed

entries: 17actionable: 0quick wins: 0linked PRs: 0
tag: proof

entries: 17actionable: 0quick wins: 0linked PRs: 0
tag: infrastructure

entries: 12actionable: 0quick wins: 0linked PRs: 0
tag: tau-ceti

entries: 12actionable: 0quick wins: 0linked PRs: 0
Show all 8 more tags
- tag: upstream
  
  entries: 12actionable: 0quick wins: 0linked PRs: 0
- tag: compiled
  
  entries: 10actionable: 0quick wins: 0linked PRs: 0
- tag: integration
  
  entries: 6actionable: 0quick wins: 0linked PRs: 0
- tag: paused
  
  entries: 6actionable: 0quick wins: 0linked PRs: 0
- tag: statement-only
  
  entries: 4actionable: 0quick wins: 0linked PRs: 0
- tag: mathlib
  
  entries: 3actionable: 0quick wins: 0linked PRs: 0
- tag: open
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0
- tag: research-open
  
  entries: 1actionable: 0quick wins: 0linked PRs: 0

Metadata audit

Missing owner48

Missing effort48

Missing owner (48)

«MT-API-INTEGRATION»(Theorem)

Missing owner metadata.

tag: integrationtag: blockedtag: statement-onlytag: mazur
«MT-BASE-INTEGRATED»(Theorem)

Missing owner metadata.

tag: milestonetag: donetag: integratedtag: mazur
«MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)

Missing owner metadata.

tag: prooftag: pausedtag: compiledtag: mathlib
«MT-EC-ISOGENY-WEIL»(Theorem)

Missing owner metadata.

tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
«MT-EXPOSITION-AUDIT»(Theorem)

Missing owner metadata.

tag: integrationtag: blockedtag: statement-onlytag: mixed
«MT-FFGS-BASIC»(Theorem)

Missing owner metadata.

tag: infrastructuretag: donetag: integratedtag: mixed
«MT-FFGS-CONNECTED-ETALE»(Theorem)

Missing owner metadata.

tag: infrastructuretag: blockedtag: compiledtag: mixed
«MT-FFGS-OORT-RAYNAUD»(Theorem)

Missing owner metadata.

tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
«MT-FINAL-ASSEMBLY»(Theorem)

Missing owner metadata.

tag: integrationtag: blockedtag: compiledtag: mazur
«MT-FINITE-JOIN»(Theorem)

Missing owner metadata.

tag: integrationtag: blockedtag: statement-onlytag: mazur
Show all 38 more entries missing owner
- «MT-NERON-BASE»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-NERON-COMPONENTS»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-NERON-SPECIALIZATION»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-O25-EXCLUDE»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: pausedtag: compiledtag: mathlib
- «MT-O35-EXCLUDE»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: pausedtag: compiledtag: mathlib
- «MT-O49-TOWER»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: opentag: compiledtag: mazur
- «MT-PIN-MIGRATION»(Theorem)
  
  Missing owner metadata.
  
  tag: integrationtag: donetag: integratedtag: mixed
- «MT-PRIME-DIVISION-FIELD»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-HERBRAND-KUMMER»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-PRIME-ISOGENY-CHAIN»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-SEMISTABLE»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-SHAFAREVICH»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: donetag: integratedtag: mixed
- «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-TC-A1-ORDER-SUPPORT»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: research-opentag: compiledtag: tau-ceti
- «MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-B2-RR-SERRE»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-D1-PICARD-FUNCTOR»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-E0-PRODUCT-DIM»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-E1-JACOBIAN-VARIETY»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-F1-ABEL-JACOBI»(Theorem)
  
  Missing owner metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-X0-CUSPS»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-EISENSTEIN-ALGEBRA»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mixed
- «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mixed
- «MT-X0-HECKE»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-INTEGRAL»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-JACOBIAN»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-MODULI»(Theorem)
  
  Missing owner metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X11-COSET»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur
- «MT-X11-JOIN»(Theorem)
  
  Missing owner metadata.
  
  tag: integrationtag: blockedtag: statement-onlytag: mazur
- «MT-X13-NONCUSP»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur
- «MT-X18-NONCUSP»(Theorem)
  
  Missing owner metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur

Missing effort (48)

«MT-API-INTEGRATION»(Theorem)

Missing effort metadata.

tag: integrationtag: blockedtag: statement-onlytag: mazur
«MT-BASE-INTEGRATED»(Theorem)

Missing effort metadata.

tag: milestonetag: donetag: integratedtag: mazur
«MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)

Missing effort metadata.

tag: prooftag: pausedtag: compiledtag: mathlib
«MT-EC-ISOGENY-WEIL»(Theorem)

Missing effort metadata.

tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
«MT-EXPOSITION-AUDIT»(Theorem)

Missing effort metadata.

tag: integrationtag: blockedtag: statement-onlytag: mixed
«MT-FFGS-BASIC»(Theorem)

Missing effort metadata.

tag: infrastructuretag: donetag: integratedtag: mixed
«MT-FFGS-CONNECTED-ETALE»(Theorem)

Missing effort metadata.

tag: infrastructuretag: blockedtag: compiledtag: mixed
«MT-FFGS-OORT-RAYNAUD»(Theorem)

Missing effort metadata.

tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
«MT-FINAL-ASSEMBLY»(Theorem)

Missing effort metadata.

tag: integrationtag: blockedtag: compiledtag: mazur
«MT-FINITE-JOIN»(Theorem)

Missing effort metadata.

tag: integrationtag: blockedtag: statement-onlytag: mazur
Show all 38 more entries missing effort
- «MT-NERON-BASE»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-NERON-COMPONENTS»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-NERON-SPECIALIZATION»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-O25-EXCLUDE»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: pausedtag: compiledtag: mathlib
- «MT-O35-EXCLUDE»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: pausedtag: compiledtag: mathlib
- «MT-O49-TOWER»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: opentag: compiledtag: mazur
- «MT-PIN-MIGRATION»(Theorem)
  
  Missing effort metadata.
  
  tag: integrationtag: donetag: integratedtag: mixed
- «MT-PRIME-DIVISION-FIELD»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-HERBRAND-KUMMER»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-PRIME-ISOGENY-CHAIN»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-SEMISTABLE»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mazur
- «MT-PRIME-SHAFAREVICH»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: donetag: integratedtag: mixed
- «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: donetag: integratedtag: mazur
- «MT-TC-A1-ORDER-SUPPORT»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: research-opentag: compiledtag: tau-ceti
- «MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-B2-RR-SERRE»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-D1-PICARD-FUNCTOR»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-E0-PRODUCT-DIM»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: donetag: integratedtag: tau-ceti
- «MT-TC-E1-JACOBIAN-VARIETY»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-TC-F1-ABEL-JACOBI»(Theorem)
  
  Missing effort metadata.
  
  tag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
- «MT-X0-CUSPS»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-EISENSTEIN-ALGEBRA»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mixed
- «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: blockedtag: nouns-missingtag: mixed
- «MT-X0-HECKE»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-INTEGRAL»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-JACOBIAN»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X0-MODULI»(Theorem)
  
  Missing effort metadata.
  
  tag: infrastructuretag: blockedtag: nouns-missingtag: mixed
- «MT-X11-COSET»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur
- «MT-X11-JOIN»(Theorem)
  
  Missing effort metadata.
  
  tag: integrationtag: blockedtag: statement-onlytag: mazur
- «MT-X13-NONCUSP»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur
- «MT-X18-NONCUSP»(Theorem)
  
  Missing effort metadata.
  
  tag: prooftag: pausedtag: compiledtag: mazur

Structure and coverage

Informal-only48Statements with no associated Lean code yet.

Ready to formalize1Entries with an actionable next formalization step.

Blocked or incomplete47Entries not covered by the highlighted readiness buckets above.

Heaviest prerequisites (47)

«MT-FINITE-JOIN»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 3
«MT-O35-EXCLUDE»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 4
«MT-PRIME-ISOGENY-CHAIN»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 6
«MT-API-INTEGRATION»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
«MT-EXPOSITION-AUDIT»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
«MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 7
«MT-PRIME-SEMISTABLE»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 9
«MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 21
«MT-X0-EISENSTEIN-QUOTIENT»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 10
«MT-X0-JACOBIAN»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 18
Show all 37 more heaviest-prerequisite entries
- «MT-FFGS-OORT-RAYNAUD»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 11
- «MT-NERON-BASE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 15
- «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
- «MT-TC-C2-SYMMETRIC-POWERS»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 22
- «MT-TC-E1-JACOBIAN-VARIETY»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 20
- «MT-TC-F1-ABEL-JACOBI»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 19
- «MT-X0-EISENSTEIN-ALGEBRA»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 16
- «MT-X0-HECKE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 17
- «MT-X0-MODULI»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 22
- «MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
- «MT-EC-ISOGENY-WEIL»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 23
- «MT-FFGS-BASIC»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
- «MT-FFGS-CONNECTED-ETALE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 12
- «MT-FINAL-ASSEMBLY»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
- «MT-NERON-COMPONENTS»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 14
- «MT-NERON-SPECIALIZATION»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 9
- «MT-O25-EXCLUDE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
- «MT-O49-TOWER»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
- «MT-PIN-MIGRATION»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
- «MT-PRIME-DIVISION-FIELD»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
- «MT-PRIME-HERBRAND-KUMMER»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
- «MT-PRIME-SHAFAREVICH»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
- «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
- «MT-TC-A1-ORDER-SUPPORT»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 26
- «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 25
- «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 24
- «MT-TC-B1-COHERENT-COHOMOLOGY»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 25
- «MT-TC-B2-RR-SERRE»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 22
- «MT-TC-C1-RELATIVE-COHOMOLOGY»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 23
- «MT-TC-D1-PICARD-FUNCTOR»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 22
- «MT-TC-E0-PRODUCT-DIM»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 21
- «MT-X0-CUSPS»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 12
- «MT-X0-INTEGRAL»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 20
- «MT-X11-COSET»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
- «MT-X11-JOIN»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
- «MT-X13-NONCUSP»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
- «MT-X18-NONCUSP»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4

No prerequisites (1)

«MT-BASE-INTEGRATED»(Theorem)

No dependents (1)

«MT-EXPOSITION-AUDIT»(Theorem)