Correctness of Boolean relation tables and matrix evaluation

Boolean relation tables faithfully and exhaustively present propositional relation environments. Structural induction on an FO matrix proves its Boolean evaluator agrees with satisfaction under the represented environment.

theorem Complexity.DescriptiveComplexity.toREnv_cons_internal {card k : Nat} {rctx : List Nat} (S : (Fin k → Fin card) → Bool) (ρ : DecREnv card rctx) : (DecREnv.cons S ρ).toREnv = rCons (fun (args : Fin k → Fin card) => S args = true) ρ.toREnv

theorem Complexity.DescriptiveComplexity.toREnv_injective_internal (card : Nat) (rctx : List Nat) : Function.Injective DecREnv.toREnv

theorem Complexity.DescriptiveComplexity.toREnv_surjective_internal (card : Nat) (rctx : List Nat) : Function.Surjective DecREnv.toREnv

theorem Complexity.DescriptiveComplexity.evalMatrixB_eq_sat_internal {V : Vocabulary} (A : DecFinStruct V) {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (h : φ.IsFOMatrix) (σ : Env A.card n) (ρ : DecREnv A.card rctx) : SOFormula.evalMatrixB A φ h σ ρ = true ↔ SOFormula.Sat A.toFinStruct σ ρ.toREnv φ