Removing symbol countability (issue #12, the sublanguage wrapper)

The step-5/6 theorems assumed [Countable (Σ l, L.Relations l)] for the fair enumeration. This wrapper removes it by the two-sorted symbol-generated sublanguage (symbSublang φ.functionsIn (insert ⟨2, lt⟩ φ.relationsIn) — both sorts countable, proved from the sentence's own symbol supply, with lt inserted so the distinguished relation survives the restriction):

• the well-ordered-chains hypothesis transfers to the sublanguage along reducts;
• the sublanguage endpoint produces the model and rational map;
• expandSymbStructureBase expands the model back to L, preserving the root (realize_restrictSymbols_expandSymbStructureBase) and the relation (dif_pos).

[L.IsRelational] remains — it is consumed by the quotient term model, and its removal is the separate arbitrary-function-language graph translation, not this wrapper.

theorem FirstOrder.Language.symbSublang_isRelational {L : Language} [L.IsRelational] (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) : (symbSublang F R).IsRelational

A two-sorted sublanguage of a relational language is relational.

theorem FirstOrder.Language.exists_model_relPreserving_isRelational {L : Language} [L.IsRelational] (φ : L.Sentenceω) (lt : L.Relations 2) (h : HasWellOrderedChains φ lt) : ∃ (M : Type) (x : L.Structure M) (_ : Nonempty M) (f : ℚ → M), φ.Realize M ∧ RelPreserving lt f

Step-5 endpoint, no symbol countability (relational): the countable-relational-core hypothesis of exists_model_relPreserving_relational removed via the two-sorted sublanguage generated by the sentence's own symbols together with lt.

theorem FirstOrder.Language.wellFounded_boundedness_isRelational {L : Language} [L.IsRelational] (φ : L.Sentenceω) (lt : L.Relations 2) (hwf : ∀ (M : Type) (x : L.Structure M), φ.Realize M → WellFounded fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]) : ∃ α < (Cardinal.aleph 1).ord, ∀ (M : Type) (x : L.Structure M), φ.Realize M → ¬∃ (w : α.ToType → M), RelChain lt α w

Boundedness, well-founded form, no symbol countability: layer 2's wellFounded_boundedness_relational through the sublanguage-wrapped endpoint.

theorem FirstOrder.Language.wellOrder_type_boundedness_isRelational {L : Language} [L.IsRelational] (φ : L.Sentenceω) (lt : L.Relations 2) (hwo : ∀ (M : Type) (x : L.Structure M), φ.Realize M → IsWellOrder M fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]) : ∃ α < (Cardinal.aleph 1).ord, ∀ (M : Type) (inst : L.Structure M) (hreal : φ.Realize M), (Ordinal.type fun (x y : M) => Structure.RelMap lt ![x, y]) < α

Boundedness, order-type form, no symbol countability (Marker Corollary 4.27 at any relational language).

theorem FirstOrder.Language.wellOrdering_undefinable_isRelational {L : Language} [L.IsRelational] (lt : L.Relations 2) : ¬∃ (φ : L.Sentenceω), ∀ (M : Type) (x : L.Structure M), φ.Realize M ↔ IsWellOrder M fun (x_1 y : M) => Structure.RelMap lt ![x_1, y]

Undefinability of well-ordering, no symbol countability (weak form, any relational language).