Unconditional transfinite construction for Claim 14

This file builds the coherent protected chain by well-founded recursion on the fixed regular recursion cardinal. Successor stages process the bookkeeping schedule, limit stages glue and complete the earlier prefixes, and the resulting scheduled chain supplies the unconditional witness for Claim14.

@[simp]

theorem ScottishBook155.successorSegmentWithTop_apply_top (j : RecursionIndexZero) : (successorSegmentWithTop j ⋯) ⟨Order.succ j, ⋯⟩ = ⊤

theorem ScottishBook155.ProtectedStage.map_castSourcePoint {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : A.source.carrier) : B.map (castSourcePoint h x) = castTargetPoint h (A.map x)

noncomputable def ScottishBook155.ProtectedStage.castSourceLinearIsometry {r : ℝ} {A B : ProtectedStage r} (h : A = B) : A.source.carrier →ₗᵢ[ℝ] B.source.carrier

The linear isometry transporting source points along equality of protected stages.

Equations

• ScottishBook155.ProtectedStage.castSourceLinearIsometry h = h ▸ LinearIsometry.id

noncomputable def ScottishBook155.ProtectedStage.castTargetLinearIsometry {r : ℝ} {A B : ProtectedStage r} (h : A = B) : A.target.carrier →ₗᵢ[ℝ] B.target.carrier

The linear isometry transporting target points along equality of protected stages.

Equations

• ScottishBook155.ProtectedStage.castTargetLinearIsometry h = h ▸ LinearIsometry.id

theorem ScottishBook155.ProtectedStage.castSourceLinearIsometry_apply {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : A.source.carrier) : (castSourceLinearIsometry h) x = castSourcePoint h x

theorem ScottishBook155.ProtectedStage.castTargetLinearIsometry_apply {r : ℝ} {A B : ProtectedStage r} (h : A = B) (x : A.target.carrier) : (castTargetLinearIsometry h) x = castTargetPoint h x

theorem ScottishBook155.ProtectedStage.cast_bentSeed_compatible (A : ProtectedStage (1 / 2)) (h : A = bentSeedStage) (t : ℝ) : A.map ((castSourceLinearIsometry ⋯) t) = (castTargetLinearIsometry ⋯) (bentMapL1 t)

theorem ScottishBook155.ProtectedChain.reindex_target_embed_of_eq {ι κ : Type} [LinearOrder ι] [LinearOrder κ] {r L : ℝ} (C : ProtectedChain r L) (e : κ ↪o ι) (a b : κ) (hab : a ≤ b) (a' b' : ι) (ha : e a = a') (hb : e b = b') (hab' : a' ≤ b') (x : ((C.reindex e).stage a).target.carrier) : ProtectedStage.castTargetPoint ⋯ (((C.reindex e).targetSystem.embed a b hab) x) = (C.targetSystem.embed a' b' hab') (ProtectedStage.castTargetPoint ⋯ x)

