Boundedness of well-founded models (issue #12, step 6 layer 2)

Marker Corollary 4.27 in relational/countable form, via the step-5 theorem contrapositively:

• wellFounded_boundedness_relational — if every model of φ interprets lt as a well-founded relation, then some countable ordinal α chains into no model of φ: the step-5 relation-preserving map would otherwise contradict well-foundedness (layer 1).
• wellOrder_type_boundedness_relational — if every model of φ interprets lt as a well-order, the same α uniformly bounds the order types: an order type ≥ α would re-embed the missing α-chain (Ordinal.type_le_iff' on Ordinal.type_toType).

Only the raw positive forms are consumed (RelChain, RelPreserving) — no injectivity is needed anywhere: well-foundedness kills the descending sequence directly.

theorem FirstOrder.Language.wellFounded_boundedness_relational {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (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 (relational/countable): if every model of φ interprets lt as a well-founded relation, then some countable ordinal α admits an lt-chain in no model of φ. Contrapositive of the step-5 theorem: were every α < ω₁ realized by a chain, some model of φ would carry a relation-preserving map from ℚ, contradicting well-foundedness through the descending negative rationals.

theorem FirstOrder.Language.wellOrder_type_boundedness_relational {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (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 (Marker Corollary 4.27, relational/countable): if every model of φ interprets lt as a well-order, then some countable ordinal α strictly bounds the order type of every model's interpreted relation.