Base-symbol occurrence projections (neutral layer)

The generic, unsigned occurrence bookkeeping shared by the Craig engine and the Lyndon refinement: how the base function/relation symbols of a subformula sit inside those of the whole, their invariance under substitution and openBounds, the instConst bounds, and the atomic facts for constEq and relInst.

Nothing here mentions inseparability, side bounds, the paired family, a consistency property, or the Henkin completion; the file's own dependency cone stops at the generated universe. It was extracted from PairedInsepFamily.lean so that the polarity-refined development (issue #14, Units 2-3) can consume these projections without dragging the paired/Henkin assembly into its cone -- the boundary now matches the proof architecture. Declaration names and namespaces are unchanged, so no compatibility shims are needed.

Base-symbol component projections

The dual of the baseFunctionsIn_*_subset union bounds: a subformula's base symbols are contained in the whole's.

theorem FirstOrder.Language.baseFunctionsIn_imp_left {L : Language} {φ ψ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.baseFunctionsIn φ ⊆ (BoundedFormulaω.imp φ ψ).baseFunctionsIn

theorem FirstOrder.Language.baseFunctionsIn_imp_right {L : Language} {φ ψ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.baseFunctionsIn ψ ⊆ (BoundedFormulaω.imp φ ψ).baseFunctionsIn

theorem FirstOrder.Language.baseRelationsIn_imp_left {L : Language} {φ ψ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.baseRelationsIn φ ⊆ (BoundedFormulaω.imp φ ψ).baseRelationsIn

theorem FirstOrder.Language.baseRelationsIn_imp_right {L : Language} {φ ψ : (L.withConstants ℕ).Sentenceω} : BoundedFormulaω.baseRelationsIn ψ ⊆ (BoundedFormulaω.imp φ ψ).baseRelationsIn

theorem FirstOrder.Language.baseFunctionsIn_component_iInf {L : Language} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : BoundedFormulaω.baseFunctionsIn (φs k) ⊆ (BoundedFormulaω.iInf φs).baseFunctionsIn

theorem FirstOrder.Language.baseRelationsIn_component_iInf {L : Language} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : BoundedFormulaω.baseRelationsIn (φs k) ⊆ (BoundedFormulaω.iInf φs).baseRelationsIn

theorem FirstOrder.Language.baseFunctionsIn_component_iSup {L : Language} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : BoundedFormulaω.baseFunctionsIn (φs k) ⊆ (BoundedFormulaω.iSup φs).baseFunctionsIn

theorem FirstOrder.Language.baseRelationsIn_component_iSup {L : Language} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (k : ℕ) : BoundedFormulaω.baseRelationsIn (φs k) ⊆ (BoundedFormulaω.iSup φs).baseRelationsIn

Relation occurrences are invariant under subst / openBounds (for instConst)

theorem FirstOrder.Language.relationsIn_subst_eq {L : Language} {α β : Type} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) (tf : α → (L.withConstants ℕ).Term β) : (φ.subst tf).relationsIn = φ.relationsIn

theorem FirstOrder.Language.relationsIn_openBounds_eq {L : Language} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω Empty n) : BoundedFormulaω.relationsIn φ.openBounds = φ.relationsIn

theorem FirstOrder.Language.baseFunctionsIn_instConst_subset {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaω.baseFunctionsIn (instConst c φ) ⊆ φ.all.baseFunctionsIn

theorem FirstOrder.Language.baseRelationsIn_instConst_subset {L : Language} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) : BoundedFormulaω.baseRelationsIn (instConst c φ) ⊆ φ.all.baseRelationsIn

Atomic base symbols

Constant equalities have no base symbols; a relation instance has only its own relation symbol, independent of the argument constants.

theorem FirstOrder.Language.baseFunctionsIn_constEq {L : Language} (a b : ℕ) : BoundedFormulaω.baseFunctionsIn (constEq a b) = ∅

theorem FirstOrder.Language.baseRelationsIn_constEq {L : Language} (a b : ℕ) : BoundedFormulaω.baseRelationsIn (constEq a b) = ∅

theorem FirstOrder.Language.baseFunctionsIn_relInst {L : Language} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) : BoundedFormulaω.baseFunctionsIn (relInst Rr g) = ∅

theorem FirstOrder.Language.baseRelationsIn_relInst {L : Language} {l : ℕ} (Rr : L.Relations l) (g g' : Fin l → ℕ) : BoundedFormulaω.baseRelationsIn (relInst Rr g) = BoundedFormulaω.baseRelationsIn (relInst Rr g')