noncomputable def ScottishBook155.ProtectedPrefix.pointOfScheduledRequirement {j : RecursionIndexZero} (P : ProtectedPrefix j) (q : { p : RecursionIndexZero × RecursionIndexZero // bookkeepingSchedule p = j }) : P.topStage.target.carrier

Embed the point named by a requirement whose scheduled transition is j into the top target of a prefix ending at j.

Equations

• P.pointOfScheduledRequirement q = (P.chain.targetSystem.embed ⟨(↑q).1, ⋯⟩ ⟨j, ⋯⟩ ⋯) (P.enumerate ⟨(↑q).1, ⋯⟩ (↑q).2)

noncomputable def ScottishBook155.ProtectedPrefix.scheduledPoint (j : RecursionIndexZero) (P : ProtectedPrefix j) : P.topStage.target.carrier

The target point processed at the transition out of j.

Equations

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

theorem ScottishBook155.ProtectedPrefix.scheduledPoint_of_schedule (p : RecursionIndexZero × RecursionIndexZero) (P : ProtectedPrefix (bookkeepingSchedule p)) : scheduledPoint (bookkeepingSchedule p) P = (P.chain.targetSystem.embed ⟨p.1, ⋯⟩ ⟨bookkeepingSchedule p, ⋯⟩ ⋯) (P.enumerate ⟨p.1, ⋯⟩ p.2)

theorem ScottishBook155.ProtectedPrefix.linkOfRestriction_targetEmbedding_enumerate {i j : RecursionIndexZero} (Pi : ProtectedPrefix i) (Pj : ProtectedPrefix j) (hij : i ≤ j) (hchain : (Pj.restriction hij).chain = Pi.chain) (ξ : RecursionIndexZero) : (Pi.linkOfRestriction Pj hij hchain).targetEmbedding (Pi.enumerate ⟨i, ⋯⟩ ξ) = (Pj.chain.targetSystem.embed ⟨i, hij⟩ ⟨j, ⋯⟩ hij) (Pj.enumerate ⟨i, hij⟩ ξ)

theorem ScottishBook155.ProtectedPrefix.linkOfRestriction_targetEmbedding_transportTarget {i j : RecursionIndexZero} (Pi : ProtectedPrefix i) (Pj Qj : ProtectedPrefix j) (hij : i ≤ j) (hPj : (Pj.restriction hij).chain = Pi.chain) (hQj : (Qj.restriction hij).chain = Pi.chain) (h : Pj = Qj) (x : Pi.topStage.target.carrier) : ProtectedStage.castTargetPoint ⋯ ((Pi.linkOfRestriction Pj hij hPj).targetEmbedding x) = (Pi.linkOfRestriction Qj hij hQj).targetEmbedding x

theorem ScottishBook155.ProtectedPrefix.successor_topStage {j : RecursionIndexZero} (P : ProtectedPrefix j) (y : P.topStage.target.carrier) : (P.successor y).topStage = (scheduledSuccessor P.topStage y).next

theorem ScottishBook155.ProtectedPrefix.successor_link_targetEmbedding {j : RecursionIndexZero} (P : ProtectedPrefix j) (y : P.topStage.target.carrier) : (P.linkOfRestriction (P.successor y) ⋯ ⋯).targetEmbedding y = ProtectedStage.castTargetPoint ⋯ ((scheduledSuccessor P.topStage y).targetEmbedding y)

theorem ScottishBook155.ProtectedPrefix.successor_link_hits {j : RecursionIndexZero} (P : ProtectedPrefix j) (y : P.topStage.target.carrier) : ∃ (x : (P.successor y).topStage.source.carrier), (P.successor y).topStage.map x = (P.linkOfRestriction (P.successor y) ⋯ ⋯).targetEmbedding y

noncomputable def ScottishBook155.protectedPrefixFunctor : CategoryTheory.Functor RecursionIndexZeroᵒᵖ (Type 1)

The inverse system of protected prefixes under restriction.

Equations

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

noncomputable def ScottishBook155.compatiblePrefixFamilyOfSection (j : RecursionIndexZero) (x : ↑(⋯.functor.op.comp protectedPrefixFunctor).sections) : CompatiblePrefixFamily j

A compatible family of prefixes extracted from a section below a limit index.

Equations

• ScottishBook155.compatiblePrefixFamilyOfSection j x = { item := fun (i : ↑(Set.Iio j)) => ↑x (Opposite.op i), coherent := ⋯ }

theorem ScottishBook155.CompatiblePrefixFamily.openChain_source_mk_le {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i : ↑(Set.Iio j)) : Cardinal.mk (F.openChain.stage i).source.carrier ≤ stageCardinal

theorem ScottishBook155.CompatiblePrefixFamily.openChain_target_mk_le {j : RecursionIndexZero} (F : CompatiblePrefixFamily j) (i : ↑(Set.Iio j)) : Cardinal.mk (F.openChain.stage i).target.carrier ≤ stageCardinal

noncomputable def ScottishBook155.limitPrefix (j : RecursionIndexZero) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp protectedPrefixFunctor).sections) : ProtectedPrefix j

The completed prefix attached to a compatible section at a limit index.

Equations

• ScottishBook155.limitPrefix j hj x = ScottishBook155.ProtectedPrefix.ofLimit j hj (ScottishBook155.compatiblePrefixFamilyOfSection j x).openChain ⋯ ⋯

