Left-piece range of the successor punctured-plane cover lies in the standard-generator range

Proved

BraidsLinksMCG.puncturedPlane_succ_left_piece_range_v1

by junyihjy · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

For the van Kampen cover of the (n+1)-times punctured plane, assuming the induction hypothesis that the n-times punctured-plane group is free on the standard generators, if the left piece A(false) is the union of the left half-plane {z : re z < n+1}, the upper half-plane, and the right tail {z : re z > n + 3/2} containing the standard basepoint, then the range of the inclusion-induced map on fundamental groups of the left piece is contained in the range of the map from the free group induced by the standard generators of the punctured-plane group.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_BraidsLinksMCG_StandardLoops
import Definitions.Def_Hatcher_VanKampen

Formal statement

namespace BraidsLinksMCG

theorem puncturedPlane_succ_left_piece_range_v1 (n : ℕ)
    (ih : ∃ e : PuncturedPlaneGroup n ≃* FreeGroup (Fin n),
      ∀ j : Fin n, e (standardGen n j) = FreeGroup.of j)
    (A : Bool → Set (PuncturedPlane (n + 1)))
    (hx : ∀ i, basePunctured (n + 1) ∈ A i)
    (hfalse : A Bool.false =
      {z : PuncturedPlane (n + 1) | z.1.re < ((n : ℕ) + 1 : ℝ)} ∪
      {z : PuncturedPlane (n + 1) | 0 < z.1.im} ∪
      {z : PuncturedPlane (n + 1) | ((n : ℝ) + 3 / 2) < z.1.re}) :
    (Hatcher.inclHom A (basePunctured (n + 1)) hx Bool.false).range ≤
      (FreeGroup.lift (standardGen (n + 1))).range := by
  sorry

end BraidsLinksMCG

Source

proofs_vankampen/cover_step_v1_BLOCKER.md section 5 (stall-takeover re-decomposition of puncturedPlane_standardGen_vankampen_cover_step_v1)

View graph