Blueprint Summary🔗

Overview

Total entries16completed: 16; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed16Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (16)

Definitions6completed: 6; deps incomplete: 0; sorries: 0; no proof: 0

Theorems10completed: 10; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (6)

«condition-b»(Definition)
Associated lean decls (1)
- SatisfiesConditionB
«condition-a-prime»(Definition)
Associated lean decls (1)
- SatisfiesConditionA'
«null-homologous»(Definition)
Associated lean decls (1)
- IsNullHomologous
«has-cauchy-pv-on»(Definition)
Associated lean decls (1)
- HasCauchyPVOn
«closed-pwc1-immersion»(Definition)
Associated lean decls (1)
- ClosedPwC1Immersion
«generalized-winding-number»(Definition)
Associated lean decls (1)
- generalizedWindingNumber

Theorem / Proposition / Lemma / Corollary Index (10)

«gwn-at-rho-plus-one»(Theorem)
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«valence-orbit-sum-of-pvChain»(Theorem)
Associated lean decls (1)
- valence_formula_orbit_sum_of_pvChain
«gwn-at-rho»(Theorem)
Associated lean decls (1)
- pv_integral_at_rho_tendsto
«cpv-polar-multicrossed-condB»(Theorem)
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«residue-paper-faithful-clean»(Theorem)
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
«residue-compositional»(Theorem)
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_compositional
«gwn-at-i»(Theorem)
Associated lean decls (1)
- pv_integral_at_i_tendsto
«valence-formula-textbook»(Theorem)
Associated lean decls (1)
- valence_formula_textbook
«cpv-polar-uncrossed»(Theorem)
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«hw-3-3-clean-full-mero»(Theorem)
Associated lean decls (1)
- LeanModularForms.hw_3_3_clean_full_mero

Dependency insights

Statement-used entries11Entries reused in statement dependencies.

Proof-used entries9Entries reused in proof-only dependencies.

Most used in statements (11)

«closed-pwc1-immersion»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 15
Associated lean decls (1)
- ClosedPwC1Immersion
«has-cauchy-pv-on»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 11
Associated lean decls (1)
- HasCauchyPVOn
«generalized-winding-number»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 10
Associated lean decls (1)
- generalizedWindingNumber
«null-homologous»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
Associated lean decls (1)
- IsNullHomologous
«condition-a-prime»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (1)
- SatisfiesConditionA'
«condition-b»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (1)
- SatisfiesConditionB
«residue-paper-faithful-clean»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
«gwn-at-i»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_tendsto
Show all 1 more statement-used entries
- «valence-orbit-sum-of-pvChain»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - valence_formula_orbit_sum_of_pvChain

Most used in proofs (9)

«hw-3-3-clean-full-mero»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- LeanModularForms.hw_3_3_clean_full_mero
«cpv-polar-multicrossed-condB»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«cpv-polar-uncrossed»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«residue-compositional»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_compositional
«residue-paper-faithful-clean»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
«gwn-at-i»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_tendsto
«valence-orbit-sum-of-pvChain»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
Associated lean decls (1)
- valence_formula_orbit_sum_of_pvChain

Metadata

Metadata audit

Missing owner16

Missing effort16

Untagged16

Missing owner (16)

«closed-pwc1-immersion»(Definition)

Missing owner metadata.
Associated lean decls (1)
- ClosedPwC1Immersion
«condition-a-prime»(Definition)

Missing owner metadata.
Associated lean decls (1)
- SatisfiesConditionA'
«condition-b»(Definition)

Missing owner metadata.
Associated lean decls (1)
- SatisfiesConditionB
«cpv-polar-multicrossed-condB»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«cpv-polar-uncrossed»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«generalized-winding-number»(Definition)

Missing owner metadata.
Associated lean decls (1)
- generalizedWindingNumber
«gwn-at-i»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- pv_integral_at_rho_tendsto
«has-cauchy-pv-on»(Definition)

Missing owner metadata.
Associated lean decls (1)
- HasCauchyPVOn
Show all 6 more entries missing owner
- «hw-3-3-clean-full-mero»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - LeanModularForms.hw_3_3_clean_full_mero
- «null-homologous»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IsNullHomologous
- «residue-compositional»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_compositional
- «residue-paper-faithful-clean»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
- «valence-formula-textbook»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - valence_formula_textbook
- «valence-orbit-sum-of-pvChain»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - valence_formula_orbit_sum_of_pvChain

Missing effort (16)

«closed-pwc1-immersion»(Definition)

