The bundled consistency property and completion endpoint (issue #12, packaging)

The fifteen closure theorems package directly into the kernel's ConsistencyPropertyEqOn over the enumeration universe rooted at the lifted sentence, and the fair enumeration turns the infinite initial member Bφ into a Henkin-complete extension.

Boundaries (kept deliberately visible):

• WOMem is used only for the stage family (woConsistencyProperty.sets);
• the infinite initial member is baseDiagram φ lt (accepted by the fair enumeration — the frozen D4 member shape);
• the completed union is not claimed to satisfy WOMem or to belong to the family — the endpoint returns only containment and HenkinComplete;
• HasWellOrderedChains enters only through baseDiagram_mem;
• countability enters only at the fair-enumeration invocation, never in the fifteen closure lemmas.

Step 5 consumes the returned S opaquely: the quotient term model realizes the lifted root, q ↦ [ratConst q] maps the rationals, and membership of every positive diagram atom supplies RelPreserving.

def FirstOrder.Language.woConsistencyProperty {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) : ConsistencyPropertyEqOn (GenU (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ))

The well-ordering consistency property: the WOMem stage family, bundled — each kernel field is one of the fifteen closure theorems.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.exists_henkinComplete_baseDiagram {L : Language} (φ : L.Sentenceω) (lt : L.Relations 2) [Countable ((l : ℕ) × L.Relations l)] (h : HasWellOrderedChains φ lt) : ∃ (S : Set (L.withConstants ℕ).Sentenceω), baseDiagram φ lt ⊆ S ∧ HenkinComplete (GenU (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ)) S

The completion endpoint (consumer-facing): under the well-ordered-chains hypothesis and the relational-core countability, a Henkin-complete set containing the base diagram exists. Step 5 consumes S opaquely.