Preparing local tests dependency map
Project map · Full theorem DAG · Open textbook chapter
This map contains the 8 decomposed items in this chapter. Dashed chapter boxes stand for external prerequisites or dependents. fully proved4Proved, and every prerequisite is fully proved too.ready to state5Nothing it needs is blocked, so the statement can be written in Lean.planned8Described in the blueprint only.
graph LR
n0("Averaged degree-one test"):::can_state
n1("Invariant chart subset"):::planned
n2("Collapse and compactification"):::fully_proved
n3("Finite quotient sheets"):::fully_proved
n4("Moving a test"):::planned
n5("Homotopy extension"):::fully_proved
n6("Odd-sphere nullhomotopy"):::planned
n7("Rational orbit pullback"):::planned
n8["External chapter: Background prerequisites<br/><small>5 items · 1 fully proved · 4 ready to state</small>"]:::boundary
n9["External chapter: Character classes and the contradiction<br/><small>3 items · 3 planned</small>"]:::boundary
n10["External chapter: Main theorems<br/><small>1 item · 1 planned</small>"]:::boundary
n8 -. 2 .-> n1
n8 -.-> n3
n8 -. 2 .-> n6
n8 -. 3 .-> n7
n0 -.-> n9
n0 --> n4
n1 -.-> n10
n2 -.-> n9
n2 --> n0
n3 -. 2 .-> n9
n3 --> n4
n4 -.-> n9
n5 -.-> n4
n6 -.-> n4
n7 -.-> n9
n7 -.-> n4
click n0 "../../roadmap/local-tests/index.html#averaged-test" "Averaged degree-one test — 1 item · 1 ready to state"
click n1 "../../roadmap/local-tests/index.html#chart-reduction" "Invariant chart subset — 1 item · 1 planned"
click n2 "../../roadmap/local-tests/index.html#collapse" "Collapse and compactification — 1 item · 1 fully proved"
click n3 "../../roadmap/local-tests/index.html#finite-sheets" "Finite quotient sheets — 1 item · 1 fully proved"
click n4 "../../roadmap/local-tests/index.html#move-test" "Moving a test — 1 item · 1 planned"
click n5 "../../roadmap/local-tests/index.html#neighborhood-extension" "Homotopy extension — 1 item · 1 fully proved"
click n6 "../../roadmap/local-tests/index.html#odd-sphere-null" "Odd-sphere nullhomotopy — 1 item · 1 planned"
click n7 "../../roadmap/local-tests/index.html#orbit-injectivity" "Rational orbit pullback — 1 item · 1 planned"
click n8 "background.html" "Background prerequisites — 5 items · 1 fully proved · 4 ready to state"
click n9 "character-classes.html" "Character classes and the contradiction — 3 items · 3 planned"
click n10 "main-theorem.html" "Main theorems — 1 item · 1 planned"