Chapter 15: one round circle is shrunk by a global similarity (named zero parameter)
ProvedBookSixth.single_round_circle_shrinks_v5booksixthchapter15isotopyroundnesstopology
For a round circle C in R^3 there is a jointly continuous family K_t of ambient homeomorphisms of R^3, t in the half-open strip 0 <= t < 1, with jointly continuous inverse, fixing the identity at t = 0, such that every image K_t[C] is again a round circle. The motion is the global similarity K_t(x) = (1-t)x + tc where c is the centre of C; the scale 1-t is strictly positive for t < 1, so each K_t is a homeomorphism, and the images stay round by similarity_preserves_roundness. The zero parameter is named shrinkZero to keep the statement free of term-mode proofs.
Preamble
import Mathlib
import Definitions.Def_BookSixth
import Theorems.Thm_BookSixth_similarity_preserves_roundness
open scoped BigOperators
open BookSixth
noncomputable section
def shrinkZero : {t : ℝ // 0 ≤ t ∧ t < 1} := ⟨0, le_rfl, zero_lt_one⟩
Formal statement
theorem BookSixth.single_round_circle_shrinks_v5 (C : Set Space3) (hC : RoundCircle C) :
∃ K : {t : ℝ // 0 ≤ t ∧ t < 1} → Space3 ≃ₜ Space3,
(Continuous fun p : {t : ℝ // 0 ≤ t ∧ t < 1} × Space3 => K p.1 p.2) ∧
(Continuous fun p : {t : ℝ // 0 ≤ t ∧ t < 1} × Space3 => (K p.1).symm p.2) ∧
(∀ x, K shrinkZero x = x) ∧
(∀ t : {t : ℝ // 0 ≤ t ∧ t < 1}, RoundCircle ((K t) '' C)) := by sorrySource
Proofs from THE BOOK, Chapter 15 (Aigner-Ziegler), geometric motion of perfect circles; the single-circle shrinking motion, using the accepted global-similarity roundness lemma.