/-
SPDX-FileCopyrightText: 2026 Advameg, Inc.
SPDX-License-Identifier: Apache-2.0
-/

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.SpecialFunctions.Complex.Circle
import Mathlib.Topology.ContinuousMap.Basic
import Mathlib.Topology.Homotopy.Lifting
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Tactic

/-!
# No-Retraction Disk/Circle Seed

This file sets up the concrete two-dimensional no-retraction theorem: the
closed unit disk in the complex plane has no continuous retraction onto its
boundary unit circle.

The current file is a proof-facing bootstrap. It states the exact theorem,
checks the core geometric definitions, and proves small sanity lemmas that
future route work can consume.
-/

namespace AtlasKnownTheorems.NoRetractionDiskCircle

open Complex
open Topology

noncomputable section

/-- The closed unit disk in the complex plane. -/
abbrev ClosedDisk : Type :=
  {z : ℂ // ‖z‖ ≤ 1}

/-- The unit circle in the complex plane. -/
abbrev UnitCircle : Type :=
  {z : ℂ // ‖z‖ = 1}

/-- Interpret the local unit-circle subtype as mathlib's bundled circle. -/
def unitCircleToCircle (z : UnitCircle) : Circle :=
  ⟨z.1, mem_sphere_zero_iff_norm.2 z.2⟩

/-- Interpret mathlib's bundled circle as the local unit-circle subtype. -/
def circleToUnitCircle (z : Circle) : UnitCircle :=
  ⟨z.1, Circle.norm_coe z⟩

theorem continuous_unitCircleToCircle :
    Continuous unitCircleToCircle := by
  simpa [unitCircleToCircle] using
    (Continuous.subtype_mk
      (by continuity : Continuous fun z : UnitCircle => (z.1 : ℂ))
      (fun z : UnitCircle => mem_sphere_zero_iff_norm.2 z.2))

theorem continuous_circleToUnitCircle :
    Continuous circleToUnitCircle := by
  simpa [circleToUnitCircle] using
    (Continuous.subtype_mk
      (by continuity : Continuous fun z : Circle => (z.1 : ℂ))
      (fun z : Circle => Circle.norm_coe z))

@[simp]
theorem unitCircleToCircle_circleToUnitCircle (z : Circle) :
    unitCircleToCircle (circleToUnitCircle z) = z := by
  ext
  rfl

@[simp]
theorem circleToUnitCircle_unitCircleToCircle (z : UnitCircle) :
    circleToUnitCircle (unitCircleToCircle z) = z := by
  ext
  rfl

/-- The origin as a point of the closed disk. -/
def zeroInDisk : ClosedDisk :=
  ⟨0, by norm_num⟩

/-- The point `1` as a point of the unit circle. -/
def oneOnCircle : UnitCircle :=
  ⟨1, by norm_num⟩

/-- The point `-1` as a point of the unit circle. -/
def negOneOnCircle : UnitCircle :=
  ⟨-1, by norm_num⟩

/-- Include the boundary circle into the closed disk. -/
def boundaryInclusion (z : UnitCircle) : ClosedDisk :=
  ⟨z.1, by
    simp [z.2]⟩

/-- A continuous retraction from the disk to the circle, fixing the boundary. -/
def RetractionToCircle (r : ClosedDisk → UnitCircle) : Prop :=
  Continuous r ∧ ∀ z : UnitCircle, r (boundaryInclusion z) = z

/--
No-retraction theorem for the closed disk and boundary circle:
there is no continuous retraction from the disk onto its boundary.
-/
def NoRetractionDiskCircleStatement : Prop :=
  ¬ ∃ r : ClosedDisk → UnitCircle, RetractionToCircle r

theorem boundaryInclusion_norm (z : UnitCircle) :
    ‖(boundaryInclusion z).1‖ = 1 := by
  exact z.2

theorem boundaryInclusion_injective :
    Function.Injective boundaryInclusion := by
  intro z w h
  have hval : (boundaryInclusion z).1 = (boundaryInclusion w).1 :=
    congrArg (fun x : ClosedDisk => x.1) h
  ext
  simpa [boundaryInclusion] using hval

theorem continuous_boundaryInclusion :
    Continuous boundaryInclusion := by
  simpa [boundaryInclusion] using
    (Continuous.subtype_mk
      (by continuity : Continuous fun z : UnitCircle => (z.1 : ℂ))
      (fun z : UnitCircle => by
        simp [z.2]))

theorem oneOnCircle_ne_negOneOnCircle :
    oneOnCircle ≠ negOneOnCircle := by
  intro h
  have hval := congrArg Subtype.val h
  norm_num [oneOnCircle, negOneOnCircle] at hval

/-- Constant maps from the disk to the circle are never boundary retractions. -/
def constantCircleMap (z : UnitCircle) : ClosedDisk → UnitCircle :=
  fun _ => z

theorem constantCircleMap_not_retraction (z : UnitCircle) :
    ¬ RetractionToCircle (constantCircleMap z) := by
  intro hr
  have h_one : z = oneOnCircle := by
    simpa [constantCircleMap] using hr.2 oneOnCircle
  have h_neg : z = negOneOnCircle := by
    simpa [constantCircleMap] using hr.2 negOneOnCircle
  exact oneOnCircle_ne_negOneOnCircle (h_one.symm.trans h_neg)

/-- The radial contraction of a circle point into the closed disk. -/
def radialDiskPoint (t : unitInterval) (z : Circle) : ClosedDisk :=
  ⟨(t : ℝ) • (z : ℂ), by
    change ‖(((t : ℝ) : ℂ) * (z : ℂ))‖ ≤ 1
    rw [Complex.norm_mul, Complex.norm_of_nonneg t.2.1, Circle.norm_coe, mul_one]
    exact t.2.2⟩

theorem radialDiskPoint_zero (z : Circle) :
    radialDiskPoint 0 z = zeroInDisk := by
  ext
  simp [radialDiskPoint, zeroInDisk]

theorem radialDiskPoint_one (z : Circle) :
    radialDiskPoint 1 z = boundaryInclusion (circleToUnitCircle z) := by
  ext
  simp [radialDiskPoint, boundaryInclusion, circleToUnitCircle]

theorem continuous_radialDiskPoint :
    Continuous fun p : ↑unitInterval × Circle => radialDiskPoint p.1 p.2 := by
  simpa [radialDiskPoint] using
    (Continuous.subtype_mk
      (by
        continuity :
          Continuous fun p : ↑unitInterval × Circle => (p.1 : ℝ) • (p.2 : ℂ))
      (fun p : ↑unitInterval × Circle => by
        change ‖(((p.1 : ℝ) : ℂ) * (p.2 : ℂ))‖ ≤ 1
        rw [Complex.norm_mul, Complex.norm_of_nonneg p.1.2.1, Circle.norm_coe, mul_one]
        exact p.1.2.2))

def retractionCircleHomotopy (r : ClosedDisk → UnitCircle) (hr : Continuous r) :
    C(↑unitInterval × Circle, Circle) :=
  ⟨fun p => unitCircleToCircle (r (radialDiskPoint p.1 p.2)),
    continuous_unitCircleToCircle.comp (hr.comp continuous_radialDiskPoint)⟩

theorem retractionCircleHomotopy_zero
    (r : ClosedDisk → UnitCircle) (hr : Continuous r) (z : Circle) :
    retractionCircleHomotopy r hr (0, z) =
      unitCircleToCircle (r zeroInDisk) := by
  simp [retractionCircleHomotopy, radialDiskPoint_zero]

theorem retractionCircleHomotopy_one
    (r : ClosedDisk → UnitCircle) (hr : RetractionToCircle r) (z : Circle) :
    retractionCircleHomotopy r hr.1 (1, z) = z := by
  simp [retractionCircleHomotopy, radialDiskPoint_one, hr.2]

theorem no_circle_exp_section (F : C(Circle, ℝ))
    (hF : ∀ z : Circle, Circle.exp (F z) = z) : False := by
  let g : ℝ → ℝ := fun t => F (Circle.exp t)
  let h : ℝ → ℝ := fun t => g t - t
  have hg : Continuous g := by
    exact F.continuous.comp Circle.exp.continuous
  have hh : Continuous h := by
    dsimp [h]
    exact hg.sub continuous_id
  have h_exp : ∀ t : ℝ, Circle.exp (h t) = 1 := by
    intro t
    dsimp [h, g]
    rw [Circle.exp_sub, hF (Circle.exp t)]
    simp
  have hg_period : g (2 * Real.pi) = g 0 := by
    dsimp [g]
    rw [Circle.exp_two_pi, Circle.exp_zero]
  have h_endpoint : h (2 * Real.pi) = h 0 - 2 * Real.pi := by
    dsimp [h]
    rw [hg_period]
    ring
  obtain ⟨m, hm⟩ := Circle.exp_eq_one.mp (h_exp 0)
  have hmem : h 0 - Real.pi ∈ Set.Icc (h (2 * Real.pi)) (h 0) := by
    constructor
    · rw [h_endpoint]
      linarith [Real.pi_pos]
    · linarith [Real.pi_pos]
  obtain ⟨t, ht⟩ := intermediate_value_univ (2 * Real.pi) 0 hh hmem
  obtain ⟨n, hn⟩ := Circle.exp_eq_one.mp (h_exp t)
  have hpi_eq : Real.pi = ((m - n : ℤ) : ℝ) * (2 * Real.pi) := by
    rw [ht, hm] at hn
    calc
      Real.pi = (m : ℝ) * (2 * Real.pi) - (n : ℝ) * (2 * Real.pi) := by
        linarith
      _ = ((m - n : ℤ) : ℝ) * (2 * Real.pi) := by
        norm_num
        ring
  have htwo : (1 : ℝ) = ((m - n : ℤ) : ℝ) * 2 := by
    have hpi_ne : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
    apply (mul_right_inj' hpi_ne).mp
    calc
      Real.pi * 1 = Real.pi := by ring
      _ = Real.pi * (((m - n : ℤ) : ℝ) * 2) := by
        convert hpi_eq using 1
        ring
  have hint : (1 : ℤ) = (m - n) * 2 := by
    exact_mod_cast htwo
  omega

theorem circle_identity_not_nullhomotopic
    (H : C(↑unitInterval × Circle, Circle)) (c : Circle)
    (h0 : ∀ z : Circle, H (0, z) = c)
    (h1 : ∀ z : Circle, H (1, z) = z) : False := by
  let f0 : C(Circle, ℝ) := ContinuousMap.const Circle (Complex.arg c)
  have H0 : ∀ z : Circle, H (0, z) = Circle.exp (f0 z) := by
    intro z
    rw [h0 z]
    dsimp [f0]
    rw [Circle.exp_arg]
  let L : C(↑unitInterval × Circle, ℝ) :=
    Circle.isCoveringMap_exp.liftHomotopy H f0 H0
  let F : C(Circle, ℝ) :=
    ⟨fun z => L (1, z), by
      exact L.continuous.comp (continuous_const.prodMk continuous_id)⟩
  have hF : ∀ z : Circle, Circle.exp (F z) = z := by
    intro z
    have hL := congr_fun (Circle.isCoveringMap_exp.liftHomotopy_lifts H f0 H0) (1, z)
    dsimp [F] at hL ⊢
    simpa [h1 z] using hL
  exact no_circle_exp_section F hF

/-- Checked statement wrapper for the minimum theorem. -/
theorem noRetractionDiskCircle_statement :
    NoRetractionDiskCircleStatement ↔ NoRetractionDiskCircleStatement := by
  rfl

theorem noRetractionDiskCircle :
    NoRetractionDiskCircleStatement := by
  rintro ⟨r, hr⟩
  exact circle_identity_not_nullhomotopic
    (retractionCircleHomotopy r hr.1)
    (unitCircleToCircle (r zeroInDisk))
    (retractionCircleHomotopy_zero r hr.1)
    (retractionCircleHomotopy_one r hr)

end

end AtlasKnownTheorems.NoRetractionDiskCircle