The signed root gate (issue #14, Unit 5, commit 1)

The polarity-refined twin of base_interpolant_of_empty_support_separator: at the root of the argument the allowed constant support is empty, so any separator is constant-free and strips to a base-language sentence — and the strip carries all three occurrence bounds, the two signed relation bounds included.

No new semantics: the entailment transport is the existing entails_reduct_of_entails_map, and the signed bound is the Unit-0 calculus lemma relationsInSigned_stripConsts. Nothing here inducts over formulas.

The file is deliberately neutral: it imports only the unsigned root gate and the signed occurrence calculus, so the paired/countable-completion machinery enters the Lyndon development only at the countable core (LyndonRelational.lean), which is its first semantic consumer.

theorem FirstOrder.Language.base_lyndon_interpolant_of_empty_support_separator {L : Language} {Γ₀ Δ₀ : Set L.Sentenceω} (σ : (L.withConstants ℕ).Sentenceω) (hsupp : sentenceJConsts σ ⊆ ∅) (hΓ : Theoryω.Entails (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' Γ₀) σ) (hΔ : Theoryω.Entails (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' Δ₀) (BoundedFormulaω.not σ)) : ∃ (θ₀ : L.Sentenceω), BoundedFormulaω.functionsIn θ₀ ⊆ BoundedFormulaω.baseFunctionsIn σ ∧ BoundedFormulaω.positiveRelationsIn θ₀ ⊆ BoundedFormulaω.basePositiveRelations σ ∧ BoundedFormulaω.negativeRelationsIn θ₀ ⊆ BoundedFormulaω.baseNegativeRelations σ ∧ Theoryω.Entails Γ₀ θ₀ ∧ Theoryω.Entails Δ₀ (BoundedFormulaω.not θ₀)

The signed root gate: an empty-support L[[ℕ]]-separator of the mapLanguage-images of (Γ₀, Δ₀) strips to a genuine base-language interpolant whose function symbols, positive relation occurrences, and negative relation occurrences are each bounded by the separator's corresponding base sets.