The four-case gap insertion engine (issue #12, risky engine 2)

One uniform insertion lemma: a gap witness at β with α + α < β admits, at every slot s : Fin (m + 1) — below everything, between any two neighbours, above everything, or into empty support — a chain point whose insertion yields a gap witness at α for the extended tuple. This is Marker's C7c move ("pick β > α + α and place the fresh constant inside a gap"), made slot-uniform by the terminal and bottom margins (audit v2, D6).

The inserted rank is α at slot 0 and rank (s-1) + α otherwise (insertGapRank); every margin obligation is ordinal-rank arithmetic, and the four cases collapse into a single Fin.succAbove case analysis.

def FirstOrder.Language.insertGapRank {m : ℕ} (rank : Fin m → Ordinal.{0}) (α : Ordinal.{0}) (s : Fin (m + 1)) : Ordinal.{0}

The rank of the point inserted at slot s: α below everything (slot 0), the predecessor's rank plus α otherwise.

Equations

• FirstOrder.Language.insertGapRank rank α s = Fin.cases α (fun (k : Fin m) => rank k + α) s

theorem FirstOrder.Language.GapWitness.exists_insertNth {L : Language} {M : Type} [L.Structure M] {lt : L.Relations 2} {α β : Ordinal.{0}} {m : ℕ} {b : Fin m → M} (W : GapWitness lt β b) (hβ : α + α < β) (s : Fin (m + 1)) : ∃ (x : M), Nonempty (GapWitness lt α (s.insertNth x b))

The uniform insertion engine: given a gap witness at β with α + α < β, every slot admits a chain point whose insertion is a gap witness at α.