Full theorem dependency graph
66 nodes · 127 dependencies. Arrows point from a prerequisite to what depends on it; dashed arrows are needed only by proofs. fully proved6Proved, and every prerequisite is fully proved too.ready to state15Nothing it needs is blocked, so the statement can be written in Lean.planned37Described in the blueprint only.
graph LR
n0["Background prerequisites<br/><small>14 items · 2 fully proved · 12 ready to state</small>"]:::scope
n1("Balmer--Walter localization"):::can_state
n2("Cech comparison"):::can_state
n3("Classical reduction"):::can_state
n4("Compact abelian Lie groups"):::can_state
n5("Hardt triviality"):::can_state
n6("Hatcher degree facts"):::can_state
n7("Newman rigidity"):::can_state
n8("Closed subgroups of $\Zp$"):::fully_proved
n9("Serre odd-sphere maps"):::can_state
n10("Sheaf cohomology bounds"):::can_state
n11("Sheaf pushforward toolkit"):::can_state
n12("Stacks derived facts"):::can_state
n13("Symmetric forms and orthogonal sums"):::fully_proved
n14("Verdier duality formalism"):::can_state
n15["Character classes and the contradiction<br/><small>8 items · 8 planned</small>"]:::scope
n16["Test categories"]:::planned
n17("Simplex generators"):::planned
n18("Verdier duality on test categories"):::planned
n19("Direct images and open extension"):::planned
n20("Symmetric cone"):::can_state
n21("Products with the interval"):::planned
n22("Product shift sign"):::planned
n23("Two endpoint forms"):::planned
n24("Homotopy invariance"):::planned
n25("Point groups"):::planned
n26("Cutoff"):::planned
n27("Objects supported in an open set"):::planned
n28("Witt localization"):::planned
n29("Contractible quotient"):::planned
n30("Germ description"):::planned
n31("Rational orbit pullback"):::planned
n32("Character coproducts"):::planned
n33("Real orthogonality"):::planned
n34["Character classes"]:::planned
n35("Covariance of character classes"):::planned
n36("Homotopy of character classes"):::planned
n37("Open cover dense inclusion"):::planned
n38("Dense doubling"):::can_state
n39("Finite diagram chases"):::fully_proved
n40("Bounded comparison"):::planned
n41("Rational sphere calculation"):::planned
n42("Signature on a finite relation"):::planned
n43("Fixed sphere lattice"):::planned
n44("Collapse and compactification"):::fully_proved
n45("Averaged degree-one test"):::can_state
n46("Finite quotient sheets"):::fully_proved
n47("Odd-sphere nullhomotopy"):::planned
n48("Homotopy extension"):::fully_proved
n49("Moving a test"):::planned
n50("Equal parts"):::planned
n51("Action of degree"):::planned
n52("Sum of the character classes"):::planned
n53("Contradiction on the invariant chart"):::planned
n54["Preparing local tests<br/><small>8 items · 3 fully proved · 1 ready to state · 4 planned</small>"]:::scope
n55("Invariant chart subset"):::planned
n56["Localization, germs, and dense subcategories<br/><small>7 items · 1 ready to state · 6 planned</small>"]:::scope
n57("Open-cover bound"):::planned
n58["Main theorems<br/><small>3 items · 3 planned</small>"]:::scope
n59("$p$-adic exclusion"):::planned
n60("Hilbert--Smith conjecture"):::planned
n61("Almost-periodic flow"):::planned
n62["HilbertSmith roadmap<br/><small>58 items · 6 fully proved · 15 ready to state · 37 planned</small>"]:::scope
n63["Sheaf categories and homotopy invariance<br/><small>10 items · 1 ready to state · 9 planned</small>"]:::scope
n64("Sign conventions"):::planned
n65["A bounded lattice on the test sphere<br/><small>8 items · 1 fully proved · 7 planned</small>"]:::scope
n1 -.-> n28
n2 -.-> n47
n2 -.-> n31
n3 -.-> n60
n4 -.-> n61
n5 -.-> n42
n6 -.-> n51
n7 -.-> n55
n8 -.-> n55
n8 -.-> n46
n8 -.-> n31
n8 -.-> n59
n9 -.-> n47
n10 -.-> n32
n10 -.-> n16
n11 -.-> n21
n11 -.-> n18
n11 -.-> n19
n12 -.-> n32
n12 -.-> n31
n14 -.-> n21
n14 -.-> n18
n14 -.-> n19
n34 --> n35
n34 --> n36
n34 --> n50
n34 --> n52
n32 -.-> n34
n32 -.-> n35
n32 --> n33
n35 -.-> n36
n35 -.-> n53
n36 -.-> n53
n53 -.-> n59
n50 -.-> n53
n33 -.-> n34
n52 -.-> n53
n45 -.-> n53
n45 --> n49
n55 -.-> n59
n44 -.-> n53
n44 --> n45
n46 -.-> n53
n46 -.-> n50
n46 --> n49
n49 -.-> n53
n48 -.-> n49
n47 -.-> n49
n31 -.-> n32
n31 -.-> n49
n27 --> n30
n27 --> n37
n27 --> n28
n26 -.-> n27
n26 -.-> n30
n26 -.-> n37
n38 -.-> n57
n38 -.-> n40
n38 -.-> n41
n30 --> n34
n30 -.-> n35
n30 -.-> n50
n30 -.-> n37
n37 --> n57
n37 -.-> n40
n37 -.-> n41
n28 -.-> n35
n28 -.-> n40
n28 -.-> n29
n28 -.-> n41
n60 -.-> n61
n59 -.-> n60
n23 -.-> n24
n24 -.-> n36
n24 -.-> n40
n24 -.-> n29
n24 -.-> n51
n24 -.-> n41
n21 -.-> n23
n21 --> n22
n22 -.-> n23
n17 -.-> n21
n17 -.-> n18
n17 -.-> n25
n20 -.-> n23
n16 --> n27
n16 --> n26
n16 --> n30
n16 --> n37
n16 --> n28
n16 --> n23
n16 --> n24
n16 --> n21
n16 --> n64
n16 --> n17
n16 --> n18
n16 --> n19
n16 --> n40
n16 --> n29
n16 --> n51
n16 --> n42
n16 --> n25
n16 --> n43
n16 --> n41
n18 -.-> n27
n18 -.-> n19
n19 -.-> n35
n19 -.-> n33
n19 -.-> n27
n19 -.-> n26
n19 -.-> n37
n19 --> n24
n19 -.-> n29
n19 -.-> n51
n40 -.-> n43
n29 --> n34
n29 -.-> n50
n51 -.-> n53
n39 -.-> n40
n42 -.-> n43
n25 -.-> n40
n25 -.-> n29
n25 -.-> n41
n43 -.-> n53
n43 --> n51
n41 -.-> n42
n41 -.-> n43
click n0 "../roadmap/background/index.html" "Background prerequisites — 14 items · 2 fully proved · 12 ready to state"
click n1 "../roadmap/background/index.html#balmer-walter" "Balmer--Walter localization — 1 item · 1 ready to state"
click n2 "../roadmap/background/index.html#cech-comparison" "Cech comparison — 1 item · 1 ready to state"
click n3 "../roadmap/background/index.html#classical-reduction" "Classical reduction — 1 item · 1 ready to state"
click n4 "../roadmap/background/index.html#compact-abelian-lie" "Compact abelian Lie groups — 1 item · 1 ready to state"
click n5 "../roadmap/background/index.html#hardt-triviality" "Hardt triviality — 1 item · 1 ready to state"
click n6 "../roadmap/background/index.html#hatcher-facts" "Hatcher degree facts — 1 item · 1 ready to state"
click n7 "../roadmap/background/index.html#newman-rigidity" "Newman rigidity — 1 item · 1 ready to state"
click n8 "../roadmap/background/index.html#padic-subgroups" "Closed subgroups of $\Zp$ — 1 item · 1 fully proved"
click n9 "../roadmap/background/index.html#serre-maps" "Serre odd-sphere maps — 1 item · 1 ready to state"
click n10 "../roadmap/background/index.html#sheaf-cohomology-bounds" "Sheaf cohomology bounds — 1 item · 1 ready to state"
click n11 "../roadmap/background/index.html#sheaf-pushforward" "Sheaf pushforward toolkit — 1 item · 1 ready to state"
click n12 "../roadmap/background/index.html#stacks-derived" "Stacks derived facts — 1 item · 1 ready to state"
click n13 "../roadmap/background/index.html#symmetric-forms" "Symmetric forms and orthogonal sums — 1 item · 1 fully proved"
click n14 "../roadmap/background/index.html#verdier-duality" "Verdier duality formalism — 1 item · 1 ready to state"
click n15 "../roadmap/character-classes/index.html" "Character classes and the contradiction — 8 items · 8 planned"
click n16 "../roadmap/sheaf-categories/index.html#test-categories" "Test categories — 1 item · 1 planned"
click n17 "../roadmap/sheaf-categories/index.html#simplex-generators" "Simplex generators — 1 item · 1 planned"
click n18 "../roadmap/sheaf-categories/index.html#test-duality" "Verdier duality on test categories — 1 item · 1 planned"
click n19 "../roadmap/sheaf-categories/index.html#test-pushforward" "Direct images and open extension — 1 item · 1 planned"
click n20 "../roadmap/sheaf-categories/index.html#symmetric-cone" "Symmetric cone — 1 item · 1 ready to state"
click n21 "../roadmap/sheaf-categories/index.html#interval-products" "Products with the interval — 1 item · 1 planned"
click n22 "../roadmap/sheaf-categories/index.html#product-shift-sign" "Product shift sign — 1 item · 1 planned"
click n23 "../roadmap/sheaf-categories/index.html#endpoint-forms" "Two endpoint forms — 1 item · 1 planned"
click n24 "../roadmap/sheaf-categories/index.html#homotopy-invariance" "Homotopy invariance — 1 item · 1 planned"
click n25 "../roadmap/sphere-lattice/index.html#point-groups" "Point groups — 1 item · 1 planned"
click n26 "../roadmap/localization/index.html#cutoff" "Cutoff — 1 item · 1 planned"
click n27 "../roadmap/localization/index.html#compact-support" "Objects supported in an open set — 1 item · 1 planned"
click n28 "../roadmap/localization/index.html#witt-localization" "Witt localization — 1 item · 1 planned"
click n29 "../roadmap/sphere-lattice/index.html#contractible-quotient" "Contractible quotient — 1 item · 1 planned"
click n30 "../roadmap/localization/index.html#germs" "Germ description — 1 item · 1 planned"
click n31 "../roadmap/local-tests/index.html#orbit-injectivity" "Rational orbit pullback — 1 item · 1 planned"
click n32 "../roadmap/character-classes/index.html#character-coproduct" "Character coproducts — 1 item · 1 planned"
click n33 "../roadmap/character-classes/index.html#orthogonality" "Real orthogonality — 1 item · 1 planned"
click n34 "../roadmap/character-classes/index.html#character-classes" "Character classes — 1 item · 1 planned"
click n35 "../roadmap/character-classes/index.html#class-covariance" "Covariance of character classes — 1 item · 1 planned"
click n36 "../roadmap/character-classes/index.html#class-homotopy" "Homotopy of character classes — 1 item · 1 planned"
click n37 "../roadmap/localization/index.html#open-cover" "Open cover dense inclusion — 1 item · 1 planned"
click n38 "../roadmap/localization/index.html#dense-doubling" "Dense doubling — 1 item · 1 ready to state"
click n39 "../roadmap/sphere-lattice/index.html#finite-chases" "Finite diagram chases — 1 item · 1 fully proved"
click n40 "../roadmap/sphere-lattice/index.html#bounded-comparison" "Bounded comparison — 1 item · 1 planned"
click n41 "../roadmap/sphere-lattice/index.html#sphere-rank" "Rational sphere calculation — 1 item · 1 planned"
click n42 "../roadmap/sphere-lattice/index.html#generic-signature" "Signature on a finite relation — 1 item · 1 planned"
click n43 "../roadmap/sphere-lattice/index.html#sphere-lattice" "Fixed sphere lattice — 1 item · 1 planned"
click n44 "../roadmap/local-tests/index.html#collapse" "Collapse and compactification — 1 item · 1 fully proved"
click n45 "../roadmap/local-tests/index.html#averaged-test" "Averaged degree-one test — 1 item · 1 ready to state"
click n46 "../roadmap/local-tests/index.html#finite-sheets" "Finite quotient sheets — 1 item · 1 fully proved"
click n47 "../roadmap/local-tests/index.html#odd-sphere-null" "Odd-sphere nullhomotopy — 1 item · 1 planned"
click n48 "../roadmap/local-tests/index.html#neighborhood-extension" "Homotopy extension — 1 item · 1 fully proved"
click n49 "../roadmap/local-tests/index.html#move-test" "Moving a test — 1 item · 1 planned"
click n50 "../roadmap/character-classes/index.html#equal-parts" "Equal parts — 1 item · 1 planned"
click n51 "../roadmap/sphere-lattice/index.html#degree-action" "Action of degree — 1 item · 1 planned"
click n52 "../roadmap/character-classes/index.html#sum-classes" "Sum of the character classes — 1 item · 1 planned"
click n53 "../roadmap/character-classes/index.html#contradiction" "Contradiction on the invariant chart — 1 item · 1 planned"
click n54 "../roadmap/local-tests/index.html" "Preparing local tests — 8 items · 3 fully proved · 1 ready to state · 4 planned"
click n55 "../roadmap/local-tests/index.html#chart-reduction" "Invariant chart subset — 1 item · 1 planned"
click n56 "../roadmap/localization/index.html" "Localization, germs, and dense subcategories — 7 items · 1 ready to state · 6 planned"
click n57 "../roadmap/localization/index.html#open-cover-bound" "Open-cover bound — 1 item · 1 planned"
click n58 "../roadmap/main-theorem/index.html" "Main theorems — 3 items · 3 planned"
click n59 "../roadmap/main-theorem/index.html#padic-exclusion" "$p$-adic exclusion — 1 item · 1 planned"
click n60 "../roadmap/main-theorem/index.html#hilbert-smith-conjecture" "Hilbert--Smith conjecture — 1 item · 1 planned"
click n61 "../roadmap/main-theorem/index.html#almost-periodic-flow" "Almost-periodic flow — 1 item · 1 planned"
click n62 "../roadmap/index.html" "HilbertSmith roadmap — 58 items · 6 fully proved · 15 ready to state · 37 planned"
click n63 "../roadmap/sheaf-categories/index.html" "Sheaf categories and homotopy invariance — 10 items · 1 ready to state · 9 planned"
click n64 "../roadmap/sheaf-categories/index.html#sign-conventions" "Sign conventions — 1 item · 1 planned"
click n65 "../roadmap/sphere-lattice/index.html" "A bounded lattice on the test sphere — 8 items · 1 fully proved · 7 planned"