Semantics of openBounds and of relabeling by insertLastBound

Two semantic round-trip lemmas about the bound/free variable bookkeeping of Lomega1omega/Operations, in a neutral module so that consumers below the Henkin construction and the Scott analysis can use them without importing either:

• realize_relabel_insertLastBound_zero — relabeling a formula with n + 1 free variables by insertLastBound binds the last one; evaluating with v and a one-element bound tuple xs is evaluating the original at snoc v (xs 0);
• realize_openBounds — openBounds preserves semantics: evaluating φ.openBounds at a free assignment xs is evaluating φ with bound assignment xs.

Both were previously proved inside Scott/Formula.lean and Methods/Henkin/Construction.lean respectively; the statements and names are unchanged.

theorem FirstOrder.Language.realize_relabel_insertLastBound_zero {L : Language} {N : Type w} [L.Structure N] {n : ℕ} (φ : L.Formulaω (Fin (n + 1))) (v : Fin n → N) (xs : Fin 1 → N) : (BoundedFormulaω.relabel insertLastBound φ).Realize v xs ↔ φ.Realize (Fin.snoc v (xs 0))

The key semantics lemma for formulas with 0 bound variables: relabeling with insertLastBound shifts the last free variable to a bound variable position.

For φ : L.Formulaω (Fin (n+1)) (a formula with n+1 free vars and 0 bound vars):

• φ.relabel insertLastBound : L.BoundedFormulaω (Fin n) 1 has n free vars and 1 bound var
• When we evaluate with free var assignment v : Fin n → N and bound var assignment xs : Fin 1 → N, this corresponds to evaluating the original formula with snoc v (xs 0) : Fin (n+1) → N

theorem FirstOrder.Language.snoc_elim0_zero_eq {M : Type u_1} (x : M) : Fin.snoc Fin.elim0 x 0 = x

Helper: snoc Fin.elim0 x evaluated at 0 : Fin 1 gives x.

theorem FirstOrder.Language.realize_openBounds {L : Language} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (xs : Fin n → M) : φ.openBounds.Realize xs ↔ φ.Realize Empty.elim xs

Semantic roundtrip: openBounds preserves semantics. For φ : BoundedFormulaω Empty n, evaluating openBounds φ with free variable assignment xs : Fin n → M is equivalent to evaluating φ with bound variable assignment xs.