theorem ScottishBook155.limitPrefix_restriction (j : RecursionIndexZero) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp protectedPrefixFunctor).sections) (i : RecursionIndexZero) (hi : i < j) : (limitPrefix j hj x).restriction ⋯ = ↑x (Opposite.op ⟨i, hi⟩)

noncomputable def ScottishBook155.protectedPrefixInductionData : protectedPrefixFunctor.WellOrderInductionData

Successor and limit lifts for the inverse system of bounded prefixes.

Equations

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

noncomputable def ScottishBook155.seedPrefix : ProtectedPrefix ⊥

The bent seed prefix at the least recursion index.

Equations

• ScottishBook155.seedPrefix = ScottishBook155.ProtectedPrefix.ofMin ⊥ ScottishBook155.seedPrefix._proof_1

noncomputable def ScottishBook155.protectedPrefixSection : ↑protectedPrefixFunctor.sections

The coherent transfinite section selected from the successor and limit clauses.

Equations

• ScottishBook155.protectedPrefixSection = ScottishBook155.protectedPrefixInductionData.sectionsMk ScottishBook155.seedPrefix

noncomputable def ScottishBook155.canonicalPrefix (j : RecursionIndexZero) : ProtectedPrefix j

The canonical bounded prefix ending at j.

Equations

• ScottishBook155.canonicalPrefix j = ↑ScottishBook155.protectedPrefixSection (Opposite.op j)

theorem ScottishBook155.canonicalPrefix_restriction {i j : RecursionIndexZero} (hij : i ≤ j) : (canonicalPrefix j).restriction hij = canonicalPrefix i

theorem ScottishBook155.canonicalPrefix_bot : canonicalPrefix ⊥ = seedPrefix

theorem ScottishBook155.canonicalPrefix_succ (j : RecursionIndexZero) : canonicalPrefix (Order.succ j) = (canonicalPrefix j).successor (ProtectedPrefix.scheduledPoint j (canonicalPrefix j))

structure ScottishBook155.CompatiblePrefixSequence : Type 1

A coherent family of closed prefixes over the whole recursion order.

• item (j : RecursionIndexZero) : ProtectedPrefix j

  The closed protected prefix at each index of the complete recursion order.

• coherent (_i _j : RecursionIndexZero) (hij : _i ≤ _j) : ((self.item _j).restriction hij).chain = (self.item _i).chain

noncomputable def ScottishBook155.canonicalPrefixSequence : CompatiblePrefixSequence

The canonical transfinite section as a coherent prefix sequence.

Equations

• ScottishBook155.canonicalPrefixSequence = { item := ScottishBook155.canonicalPrefix, coherent := ScottishBook155.canonicalPrefixSequence._proof_1 }

noncomputable def ScottishBook155.CompatiblePrefixSequence.below (G : CompatiblePrefixSequence) (j : RecursionIndexZero) : CompatiblePrefixFamily j

Restrict a global prefix sequence to indices below j.

Equations

• G.below j = { item := fun (i : ↑(Set.Iio j)) => G.item ↑i, coherent := ⋯ }

@[reducible, inline]

abbrev ScottishBook155.CompatiblePrefixSequence.stage (G : CompatiblePrefixSequence) (i : RecursionIndexZero) : ProtectedStage (1 / 2)

The top protected stage of the prefix at the specified recursion index.

Equations

• G.stage i = (G.item i).topStage

noncomputable def ScottishBook155.CompatiblePrefixSequence.link (G : CompatiblePrefixSequence) (i j : RecursionIndexZero) (hij : i ≤ j) : ProtectedLink (G.stage i) (G.stage j) 1

The protected link between two stages, obtained from coherence of their closed prefixes.

Equations

• G.link i j hij = (G.item i).linkOfRestriction (G.item j) hij ⋯

theorem ScottishBook155.CompatiblePrefixSequence.below_link (G : CompatiblePrefixSequence) (j : RecursionIndexZero) (i k : ↑(Set.Iio j)) (hik : i ≤ k) : (G.below j).link i k hik = G.link (↑i) (↑k) hik

theorem ScottishBook155.CompatiblePrefixSequence.sourceEmbedding_refl (G : CompatiblePrefixSequence) (i : RecursionIndexZero) (x : (G.stage i).source.carrier) : (G.link i i ⋯).sourceEmbedding x = x

