Base diagram, preservation predicate, and the gap witness (issue #12, commit 2)

The three frozen foundations of the well-ordering construction (audit v2, D1/D2/D4/D6):

• baseDiagram φ lt — the countable base Bφ = {φ} ∪ {d_q < d_r : q < r} that literally belongs to every consistency-property member (D4);
• RelChain / RelPreserving — the raw positive forms: an ordinal-indexed chain strictly increasing for the interpreted relation, and a relation-preserving map from ℚ (D1/D2 — no injectivity, no order-embedding packaging);
• GapWitness — the rank-based representation frozen from the audit-§8 probe: a chain of length γ, marked ranks for the mentioned tuple, and the three α-margins (initial, internal, terminal) as explicit fields.

One addition to the §8 structure (discovered by the insertion engine, kept as an explicit field per review): lt_gamma : α < γ, the bottom margin. For m > 0 it is derivable (α ≤ rank 0 < γ), but for m = 0 the other fields are vacuous and the witness would carry no information about the chain's length — insertion into empty support (the fourth case of the uniform insertion lemma) needs the chain to be long enough to contain rank α.

GapWitness.mono is the downward closure in α consumed by the ω₁ fiber argument (C4).

The base diagram

def FirstOrder.Language.ratLtAtom {L : Language} (lt : L.Relations 2) (q r : ℚ) : (L.withConstants ℕ).Sentenceω

The positive order atom d_q < d_r (over the rational constants of the coding layer).

Equations

• FirstOrder.Language.ratLtAtom lt q r = FirstOrder.Language.relInst lt ![FirstOrder.Language.ratConstIdx q, FirstOrder.Language.ratConstIdx r]

def FirstOrder.Language.baseDiagram {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) : Set (L.withConstants ℕ).Sentenceω

The base diagram Bφ = {φ} ∪ {d_q < d_r : q < r}: the lifted sentence together with the full positive rational diagram. Per the frozen member shape (D4), Bφ literally belongs to every consistency-property member.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.mapLanguage_mem_baseDiagram {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) : BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ ∈ baseDiagram φ lt

theorem FirstOrder.Language.ratLtAtom_mem_baseDiagram {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) {q r : ℚ} (h : q < r) : ratLtAtom lt q r ∈ baseDiagram φ lt

theorem FirstOrder.Language.baseDiagram_countable {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) : (baseDiagram φ lt).Countable

The base diagram is countable.

The raw positive predicates

def FirstOrder.Language.RelChain {L : Language} {M : Type} [L.Structure M] (lt : L.Relations 2) (γ : Ordinal.{0}) (w : γ.ToType → M) : Prop

An ordinal-indexed chain in M, strictly increasing for the interpreted relation lt — the raw positive form (no injectivity packaged).

Equations

• FirstOrder.Language.RelChain lt γ w = ∀ (x y : γ.ToType), x < y → FirstOrder.Language.Structure.RelMap lt ![w x, w y]

def FirstOrder.Language.RelPreserving {L : Language} {M : Type} [L.Structure M] (lt : L.Relations 2) (f : ℚ → M) : Prop

A relation-preserving map from ℚ — the raw positive conclusion form (D2).

Equations

• FirstOrder.Language.RelPreserving lt f = ∀ (q r : ℚ), q < r → FirstOrder.Language.Structure.RelMap lt ![f q, f r]

def FirstOrder.Language.HasWellOrderedChains {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) : Prop

The hypothesis form (D1): for every countable ordinal, a model of φ with an α-length lt-chain.

Equations

• One or more equations did not get rendered due to their size.

The gap witness (frozen, audit §8 + the bottom margin)

structure FirstOrder.Language.GapWitness {L : Language} {M : Type} [L.Structure M] (lt : L.Relations 2) (α : Ordinal.{0}) {m : ℕ} (b : Fin m → M) : Type 1

The gap witness (rank form): a chain of length γ containing the marked tuple b at ranks that carry an initial margin ≥ α, pairwise internal gaps ≥ α, a terminal margin ≥ α, and the bottom margin α < γ (explicit even where derivable — see the module docstring).

• γ : Ordinal.{0}

  the chain length

• w : self.γ.ToType → M

  the chain

• chain : RelChain lt self.γ self.w
• rank : Fin m → Ordinal.{0}

  the marked ranks of the tuple

• rank_lt (i : Fin m) : self.rank i < self.γ
• initial (i : Fin m) : α ≤ self.rank i

  initial margin

• gaps (i j : Fin m) : i < j → self.rank i + α ≤ self.rank j

  internal gaps

• terminal (i : Fin m) : self.rank i + α ≤ self.γ

  terminal margin

• lt_gamma : α < self.γ

  bottom margin: the chain is long enough to contain rank α (data for m = 0)

• marks (i : Fin m) : b i = self.w (Ordinal.ToType.mk ⟨self.rank i, ⋯⟩)

  the tuple is the chain at the marked ranks

def FirstOrder.Language.GapWitness.mono {L : Language} {M : Type} [L.Structure M] {lt : L.Relations 2} {α β : Ordinal.{0}} (hβ : β ≤ α) {m : ℕ} {b : Fin m → M} (W : GapWitness lt α b) : GapWitness lt β b

Downward closure in α — the monotonicity consumed by the ω₁ fiber argument: a witness at α is a witness at every β ≤ α.

Equations

• FirstOrder.Language.GapWitness.mono hβ W = { γ := W.γ, w := W.w, chain := ⋯, rank := W.rank, rank_lt := ⋯, initial := ⋯, gaps := ⋯, terminal := ⋯, lt_gamma := ⋯, marks := ⋯ }