Cardinal-controlled protected prefixes

structure ScottishBook155.ProtectedPrefix (j : RecursionIndexZero) : Type 1

A coherent chain on a closed initial segment, with the cardinal bounds needed to enumerate every target stage.

• chain : ProtectedChain (1 / 2) 1

  The protected chain on the closed initial segment through the prefix index.

• source_mk_le (i : ↑(Set.Iic j)) : Cardinal.mk (self.chain.stage i).source.carrier ≤ stageCardinal
• target_mk_le (i : ↑(Set.Iic j)) : Cardinal.mk (self.chain.stage i).target.carrier ≤ stageCardinal

theorem ScottishBook155.ProtectedPrefix.ext {j : RecursionIndexZero} {P Q : ProtectedPrefix j} (h : P.chain = Q.chain) : P = Q

A bounded protected prefix is determined by its coherent chain; the two cardinal bounds are propositions.

@[reducible, inline]

abbrev ScottishBook155.ProtectedPrefix.topStage {j : RecursionIndexZero} (P : ProtectedPrefix j) : ProtectedStage (1 / 2)

The top stage of a prefix.

Equations

• P.topStage = P.chain.stage ⟨j, ⋯⟩

noncomputable def ScottishBook155.ProtectedPrefix.enumerate {j : RecursionIndexZero} (P : ProtectedPrefix j) (i : ↑(Set.Iic j)) : RecursionIndexZero → (P.chain.stage i).target.carrier

The canonical recursion-indexed enumeration at a stage of a prefix.

Equations

• P.enumerate i = ScottishBook155.stageEnumeration ⋯

theorem ScottishBook155.ProtectedPrefix.enumerate_surjective {j : RecursionIndexZero} (P : ProtectedPrefix j) (i : ↑(Set.Iic j)) : Function.Surjective (P.enumerate i)

noncomputable def ScottishBook155.ProtectedPrefix.ofMin (j : RecursionIndexZero) (_hj : IsMin j) : ProtectedPrefix j

The bent seed as the bounded prefix at the minimum recursion index.

Equations

• ScottishBook155.ProtectedPrefix.ofMin j _hj = { chain := ScottishBook155.constantProtectedChain ScottishBook155.bentSeedStage, source_mk_le := ⋯, target_mk_le := ⋯ }

noncomputable def ScottishBook155.ProtectedPrefix.successor {j : RecursionIndexZero} (P : ProtectedPrefix j) (y : P.topStage.target.carrier) : ProtectedPrefix (Order.succ j)

Append one scheduled successor to a bounded prefix.

Equations

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

noncomputable def ScottishBook155.ProtectedPrefix.ofLimit (j : RecursionIndexZero) (hj : Order.IsSuccLimit j) (C : ProtectedChain (1 / 2) 1) (hSource : ∀ (i : ↑(Set.Iio j)), Cardinal.mk (C.stage i).source.carrier ≤ stageCardinal) (hTarget : ∀ (i : ↑(Set.Iio j)), Cardinal.mk (C.stage i).target.carrier ≤ stageCardinal) : ProtectedPrefix j

Append the completed direct limit at a nonzero limit index.

Equations

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

noncomputable def ScottishBook155.ProtectedPrefix.restriction {j : RecursionIndexZero} (P : ProtectedPrefix j) {i : RecursionIndexZero} (hij : i ≤ j) : ProtectedPrefix i

Restrict a bounded prefix to an earlier closed initial segment.

Equations

• P.restriction hij = { chain := P.chain.reindex { toFun := fun (k : ↑(Set.Iic i)) => ⟨↑k, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }, source_mk_le := ⋯, target_mk_le := ⋯ }

@[simp]

theorem ScottishBook155.ProtectedPrefix.restriction_refl {j : RecursionIndexZero} (P : ProtectedPrefix j) : P.restriction ⋯ = P

theorem ScottishBook155.ProtectedPrefix.restriction_trans {j a i : RecursionIndexZero} (P : ProtectedPrefix j) (hai : a ≤ i) (hij : i ≤ j) : (P.restriction hij).restriction hai = P.restriction ⋯

theorem ScottishBook155.ProtectedPrefix.successor_restriction {j : RecursionIndexZero} (P : ProtectedPrefix j) (y : P.topStage.target.carrier) : (P.successor y).restriction ⋯ = P

The new successor prefix restricts to the prefix from which it was constructed.