Contradiction on the invariant chart: local context
Project map · Chapter map · Full theorem DAG · Open textbook statement
This local map shows one dependency hop in either direction. The highlighted item is the current focus. fully proved2Proved, and every prerequisite is fully proved too.ready to state1Nothing it needs is blocked, so the statement can be written in Lean.planned9Described in the blueprint only.
graph LR
n0("Covariance of character classes"):::planned
n1("Homotopy of character classes"):::planned
n2("Fixed sphere lattice"):::planned
n3("Collapse and compactification"):::fully_proved
n4("Averaged degree-one test"):::can_state
n5("Finite quotient sheets"):::fully_proved
n6("Moving a test"):::planned
n7("Equal parts"):::planned
n8("Action of degree"):::planned
n9("Sum of the character classes"):::planned
n10("Contradiction on the invariant chart"):::planned
n11("$p$-adic exclusion"):::planned
n0 -.-> n1
n0 -.-> n10
n1 -.-> n10
n10 -.-> n11
n7 -.-> n10
n9 -.-> n10
n4 -.-> n10
n4 --> n6
n3 -.-> n10
n3 --> n4
n5 -.-> n10
n5 -.-> n7
n5 --> n6
n6 -.-> n10
n8 -.-> n10
n2 -.-> n10
n2 --> n8
click n0 "../../../roadmap/character-classes/index.html#class-covariance" "Covariance of character classes — 1 item · 1 planned"
click n1 "../../../roadmap/character-classes/index.html#class-homotopy" "Homotopy of character classes — 1 item · 1 planned"
click n2 "../../../roadmap/sphere-lattice/index.html#sphere-lattice" "Fixed sphere lattice — 1 item · 1 planned"
click n3 "../../../roadmap/local-tests/index.html#collapse" "Collapse and compactification — 1 item · 1 fully proved"
click n4 "../../../roadmap/local-tests/index.html#averaged-test" "Averaged degree-one test — 1 item · 1 ready to state"
click n5 "../../../roadmap/local-tests/index.html#finite-sheets" "Finite quotient sheets — 1 item · 1 fully proved"
click n6 "../../../roadmap/local-tests/index.html#move-test" "Moving a test — 1 item · 1 planned"
click n7 "../../../roadmap/character-classes/index.html#equal-parts" "Equal parts — 1 item · 1 planned"
click n8 "../../../roadmap/sphere-lattice/index.html#degree-action" "Action of degree — 1 item · 1 planned"
click n9 "../../../roadmap/character-classes/index.html#sum-classes" "Sum of the character classes — 1 item · 1 planned"
class n10 focus
click n10 "../../../roadmap/character-classes/index.html#contradiction" "Contradiction on the invariant chart — 1 item · 1 planned"
click n11 "../../../roadmap/main-theorem/index.html#padic-exclusion" "$p$-adic exclusion — 1 item · 1 planned"