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.

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