Formal target for canonical claim 14

This file fixes the exact existential statement before the transfinite construction is assembled. The witness packages two real Banach spaces and a bijection satisfying the paper's closed-ball conclusion while failing to be a global isometry.

structure ScottishBook155.RealBanachSpace : Type (u + 1)

A bundled real Banach space, used so that the source and target types of the final existential statement may themselves be chosen by the construction.

• carrier : Type u

  The underlying type of the bundled real Banach space.

• normedAddCommGroup : NormedAddCommGroup self.carrier
• normedSpace : NormedSpace ℝ self.carrier
• completeSpace : CompleteSpace self.carrier

@[instance_reducible]

instance ScottishBook155.instCoeSortRealBanachSpaceType : CoeSort RealBanachSpace (Type u)

Equations

• ScottishBook155.instCoeSortRealBanachSpaceType = { coe := ScottishBook155.RealBanachSpace.carrier }

def ScottishBook155.RealBanachSpace.ofType (X : Type u) [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] : RealBanachSpace

Bundle an already-instanced real Banach space.

Equations

• ScottishBook155.RealBanachSpace.ofType X = { carrier := X, normedAddCommGroup := inst✝², normedSpace := inst✝¹, completeSpace := inst✝ }

structure ScottishBook155.Claim14Witness : Type (u + 1)

Exact witness asserted by canonical claim 14.

• source : RealBanachSpace

  The real Banach space on which the counterexample map is defined.

• target : RealBanachSpace

  The real Banach space into which the counterexample map takes values.

• map : self.source.carrier → self.target.carrier

  The map witnessing the failure of global distance preservation at protected scale one quarter.

• isCounterexample : IsCounterexampleAt (1 / 4) self.map

def ScottishBook155.Claim14 : Prop

The exact formal proposition corresponding to canonical claim 14.

Equations

• ScottishBook155.Claim14 = Nonempty ScottishBook155.Claim14Witness

def ScottishBook155.claim14WitnessOfHalfScale (X Y : RealBanachSpace) (U : X.carrier → Y.carrier) (hbij : Function.Bijective U) (hshort : PreservesUpTo (1 / 2) U) {p q : X.carrier} (hcontracts : dist (U p) (U q) ≠ dist p q) : Claim14Witness

The stronger construction invariant used in the paper is sufficient for the exact claim-14 witness.

Equations

• ScottishBook155.claim14WitnessOfHalfScale X Y U hbij hshort hcontracts = { source := X, target := Y, map := U, isCounterexample := ⋯ }