Final assembly from a scheduled protected chain

This file isolates the last step of the transfinite argument. Once a coherent chain and its bookkeeping obligations have been constructed, regularity shows that the completed direct limits contain no points beyond the stage union, and the schedule gives surjectivity of the final map.

structure ScottishBook155.ScheduledProtectedChain : Type 1

The exact output required from the transfinite recursion.

• chain : ProtectedChain (1 / 2) 1

  The protected chain produced by the transfinite construction, with distance scale one half and projection bound one.

• enumerate (i a✝ : RecursionIndexZero) : (self.chain.stage i).target.carrier

  An enumeration of each stage target by recursion indices for the processing schedule.

• enumerate_surjective (i : RecursionIndexZero) : Function.Surjective (self.enumerate i)
• processed (i ξ : RecursionIndexZero) : ∃ (x : (self.chain.stage (bookkeepingReceivingStage (i, ξ))).source.carrier), (self.chain.stage (bookkeepingReceivingStage (i, ξ))).map x = (self.chain.targetSystem.embed i (bookkeepingReceivingStage (i, ξ)) ⋯) (self.enumerate i ξ)
• seedIndex : RecursionIndexZero

  The index at which the initial bent-map witness is embedded in the protected chain.

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

  The isometric embedding of the real-line seed into the scheduled source stage.

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

  The isometric embedding of the bent seed target into the scheduled target stage.

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

theorem ScottishBook155.ScheduledProtectedChain.sourceDirectedSystem (D : ScheduledProtectedChain) : DirectedSystem (fun (i : RecursionIndexZero) => (D.chain.stage i).source.carrier) fun (x1 x2 : RecursionIndexZero) (x3 : x1 ≤ x2) => ⇑(D.chain.sourceSystem.embed x1 x2 x3)

theorem ScottishBook155.ScheduledProtectedChain.targetDirectedSystem (D : ScheduledProtectedChain) : DirectedSystem (fun (i : RecursionIndexZero) => (D.chain.stage i).target.carrier) fun (x1 x2 : RecursionIndexZero) (x3 : x1 ≤ x2) => ⇑(D.chain.targetSystem.embed x1 x2 x3)

@[reducible, inline]

abbrev ScottishBook155.ScheduledProtectedChain.FinalSource (D : ScheduledProtectedChain) : Type

The Banach space obtained by completing the direct limit of the source stages.

Equations

• D.FinalSource = D.chain.LimitSource

@[reducible, inline]

abbrev ScottishBook155.ScheduledProtectedChain.FinalTarget (D : ScheduledProtectedChain) : Type

The Banach space obtained by completing the direct limit of the target stages.

Equations

• D.FinalTarget = D.chain.LimitTarget

noncomputable def ScottishBook155.ScheduledProtectedChain.finalMap (D : ScheduledProtectedChain) : D.FinalSource → D.FinalTarget

The map induced on completed limits by the compatible protected stage maps.

Equations

• D.finalMap = D.chain.completedMap

theorem ScottishBook155.ScheduledProtectedChain.finalMap_completedOf (D : ScheduledProtectedChain) (i : RecursionIndexZero) (x : (D.chain.stage i).source.carrier) : D.finalMap ((NormedDirectLimit.completedOf (fun (i : RecursionIndexZero) => (D.chain.stage i).source.carrier) D.chain.sourceSystem.embed i) x) = (NormedDirectLimit.completedOf (fun (i : RecursionIndexZero) => (D.chain.stage i).target.carrier) D.chain.targetSystem.embed i) ((D.chain.stage i).map x)

theorem ScottishBook155.ScheduledProtectedChain.commonSourceStage (D : ScheduledProtectedChain) (x y : D.FinalSource) : ∃ (i : RecursionIndexZero) (x₀ : (D.chain.stage i).source.carrier) (y₀ : (D.chain.stage i).source.carrier), (NormedDirectLimit.completedOf (fun (i : RecursionIndexZero) => (D.chain.stage i).source.carrier) D.chain.sourceSystem.embed i) x₀ = x ∧ (NormedDirectLimit.completedOf (fun (i : RecursionIndexZero) => (D.chain.stage i).source.carrier) D.chain.sourceSystem.embed i) y₀ = y

theorem ScottishBook155.ScheduledProtectedChain.finalMap_surjective (D : ScheduledProtectedChain) : Function.Surjective D.finalMap

noncomputable def ScottishBook155.ScheduledProtectedChain.toFinalAssemblyData (D : ScheduledProtectedChain) : FinalAssemblyData

A completed scheduled chain supplies exactly the data consumed by the final metric argument.

Equations

• One or more equations did not get rendered due to their size.

theorem ScottishBook155.ScheduledProtectedChain.claim14 (D : ScheduledProtectedChain) : Claim14