Final-union assembly for claim 14

The transfinite recursion is separated from the last metric argument. The data below state exactly what the increasing union and bookkeeping must provide; the theorem proves that those data yield the canonical claim-14 witness.

structure ScottishBook155.FinalAssemblyData : Type (u + 1)

The output required from the transfinite recursion before the final metric deduction. Every pair of source points must lie in one common protected stage, and the initial bent stage must remain compatible with the final map.

• source : RealBanachSpace

  The final real Banach source assembled from the protected stages.

• target : RealBanachSpace

  The final real Banach target assembled from the protected stages.

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

  The final map whose restriction to each stage agrees with that stage map.

• stageIndex : Type u

  The type indexing the protected stages used in the final assembly.

• stage : self.stageIndex → ProtectedStage (1 / 2)

  The family of stages that preserve distances up to one half.

• sourceEmbedding (i : self.stageIndex) : (self.stage i).source.carrier →ₗᵢ[ℝ] self.source.carrier

  Linear isometric embeddings of the stage sources into the final source.

• targetEmbedding (i : self.stageIndex) : (self.stage i).target.carrier →ₗᵢ[ℝ] self.target.carrier

  Linear isometric embeddings of the stage targets into the final target.

• compatible (i : self.stageIndex) (x : (self.stage i).source.carrier) : self.map ((self.sourceEmbedding i) x) = (self.targetEmbedding i) ((self.stage i).map x)
• commonStage (x y : self.source.carrier) : ∃ (i : self.stageIndex) (x₀ : (self.stage i).source.carrier) (y₀ : (self.stage i).source.carrier), (self.sourceEmbedding i) x₀ = x ∧ (self.sourceEmbedding i) y₀ = y
• surjective : Function.Surjective self.map
• seedIndex : self.stageIndex

  The stage carrying the initial bent-map witness.

• seedSource : ℝ →ₗᵢ[ℝ] (self.stage self.seedIndex).source.carrier

  The isometric inclusion of the real-line source of the bent seed into its stage.

• seedTarget : OneSum ℝ →ₗᵢ[ℝ] (self.stage self.seedIndex).target.carrier

  The isometric inclusion of the one-sum target of the bent seed into its stage.

• seedCompatible (t : ℝ) : (self.stage self.seedIndex).map (self.seedSource t) = self.seedTarget (bentMapL1 t)

theorem ScottishBook155.FinalAssemblyData.injective (D : FinalAssemblyData) : Function.Injective D.map

theorem ScottishBook155.FinalAssemblyData.preservesUpTo (D : FinalAssemblyData) : PreservesUpTo (1 / 2) D.map

theorem ScottishBook155.FinalAssemblyData.contractsSeed (D : FinalAssemblyData) : dist (D.map ((D.sourceEmbedding D.seedIndex) (D.seedSource (-1)))) (D.map ((D.sourceEmbedding D.seedIndex) (D.seedSource 2))) ≠ dist ((D.sourceEmbedding D.seedIndex) (D.seedSource (-1))) ((D.sourceEmbedding D.seedIndex) (D.seedSource 2))

theorem ScottishBook155.claim14_of_finalAssembly (D : FinalAssemblyData) : Claim14

A completed transfinite assembly yields the exact canonical claim 14.