From coded well-orders to models: the defect bridge

A structure whose distinguished relation fails to be a well-order carries a countable nonempty seed of witnesses; seeding a countable fragment-elementary substructure with it and transporting that substructure to the carrier ℕ produces a code which is not a well-order. Contrapositively, if every code satisfying φ is a well-order then so is every model of φ ⊓ infiniteAxiom.

Deliberately independent of López–Escobar. This file imports only the well-order class, the fragment Löwenheim–Skolem machinery and the infiniteness axiom. Two very different consumers need the bridge and neither should have to drag in the other:

• Descriptive/WellOrderNonBorel.lean (#33) obtains its φ from López–Escobar applied to a hypothetically Borel WO;
• Descriptive/AnalyticWellOrderBoundedness.lean (#64) obtains its φ from the analytic-PC sandwich, where the reduct class is only contained in WO.

That second consumer is why isWellOrder_of_realize_of_modelsOf_subset is the primary form: a pcSentence's reduct class sits inside an invariant envelope and never equals a prescribed set.

Main results

• exists_countable_defect_seed: a well-order failure has a countable nonempty witness set.
• isWellOrder_of_realize_of_modelsOf_subset: containment form of the bridge.
• isWellOrder_of_realize: the equality-form corollary.

The defect seed

theorem FirstOrder.Language.exists_countable_defect_seed {M : Type} {r : M → M → Prop} (h : ¬IsWellOrder M r) : ∃ (X : Set M), X.Countable ∧ X.Nonempty ∧ ∀ (N : Set M), X ⊆ N → ¬IsWellOrder ↑N fun (x y : ↑N) => r ↑x ↑y

A structure whose relation fails to be a well-order carries a countable nonempty seed of witnesses: every subset containing the seed inherits the failure. In this Mathlib a well-order is trichotomy plus well-foundedness (transitivity is derived), so there are exactly two cases: a two-element trichotomy failure, and the range of an infinite descending sequence.

The bridge: coded definability forces every model to be well-ordered

theorem FirstOrder.Language.isWellOrder_of_realize {L : Language} [L.IsRelational] (lt : L.Relations 2) {φ : L.Sentenceω} (hφ : ModelsOf φ = wellOrderClass lt) (M : Type) [instM : L.Structure M] (hM : Sentenceω.Realize (BoundedFormulaω.and φ L.infiniteAxiom) M) : IsWellOrder M fun (x y : M) => Structure.RelMap lt ![x, y]

The bridge, equality form: if a sentence defines the well-order class on codes, then every model of it conjoined with the infiniteness axiom is well-ordered.

The ModelsOf φ = wellOrderClass lt specialization of isWellOrder_of_realize_of_modelsOf_subset; the defect-seed argument lives there and is not repeated.