Foundation Circle Winding Path Homotopic Rel Const Of Loop Winding Zero

/-- A closed path in `S¹` with zero winding is homotopic rel endpoints to the
constant path at its basepoint.  The homotopy lifts the path to `ℝ`, uses zero
winding to identify the lift endpoints, and contracts the lifted path linearly
to its initial value before projecting back through the covering map. -/
theorem pathHomotopicRel_const_of_loop_winding_zero (γ : C(I, SphereOne))
    (hloop : γ 1 = γ 0) (hw : pathWinding γ = 0) :
    γ.HomotopicRel (ContinuousMap.const I (γ 0)) {0, 1} := by
  have hlift_end : pathLift γ 1 = pathLift γ 0 := by
    exact pathLift_endpoint_eq_of_winding_zero γ hw
  let Hmap : C(I × I, SphereOne) := {
    toFun p :=
      trigCirclePoint
        ((1 - ((p.1 : I) : ℝ)) * pathLift γ p.2 +
          ((p.1 : I) : ℝ) * pathLift γ 0)
    continuous_toFun := by
      exact continuous_trigCirclePoint.comp (by continuity)
  }
  let H : γ.Homotopy (ContinuousMap.const I (γ 0)) :=
    ContinuousMap.Homotopy.mk Hmap
      (by
        intro x
        change trigCirclePoint
            ((1 - (((0 : I) : I) : ℝ)) * pathLift γ x +
              (((0 : I) : I) : ℝ) * pathLift γ 0) = γ x
        simp
        exact congrFun (pathLift_lifts γ) x)
      (by
        intro x
        change trigCirclePoint
            ((1 - (((1 : I) : I) : ℝ)) * pathLift γ x +
              (((1 : I) : I) : ℝ) * pathLift γ 0) =
            (ContinuousMap.const I (γ 0)) x
        simp
        exact congrFun (pathLift_lifts γ) 0)
  refine ⟨ContinuousMap.HomotopyWith.mk H ?_⟩
  intro t x hx
  rcases hx with hx | hx
  · subst x
    change trigCirclePoint
        ((1 - ((t : I) : ℝ)) * pathLift γ 0 +
          ((t : I) : ℝ) * pathLift γ 0) = γ 0
    rw [← congrFun (pathLift_lifts γ) 0]
    congr 1
    ring
  · subst x
    change trigCirclePoint
        ((1 - ((t : I) : ℝ)) * pathLift γ 1 +
          ((t : I) : ℝ) * pathLift γ 0) = γ 1
    rw [hlift_end]
    rw [hloop]
    rw [← congrFun (pathLift_lifts γ) 0]
    congr 1
    ring

/-- A closed path has integer winding. -/
theorem pathWinding_loop_integral (γ : C(I, SphereOne)) (hloop : γ 1 = γ 0) :
    ∃ k : ℤ, pathWinding γ = (k : ℝ) := by
  obtain ⟨k, hk⟩ := pathDisplacement_loop_intMul γ hloop
  refine ⟨k, ?_⟩
  rw [pathWinding, hk]
  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
  field_simp [hpi]

/-- **The winding number of the fundamental loop is `1`.**  The winding invariant
is therefore a left inverse to the fundamental loop class on the nose: it sends
the canonical generator to `1`. -/
theorem pathWinding_fundamentalLoop : pathWinding fundamentalLoop = 1 := by
  rw [pathWinding, pathDisplacement_fundamentalLoop]
  have hpi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
  field_simp

/-- **Homotopy invariance of the displacement.**  If two paths are homotopic
relative to their endpoints, they have the same displacement.  This is the core
mechanism by which the winding invariant kills boundaries: the boundary loop of a
singular `2`-simplex is null-homotopic in the contractible standard simplex, so
its displacement vanishes. -/
theorem pathDisplacement_homotopic {γ δ : C(I, SphereOne)}
    (h : γ.HomotopicRel δ {0, 1}) : pathDisplacement γ = pathDisplacement δ := by
  have hend : γ 0 = δ 0 := homotopicRel_apply_zero h
  have he_γ : γ 0 = trigCirclePoint (pathLiftStart γ) := (pathLiftStart_spec γ).symm
  have he_δ : δ 0 = trigCirclePoint (pathLiftStart γ) := by rw [← hend]; exact he_γ
  have key : isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1
      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 :=
    isCoveringMap_trig.liftPath_apply_one_eq_of_homotopicRel h (pathLiftStart γ) he_γ he_δ
  have dγ : pathDisplacement γ
      = isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ 1 - pathLiftStart γ := by
    rw [pathDisplacement_eq γ (isCoveringMap_trig.liftPath γ (pathLiftStart γ) he_γ)
        (isCoveringMap_trig.liftPath_lifts γ (pathLiftStart γ) he_γ),
      isCoveringMap_trig.liftPath_zero γ (pathLiftStart γ) he_γ]
  have dδ : pathDisplacement δ
      = isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ 1 - pathLiftStart γ := by
    rw [pathDisplacement_eq δ (isCoveringMap_trig.liftPath δ (pathLiftStart γ) he_δ)
        (isCoveringMap_trig.liftPath_lifts δ (pathLiftStart γ) he_δ),
      isCoveringMap_trig.liftPath_zero δ (pathLiftStart γ) he_δ]
  rw [dγ, dδ, key]