Generic relation lemmas for the boundedness corollaries (issue #12, step 6 layer 1)

Pure order-theoretic consequences of the raw positive conclusion RelPreserving, with no model extraction involved:

• RelPreserving.injective_of_irreflexive — the derived injectivity corollary (issue precision note: injectivity is not part of the raw theorem, it is a corollary under irreflexivity of the interpreted relation);
• RelPreserving.descending — the negative rationals give an infinite strictly descending sequence through the interpreted relation;
• not_relPreserving_of_wellFounded — hence no relation-preserving map from ℚ exists into a structure whose interpreted relation is well-founded (via WellFounded.has_min; no strict-order hypotheses, so RelEmbedding.natGT is deliberately not used).

theorem FirstOrder.Language.RelPreserving.injective_of_irreflexive {L : Language} {M : Type} [L.Structure M] {lt : L.Relations 2} {f : ℚ → M} (hf : RelPreserving lt f) (hirr : ∀ (x : M), ¬Structure.RelMap lt ![x, x]) : Function.Injective f

Derived injectivity: a relation-preserving map from ℚ into a structure whose interpreted relation is irreflexive is injective — if q < r collided, preservation would put the collision point below itself.

theorem FirstOrder.Language.RelPreserving.descending {L : Language} {M : Type} [L.Structure M] {lt : L.Relations 2} {f : ℚ → M} (hf : RelPreserving lt f) (n : ℕ) : Structure.RelMap lt ![f (-↑(n + 1)), f (-↑n)]

The descending sequence: the negative rationals turn a relation-preserving map into an infinite strictly descending sequence for the interpreted relation.

theorem FirstOrder.Language.not_descending_of_wellFounded {α : Type u_1} {r : α → α → Prop} (hwf : WellFounded r) (g : ℕ → α) : ¬∀ (n : ℕ), r (g (n + 1)) (g n)

A well-founded relation admits no infinite descending sequence (direct, via WellFounded.has_min — no strict-order hypotheses on the relation).

theorem FirstOrder.Language.not_relPreserving_of_wellFounded {L : Language} {M : Type} [L.Structure M] {lt : L.Relations 2} (hwf : WellFounded fun (x y : M) => Structure.RelMap lt ![x, y]) (f : ℚ → M) : ¬RelPreserving lt f

No relation-preserving map into a well-founded relation: the target of the step-5 theorem can never have a well-founded interpreted relation.