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.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_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.