Transfinite Construction

The ordinal-indexed iteration that builds an ascending chain of N-subrings, ensuring at each successor step that one more prime is caught and one more element of T/M^2 is covered.

Jensen, "Completions of UFDs with semi-local formal fibers", 2006, Theorem 2.2.

Ordinal-indexed transfinite construction

Replace the Zorn approach (which needs hk_countable) with ordinal recursion over V = {nonzero primes of T} × T/M². This eliminates the countability assumption, using ℵ₀ < #T and #R < #T propagation instead.

Architecture

• Index set: V = {q : Ideal T // q.IsPrime ∧ q ≠ ⊥} × (T ⧸ M²)
• Ordinal: κ = Cardinal.ord (#V)
• Base: R₀ = initial_NSubring (from NSubring.lean), closed up
• Successor at α: combined_step_card R(α) (q_α, ℓ_α)
• Limit at λ: transfinite union of R(β) for β < λ
• Result: A = R(κ) satisfies surjectivity, closedness, prime coverage

Helper lemma: build an NSubring from a union of predecessors

Extracted from the main transfinite construction to stay within the default heartbeat budget. Given a family of NSubrings indexed by predecessors of α, builds the union as an NSubring with cardinal bounds and prime preservation.

theorem transfinite_construction {T : Type u} [CommRing T] [IsLocalRing T] [IsNoetherianRing T] [IsDomain T] [IsAdicComplete (IsLocalRing.maximalIdeal T) T] (hdepth : ∃ (a : T) (b : T), a ∈ IsLocalRing.maximalIdeal T ∧ b ∈ IsLocalRing.maximalIdeal T ∧ RingTheory.Sequence.IsRegular T [a, b]) (hcard : Cardinal.mk T = Cardinal.mk (IsLocalRing.ResidueField T)) (hchar : ∀ (n : ℤ), n ≠ 0 → (algebraMap ℤ T) n ≠ 0) (hM_not_assoc : ∀ (r : T), r ≠ 0 → IsLocalRing.maximalIdeal T ∉ associatedPrimes T (T ⧸ Ideal.span {r})) (hAss_ht : ∀ (r : T), r ≠ 0 → ∀ P ∈ associatedPrimes T (T ⧸ Ideal.span {r}), P.height ≤ 1) (hT_aleph0 : Cardinal.aleph0 < Cardinal.mk T) : ∃ (A : NSubring T), (Function.Surjective fun (r : ↥A.carrier) => (Ideal.Quotient.mk (IsLocalRing.maximalIdeal T ^ 2)) ↑r) ∧ (∀ (I : Ideal ↥A.carrier), I.FG → ∀ (c : ↥A.carrier), ↑c ∈ Ideal.map A.carrier.subtype I → c ∈ I) ∧ ∀ (q : Ideal T), q.IsPrime → q ≠ ⊥ → ∃ (t : ↥A.carrier), ↑t ∈ q ∧ ↑t ≠ 0

The transfinite construction via ordinal recursion: iterate combined_step over all (prime, residue) pairs indexed by ordinals, building an N-subring A of T that is surjective onto T/M², has every nonzero prime of T meeting A nontrivially, and satisfies the closedness condition IT ∩ A = I.

This replaces the Zorn-based transfinite_construction_zorn which required hk_countable : #k ≤ ℵ₀ (false for our T). Instead takes hT_aleph0 : ℵ₀ < #T and propagates cardinal bounds #R < #T through the chain.