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

Proved

BraidsLinksMCG.puncturedPlane_succ_right_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 by a left piece and a right piece, if the right piece A(true) is exactly the once-punctured right half-plane {z : re z > n + 1/2} containing the standard basepoint, then the range of the inclusion-induced map on fundamental groups of the right 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_right_piece_range_v1 (n : ℕ)
    (A : Bool → Set (PuncturedPlane (n + 1)))
    (hx : ∀ i, basePunctured (n + 1) ∈ A i)
    (htrue : A Bool.true =
      {z : PuncturedPlane (n + 1) | ((n : ℕ) : ℝ) + 1 / 2 < z.1.re}) :
    (Hatcher.inclHom A (basePunctured (n + 1)) hx Bool.true).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