theorem ScottishBook155.CompatiblePrefixSequence.targetEmbedding_refl (G : CompatiblePrefixSequence) (i : RecursionIndexZero) (x : (G.stage i).target.carrier) : (G.link i i ⋯).targetEmbedding x = x

theorem ScottishBook155.CompatiblePrefixSequence.sourceEmbedding_trans (G : CompatiblePrefixSequence) (i k m : RecursionIndexZero) (hik : i ≤ k) (hkm : k ≤ m) (x : (G.stage i).source.carrier) : (G.link k m hkm).sourceEmbedding ((G.link i k hik).sourceEmbedding x) = (G.link i m ⋯).sourceEmbedding x

theorem ScottishBook155.CompatiblePrefixSequence.targetEmbedding_trans (G : CompatiblePrefixSequence) (i k m : RecursionIndexZero) (hik : i ≤ k) (hkm : k ≤ m) (x : (G.stage i).target.carrier) : (G.link k m hkm).targetEmbedding ((G.link i k hik).targetEmbedding x) = (G.link i m ⋯).targetEmbedding x

theorem ScottishBook155.CompatiblePrefixSequence.sourceProjection_embed (G : CompatiblePrefixSequence) (a i j : RecursionIndexZero) (hai : a ≤ i) (hij : i ≤ j) (x : (G.stage i).source.carrier) : (G.link a j ⋯).sourceProjection ((G.link i j hij).sourceEmbedding x) = (G.link a i hai).sourceProjection x

theorem ScottishBook155.CompatiblePrefixSequence.targetProjection_embed (G : CompatiblePrefixSequence) (a i j : RecursionIndexZero) (hai : a ≤ i) (hij : i ≤ j) (x : (G.stage i).target.carrier) : (G.link a j ⋯).targetProjection ((G.link i j hij).targetEmbedding x) = (G.link a i hai).targetProjection x

noncomputable def ScottishBook155.CompatiblePrefixSequence.toProtectedChain (G : CompatiblePrefixSequence) : ProtectedChain (1 / 2) 1

Glue a coherent sequence of closed prefixes into one protected chain on the whole recursion order.

Equations

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

noncomputable def ScottishBook155.canonicalProtectedChain : ProtectedChain (1 / 2) 1

The global coherent protected chain produced by the transfinite section.

Equations

• ScottishBook155.canonicalProtectedChain = ScottishBook155.canonicalPrefixSequence.toProtectedChain

noncomputable def ScottishBook155.canonicalEnumerate (i a✝ : RecursionIndexZero) : (canonicalProtectedChain.stage i).target.carrier

The fixed enumeration of the target at each global stage.

Equations

• ScottishBook155.canonicalEnumerate i = (ScottishBook155.canonicalPrefix i).enumerate ⟨i, ⋯⟩

theorem ScottishBook155.canonicalEnumerate_surjective (i : RecursionIndexZero) : Function.Surjective (canonicalEnumerate i)

theorem ScottishBook155.canonical_stage_bot : canonicalProtectedChain.stage ⊥ = bentSeedStage

theorem ScottishBook155.canonical_scheduledPoint_eq_link (p : RecursionIndexZero × RecursionIndexZero) : ProtectedPrefix.scheduledPoint (bookkeepingSchedule p) (canonicalPrefix (bookkeepingSchedule p)) = (canonicalPrefixSequence.link p.1 (bookkeepingSchedule p) ⋯).targetEmbedding (canonicalEnumerate p.1 p.2)

theorem ScottishBook155.canonical_processed (i ξ : RecursionIndexZero) : ∃ (x : (canonicalProtectedChain.stage (bookkeepingReceivingStage (i, ξ))).source.carrier), (canonicalProtectedChain.stage (bookkeepingReceivingStage (i, ξ))).map x = (canonicalProtectedChain.targetSystem.embed i (bookkeepingReceivingStage (i, ξ)) ⋯) (canonicalEnumerate i ξ)

noncomputable def ScottishBook155.canonicalScheduledProtectedChain : ScheduledProtectedChain

The unconditional scheduled chain required by the final direct-limit assembly.

Equations

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

theorem ScottishBook155.claim14 : Claim14

Canonical claim 14, with the transfinite recursion discharged.