OAI/Topology/ArtinGroups/ParabolicIntersections/SphericalNoChain.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Bounded total height forbids infinitely many complete positive passes.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveWord_generator_exterior line 14
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.classPositiveTwist_outside_placement line 24
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveWord_outside_placement line 43
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.positiveWord_allTests_reflect line 55
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.generatorArray_positive_iff line 74
  6. theorem OAI.HarmonicArtin.ParabolicIntersections.no_bounded_complete_positive_chain line 89

    Source documentation

    Proposition 7.4 for actual positive vertex operations. The only published input is the abstract mesh-algebra path identity.

    theorem no_bounded_complete_positive_chain (hn : ∀ a, Q.source a ≠ Q.target a)
    (U : Set V) (hmesh : MeshNilpotent Q U)
    (x : ℕ → FiniteHomotopyClass Q (K := ℂ)) (w : ℕ → List V)
…

    Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent