Forcing more 𝖣𝖢 over the Chang model using the Thorn sequence

In the context of Z F + D C ZF+DC , we force D C κ DC_κ for relations on P ( κ ) P(κ ) for arbitrarily large κ > ℵ ω κ > _ω over the Chang model L ( O r d ω ) L(Ord^ω ) making some assumptions on the thorn sequence defined by Þ 0 = ω Þ_0=ω , Þ α + 1 Þα +1 as the least ordinal not a surjective image of Þ α ω Þ_α ^ω and Þ γ = sup α > γ Þ α Þ_γ = α >γÞ_α for limit γ γ . These assumptions are motivated from results about Θ Θ in the context of determinacy, and could be reasonable ways of thinking about the Chang model. Explicitly, we assume successor points λ λ on the thorn sequence are strongly regular—meaning regular and functions f : κ > κ → λ f:κ >κ→ λ are bounded whenever κ > λ κ >λ is on the thorn sequence—and justified—meaning P ( κ ω ) ∩ L ( O r d ω ) ⊆ L λ ( λ ω , X ) P(κ ^ω )∩ L(Ord^ω )⊆ Lλ(λ ^ω ,X) for some X ⊆ λ X⊆ λ for any κ > λ κ >λ on the thorn sequence. This allows us to use Cohen forcing and establish more dependent choice while preserving the thorn sequence and calculating it: Þ i = ℵ i + 1 Þ_i= ᵢ₊₁ for 0 > i > ω 0>i>ω after i i steps in the iteration.