Coherent links in a protected-stage chain

The uniform recovery law is stable when one more active or idle successor is attached. This is the successor induction step used by the transfinite chain.

structure ScottishBook155.ProtectedLink {r : ℝ} (A S : ProtectedStage r) (L : ℝ) : Type u

A coherent embedding/retraction link from an earlier protected stage to a later one, with the uniform recovery band retained.

• sourceEmbedding : A.source.carrier →ₗᵢ[ℝ] S.source.carrier

  The isometric embedding from the earlier source space into the later source space.

• sourceProjection : S.source.carrier →L[ℝ] A.source.carrier

  The continuous linear retraction from the later source space to the earlier one.

• targetEmbedding : A.target.carrier →ₗᵢ[ℝ] S.target.carrier

  The isometric embedding from the earlier target space into the later target space.

• targetProjection : S.target.carrier →L[ℝ] A.target.carrier

  The continuous linear retraction from the later target space to the earlier one.

• compatible (x : A.source.carrier) : S.map (self.sourceEmbedding x) = self.targetEmbedding (A.map x)
• sourceRetracts (x : A.source.carrier) : self.sourceProjection (self.sourceEmbedding x) = x
• targetRetracts (y : A.target.carrier) : self.targetProjection (self.targetEmbedding y) = y
• sourceContractive (z : S.source.carrier) : ‖self.sourceProjection z‖ ≤ ‖z‖
• targetContractive (z : S.target.carrier) : ‖self.targetProjection z‖ ≤ ‖z‖
• recovers (z : S.source.carrier) : dist z (self.sourceEmbedding (self.sourceProjection z)) < L → self.targetProjection (S.map z) = A.map (self.sourceProjection z)

noncomputable def ScottishBook155.ProtectedLink.refl {r L : ℝ} (S : ProtectedStage r) : ProtectedLink S S L

The identity link.

Equations

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

noncomputable def ScottishBook155.ProtectedTransition.toLink {r L : ℝ} {S : ProtectedStage r} (T : ProtectedTransition S L) : ProtectedLink S T.next L

A single transition as a link.

Equations

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

noncomputable def ScottishBook155.ProtectedLink.extend {r L : ℝ} {A S : ProtectedStage r} (P : ProtectedLink A S L) (T : ProtectedTransition S L) : ProtectedLink A T.next L

Append one successor transition to an existing coherent link.

Equations

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