Arbitrary-target stabilization (issue #17 chunk 5.1) #

The kernel of the Scott completion, and the point of contact between #13 and #17: the existing stabilization theory (StabilizesCompletely, from the proved countable refinement hypothesis) upgrades BFEquiv α → BFEquiv (succ α) only against COUNTABLE targets. This file extends it to ARBITRARY targets using the fragment Löwenheim–Skolem machinery:

for each required extension, take a countable A-elementary substructure of the arbitrary target containing the current tuple (and, in the back direction, the requested new element), where the controlling fragment contains the CLOSED level-α Scott formulas of all finite tuples of the countable source (scottSeed — countably many, since the source is countable; closing is relabel Sum.inr, with realize_relabel_sumInr as the bridge). A-elementarity transfers Scott-formula realization between the target and the substructure, where the countable-target stabilization supplies the witness.

The generic extension-family bridge (bfEquiv_all_of_extensionFamily, the two-structure form of the audited thin bridge) then upgrades stabilized BFEquiv α to EVERY ordinal (bfEquiv_all_of_stabilizesCompletely_arbitrary).

The generic extension-family bridge (two arbitrary structures) #

source

theorem FirstOrder.Language.bfEquiv_all_of_extensionFamily {L : Language} {M' N' : Type w} [L.Structure M'] [L.Structure N'] (R : (n : ℕ) → (Fin n → M') → (Fin n → N') → Prop) (hzero : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → SameAtomicType a b) (hforth : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → ∀ (a' : M'), ∃ (b' : N'), R (n + 1) (Fin.snoc a a') (Fin.snoc b b')) (hback : ∀ {n : ℕ} {a : Fin n → M'} {b : Fin n → N'}, R n a b → ∀ (b' : N'), ∃ (a' : M'), R (n + 1) (Fin.snoc a a') (Fin.snoc b b')) (α : Ordinal.{u_1}) {n : ℕ} (a : Fin n → M') (b : Fin n → N') :

R n a b → BFEquiv α n a b

The two-structure form of the audited thin bridge: any tuple relation with atomic agreement and the forth/back extensions is BFEquiv at every ordinal.

The closed Scott seed and its fragment #