Semantics of tuple pullback for least-fixed-point formulas

The full-tuple compiler preserves truth, including nested least fixed points and captured parameters. The proof transports all candidate relations through the tuple bijection; it therefore also preserves the total pre-fixed-intersection semantics of unchecked syntax.

theorem Cslib.Logic.FO.LFP.Tuple.realize_onFormula {L : FirstOrder.Language} {L' : FirstOrder.Language} {d : ℕ} {M N : Type} [L.Structure M] [L'.Structure N] (f : Operator.Tuple.FOMap L L' d) (e : (Fin d → M) ≃ N) (hf : ∀ {α : Type} (φ : L'.Formula α) (v : α × Fin d → M), (f φ).Realize v ↔ φ.Realize fun (a : α) => e fun (i : Fin d) => v (a, i)) {Γ : List ℕ} {α : Type} (φ : RawFormula L' Γ α) (ρs : Operator.RelEnv (List.map (fun (x : ℕ) => x * d) Γ) M) (ρt : Operator.RelEnv Γ N) : (∀ {k : ℕ} (r : Operator.RelVar Γ k) (xs : Fin (k * d) → M), xs ∈ ρs (Operator.RelVar.scale d r) ↔ (Operator.Tuple.blockEquiv e k) xs ∈ ρt r) → ∀ (v : α × Fin d → M), Operator.Formula.Realize interpretation (onFormula (fun {α : Type} => f) φ) (fun {k : ℕ} => ρs) v ↔ Operator.Formula.Realize interpretation φ (fun {k : ℕ} => ρt) fun (a : α) => e fun (i : Fin d) => v (a, i)

Full-tuple pullback preserves truth for arbitrary scoped relation valuations, including nested operators. The relation valuations correspond blockwise through blockEquiv.