A counterexample to Scottish Book Problem 155: formalization

This file formalizes the elementary metric core of paper1: the bent seed, its fixed short-scale property, its explicit contraction, and the passage from the fixed scale 1 / 2 to the closed-ball radius 1 / 4 used in the main theorem. The protected one-point extension and the transfinite construction are not asserted here.

def ScottishBook155.l1Dist (x y : ℝ × ℝ) : ℝ

The ℓ₁ distance on the real plane.

Equations

• ScottishBook155.l1Dist x y = |x.1 - y.1| + |x.2 - y.2|

noncomputable def ScottishBook155.bentMap (t : ℝ) : ℝ × ℝ

The bent line used as the seed of the construction in paper1.

Equations

• ScottishBook155.bentMap t = if t ≤ 0 then (t, 0) else if t ≤ 1 then (0, t) else (1 - t, 1)

def ScottishBook155.PreservesUpTo {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (r : ℝ) (f : X → Y) : Prop

Preservation of all distances up to a fixed scale.

Equations

• ScottishBook155.PreservesUpTo r f = ∀ ⦃x y : X⦄, dist x y ≤ r → dist (f x) (f y) = dist x y

def ScottishBook155.PreservesOnClosedBalls {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (r : ℝ) (f : X → Y) : Prop

Pairwise distance preservation on every closed ball of radius r.

Equations

• ScottishBook155.PreservesOnClosedBalls r f = ∀ (x p q : X), p ∈ Metric.closedBall x r → q ∈ Metric.closedBall x r → dist (f p) (f q) = dist p q

def ScottishBook155.IsCounterexampleAt {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] (r : ℝ) (f : X → Y) : Prop

The exact metric conclusion required of a counterexample to Problem 155, at a specified uniform closed-ball radius.

Equations

• ScottishBook155.IsCounterexampleAt r f = (Function.Bijective f ∧ ScottishBook155.PreservesOnClosedBalls r f ∧ ¬Isometry f)

theorem ScottishBook155.preservesOnClosedBalls_of_preservesUpTo_two_mul {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {r : ℝ} {f : X → Y} (h : PreservesUpTo (2 * r) f) : PreservesOnClosedBalls r f

A fixed scale of 2r implies preservation on every closed ball of radius r. This is the last metric deduction in the proof of the main theorem.

theorem ScottishBook155.isCounterexampleAt_one_quarter_of_short_scale {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {f : X → Y} (hbij : Function.Bijective f) (hshort : PreservesUpTo (1 / 2) f) {p q : X} (hcontracts : dist (f p) (f q) ≠ dist p q) : IsCounterexampleAt (1 / 4) f

The final logical step of the paper's main proof: a bijection preserving distances up to 1 / 2, but contracting one pair, is a Problem 155 counterexample on every closed ball of radius 1 / 4. This theorem is conditional; it does not construct the required spaces or map.

theorem ScottishBook155.bentMap_contraction : l1Dist (bentMap (-1)) (bentMap 2) = 1 ∧ |-1 - 2| = 3

The bent seed contracts the pair (-1, 2) from distance three to distance one.

theorem ScottishBook155.bentMap_injective : Function.Injective bentMap

The bent seed is injective.

theorem ScottishBook155.bentMap_short (s t : ℝ) (h : |s - t| ≤ 1 / 2) : l1Dist (bentMap s) (bentMap t) = |s - t|

The bent seed preserves the ℓ₁ distance whenever the parameter distance is at most 1 / 2.