Missing effort metadata.
Associated lean decls (1)
- ClosedPwC1Immersion
«condition-a-prime»(Definition)

Missing effort metadata.
Associated lean decls (1)
- SatisfiesConditionA'
«condition-b»(Definition)

Missing effort metadata.
Associated lean decls (1)
- SatisfiesConditionB
«cpv-polar-multicrossed-condB»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«cpv-polar-uncrossed»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«generalized-winding-number»(Definition)

Missing effort metadata.
Associated lean decls (1)
- generalizedWindingNumber
«gwn-at-i»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- pv_integral_at_rho_tendsto
«has-cauchy-pv-on»(Definition)

Missing effort metadata.
Associated lean decls (1)
- HasCauchyPVOn
Show all 6 more entries missing effort
- «hw-3-3-clean-full-mero»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - LeanModularForms.hw_3_3_clean_full_mero
- «null-homologous»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IsNullHomologous
- «residue-compositional»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_compositional
- «residue-paper-faithful-clean»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
- «valence-formula-textbook»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - valence_formula_textbook
- «valence-orbit-sum-of-pvChain»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - valence_formula_orbit_sum_of_pvChain

Untagged (16)

«closed-pwc1-immersion»(Definition)

Missing tag metadata.
Associated lean decls (1)
- ClosedPwC1Immersion
«condition-a-prime»(Definition)

Missing tag metadata.
Associated lean decls (1)
- SatisfiesConditionA'
«condition-b»(Definition)

Missing tag metadata.
Associated lean decls (1)
- SatisfiesConditionB
«cpv-polar-multicrossed-condB»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«cpv-polar-uncrossed»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«generalized-winding-number»(Definition)

Missing tag metadata.
Associated lean decls (1)
- generalizedWindingNumber
«gwn-at-i»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- pv_integral_at_rho_tendsto
«has-cauchy-pv-on»(Definition)

Missing tag metadata.
Associated lean decls (1)
- HasCauchyPVOn
Show all 6 more untagged entries
- «hw-3-3-clean-full-mero»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - LeanModularForms.hw_3_3_clean_full_mero
- «null-homologous»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IsNullHomologous
- «residue-compositional»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_compositional
- «residue-paper-faithful-clean»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
- «valence-formula-textbook»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - valence_formula_textbook
- «valence-orbit-sum-of-pvChain»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - valence_formula_orbit_sum_of_pvChain

Structure and coverage

Fully closed16Local code and ancestor closure are both complete.

Heaviest prerequisites (15)

«residue-paper-faithful-clean»(Theorem)

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

total deps: 9statement deps: 6proof deps: 3direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_paper_faithful_clean
«hw-3-3-clean-full-mero»(Theorem)

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

total deps: 7statement deps: 7proof deps: 1direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- LeanModularForms.hw_3_3_clean_full_mero
«valence-orbit-sum-of-pvChain»(Theorem)

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

total deps: 5statement deps: 4proof deps: 4direct uses: 2downstream unlocks: 1
Associated lean decls (1)
- valence_formula_orbit_sum_of_pvChain
«cpv-polar-multicrossed-condB»(Theorem)

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

total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_multiCrossed_pole_under_condB_corner
«cpv-polar-uncrossed»(Theorem)

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

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.cpv_polarPart_at_uncrossed_pole
«residue-compositional»(Theorem)

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

total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 4
Associated lean decls (1)
- HungerbuhlerWasem.residueTheorem_crossing_compositional
«valence-formula-textbook»(Theorem)

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

total deps: 2statement deps: 1proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- valence_formula_textbook
«gwn-at-i»(Theorem)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_i_tendsto
«gwn-at-rho-plus-one»(Theorem)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_plus_one_tendsto
«gwn-at-rho»(Theorem)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- pv_integral_at_rho_tendsto
Show all 5 more heaviest-prerequisite entries
- «condition-a-prime»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (1)
  - SatisfiesConditionA'
- «condition-b»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (1)
  - SatisfiesConditionB
- «generalized-winding-number»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 9downstream unlocks: 10
  Associated lean decls (1)
  - generalizedWindingNumber
- «has-cauchy-pv-on»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 9downstream unlocks: 11
  Associated lean decls (1)
  - HasCauchyPVOn
- «null-homologous»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 6
  Associated lean decls (1)
  - IsNullHomologous

No prerequisites (1)

«closed-pwc1-immersion»(Definition)
Associated lean decls (1)
- ClosedPwC1Immersion

No dependents (1)

«valence-formula-textbook»(Theorem)
Associated lean decls (1)
- valence_formula_textbook