The forward truth lemma for the quotient term model (issue #8, commit 5b)

From a Henkin-complete set S over the relational core L[[ℕ]], QuotientTermModel.lean (commit 5a) built the closed-term quotient model QModel hsc and its atomic semantics. This file lifts that to the full forward, polarity-sensitive truth lemma and packages a consumer-shaped model-existence theorem.

Discipline

The truth lemma is not a biconditional M ⊨ φ ↔ φ ∈ S. It is two separate forward implications — one per polarity — proven together by a single simultaneous recursion:

• truth_pos : σ ∈ S → M ⊨ σ (positive polarity)
• truth_neg : σ.not ∈ S → ¬ M ⊨ σ (negative polarity)

No excluded middle / by_cases on membership _ ∈ S, and no maximality/decisiveness of S, is used anywhere. Every step is driven by a constructive HenkinComplete field:

• connectives — imp / neg_imp / iInf / neg_iInf / iSup / neg_iSup;
• quantifiers — all_inst (positive) and neg_all_witness (negative) only;
• atomics — the commit-5a quotient API (qmk_eq_of_mem / qmk_ne_of_neg_mem / relMap_of_mem / not_relMap_of_neg_mem), with the Empty ⊕ Fin 0 sentence-term bridge below;
• contradictions — no_falsum / no_contradiction (C0).

The all case (depth-measure recursion)

The quantifier cases are handled by well-founded recursion on an ordinal depth measure, mirroring the shape of the legacy Methods/Henkin/Construction.lean truth lemma: from (all body) ∈ S the all_inst field yields, for every constant c, the sentence instConst c body = (body.openBounds).subst (fun _ => constTerm c), whose depth is strictly smaller than that of all body; recursion on that sentence plus realize_instConst_qmodel and surjectivity of qmk discharges the universal (dually for the negated universal via neg_all_witness).

The Empty ⊕ Fin 0 sentence-term bridge

Sentence atomics equal t u / rel R ts carry terms in L[[ℕ]].Term (Empty ⊕ Fin 0). Since both Empty and Fin 0 are uninhabited, every such term is ground; we collapse it to L[[ℕ]].Term Empty (a re-statement of the private helpers in Methods/Henkin/Construction.lean).

closeBy and its realization (validated commit-5b foundation)

theorem FirstOrder.Language.realize_closeBy {L : Language} [L.IsRelational] {U S : Set (L.withConstants ℕ).Sentenceω} {n : ℕ} (hsc : HenkinComplete U S) (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) (τ : Fin n → ℕ) : (closeBy φ τ).Realize (QModel hsc) ↔ φ.Realize Empty.elim fun (i : Fin n) => qmk hsc (constTerm (τ i))

Realizing closeBy φ τ in QModel hsc is realizing φ at the classes of the constants τ.

Surjectivity of the quotient map

Ordinal depth: strict decrease for the constant instance

The generic preservation/strict-decrease calculus for BoundedFormulaω.depth now lives in the neutral Lomega1omega/Depth.lean (shared with Methods/Henkin/Construction.lean); only the instConst combination is derived here.

Two small realization bookkeeping facts

The simultaneous forward truth lemma

truth_both hsc σ bundles the two polarities. It is a single well-founded recursion on σ.depth: connectives recurse on structural subformulas (strictly smaller depth), and the all case recurses on instConst c body (a sentence of strictly smaller depth).

The consumer model-existence theorem

theorem FirstOrder.Language.exists_model_of_henkinComplete {L : Language} {U S : Set (L.withConstants ℕ).Sentenceω} [L.IsRelational] (hsc : HenkinComplete U S) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), (∀ φ ∈ S, φ.Realize M) ∧ ∀ (φ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.not φ ∈ S → ¬φ.Realize M

Model existence from a Henkin-complete set. The quotient term model is a nonempty L[[ℕ]]-structure realizing every member of S and falsifying every sentence whose negation is in S. Both polarities are exposed for members of S.