A-elementarity and the fragment Tarski–Vaught criterion (issue #13 unit 4)

Per the frozen audit (docs/fragments-audit.md §4–§5): AElementary A f is DIRECT TRUTH AGREEMENT on the fragment's members, at all semantic tuples, along an embedding — stated as an iff, since fragments are not assumed closed under formal negation. Basic API: identity, composition, the two-out-of-three lemma (the form the chain-union development consumes), and sentence/theory transport. The fragment-relative Tarski–Vaught criterion (aElementary_of_tarskiVaught) upgrades witness closure for the fragment-controlled universals to full A-elementarity — witnesses are ELEMENTS (semantic parameters), so no syntactic substitution enters the induction.

def FirstOrder.Language.AElementary {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] (A : L.Fragment) (f : L.Embedding N M) : Prop

A-elementarity: truth agreement on every fragment member, at every tuple, along an embedding.

Equations

• FirstOrder.Language.AElementary A f = ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ A.toSet → ∀ (a : Fin n → N), φ.Realize Empty.elim (⇑f ∘ a) ↔ φ.Realize Empty.elim a

theorem FirstOrder.Language.AElementary.refl {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) : AElementary A (Embedding.refl L M)

theorem FirstOrder.Language.AElementary.comp {L : Language} {M N P : Type w} [L.Structure M] [L.Structure N] [L.Structure P] {A : L.Fragment} {f : L.Embedding N M} {g : L.Embedding P N} (hf : AElementary A f) (hg : AElementary A g) : AElementary A (f.comp g)

theorem FirstOrder.Language.AElementary.of_comp {L : Language} {M N P : Type w} [L.Structure M] [L.Structure N] [L.Structure P] {A : L.Fragment} {f : L.Embedding N M} {g : L.Embedding P N} (hf : AElementary A f) (hfg : AElementary A (f.comp g)) : AElementary A g

Two-out-of-three: if the composite and the outer embedding are A-elementary, so is the inner one — the form the chain development consumes.

theorem FirstOrder.Language.AElementary.realize_sentence_iff {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (h : AElementary A f) {φ : L.Sentenceω} (hφ : ⟨0, φ⟩ ∈ A.toSet) : φ.Realize M ↔ φ.Realize N

Sentence transport: for a fragment sentence, truth agrees between the two structures.

theorem FirstOrder.Language.AElementary.theoryModel_iff {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {A : L.Fragment} {f : L.Embedding N M} (h : AElementary A f) {T : Set L.Sentenceω} (hT : ∀ φ ∈ T, ⟨0, φ⟩ ∈ A.toSet) : Theoryω.Model T M ↔ Theoryω.Model T N

Theory transport: a fragment theory true in the ambient model is true in the A-elementary substructure, and conversely.

theorem FirstOrder.Language.aElementary_of_tarskiVaught {L : Language} {M N : Type w} [L.Structure M] [L.Structure N] {A : L.Fragment} (f : L.Embedding N M) (hTV : ∀ {n : ℕ} (φ : L.BoundedFormulaω Empty (n + 1)), ⟨n, φ.all⟩ ∈ A.toSet → ∀ (a : Fin n → N), (∃ (m : M), ¬φ.Realize Empty.elim (Fin.snoc (⇑f ∘ a) m)) → ∃ (b : N), ¬φ.Realize Empty.elim (Fin.snoc (⇑f ∘ a) (f b))) : AElementary A f

The fragment Tarski–Vaught criterion: if every fragment-controlled universal admits element witnesses in N for its failures in M, then the embedding is A-elementary.