Completing the budgeted labelled pair (issue #15)

The first consumer of budgetedPairConsistencyProperty. It does one thing: run the fair Henkin completion on the labelled root member and expose the result opaquely, as containment plus HenkinComplete.

The internal S* ⊆ GenU fact is deliberately dropped. The model endpoint should consume a completion, not a subset of a particular universe, so that swapping the completion strategy cannot ripple outward.

Boundaries

• Countability of the generated universe is derived, not assumed: genU_countable needs only [Countable (Σ l, L.Relations l)], which is the honest boundary here.
• No L.IsRelational. Relationality is a requirement of the quotient term model, so it belongs to the model endpoint, not to completion.
• Finite constant support is accepted for r₂ rather than for the labelled right root r₂.not, and converted locally — the interpolation consumer holds the former.

theorem FirstOrder.Language.exists_henkinComplete_budgetedPairRoot {L : Language} [Countable ((l : ℕ) × L.Relations l)] {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hroot : BudgetedPairMem r₁ (BoundedFormulaω.not r₂) F₁ R₁ F₂ R₂ ({r₁} ∪ {BoundedFormulaω.not r₂})) : ∃ (Sstar : Set (L.withConstants ℕ).Sentenceω), {r₁} ∪ {BoundedFormulaω.not r₂} ⊆ Sstar ∧ HenkinComplete (GenU r₁ (BoundedFormulaω.not r₂)) Sstar

The completion endpoint. From a labelled root member, a Henkin-complete superset of the root pair.

Stated with finite support of r₂ rather than of r₂.not; the two are equal, but the former is what an interpolation consumer has to hand.