Signed occurrences through the relationalization layer (issue #14, Unit 6 — the D6 gate)

The polarity bookkeeping of the graph translation, in three gates.

Gate 1 — the atomic calculus. Term graphs are positive-only: termGraphAux is built from graph atoms by conjunction, einf, and existential blocks — all sign-preserving — so its negative set is empty and its positive set is the whole graphRelSym-image. The graph axioms, by contrast, do use their graph relations in both signs (functionality has one in an antecedent); what matters is that they contribute no base-relation occurrence in either sign (relationsInSigned_graphAxioms_inter_base), which is why the identities below are insensitive to whether the axioms sit in a conjunction or an antecedent.

Gate 2 — base-polarity preservation (the stop/go equation).

relationsInSigned s (relationalizeFormula φ) ∩ Set.range (baseRelSym L)
  = baseRelSym L '' relationsInSigned s φ

Relationalization preserves base-relation polarity on the nose, in the audit's exact image/intersection form, with positiveRelationsIn/negativeRelationsIn corollaries and preimage-shaped consumer lemmas.

Gate 3 — back-translation.

relationsInSigned s (backTranslateFormula θ) = baseRelSym L ⁻¹' relationsInSigned s θ

Here the key acceptance fact lands: a graph atom back-translates to an equality, whose signed sets are empty in both signs. So graph relations may carry arbitrary polarity in the graph world and still disappear harmlessly. Composing the two gates gives the exact base-polarity identities for Craig's graph antecedent (graphAxioms F).and (relationalizeFormula r) and consequent (graphAxioms F).imp (relationalizeFormula r).

Symbol-range disjointness

theorem FirstOrder.Language.graphRelSym_image_inter_range_baseRelSym {L : Language} (X : Set ((n : ℕ) × L.Functions n)) : L.graphRelSym '' X ∩ Set.range L.baseRelSym = ∅

A set of graph-relation images meets no base-relation image.

Gate 1: the atomic calculus — term graphs are positive-only

theorem FirstOrder.Language.relationsInSigned_termGraphAux {L : Language} {α β : Type} {m : ℕ} (t : L.Term β) (ρ : β → L.graphLanguage.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : BoundedFormulaω.relationsInSigned true (termGraphAux t ρ y) = L.graphRelSym '' t.functionsIn ∧ BoundedFormulaω.relationsInSigned false (termGraphAux t ρ y) = ∅

The term-graph signed identity, both signs at once (the recursion needs both): positive occurrences are the whole graphRelSym-image, negative occurrences are empty — term graphs are built from graph atoms by conjunction, einf, and existential blocks, all sign-preserving.

theorem FirstOrder.Language.positiveRelationsIn_termGraphAux {L : Language} {α β : Type} {m : ℕ} (t : L.Term β) (ρ : β → L.graphLanguage.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : (termGraphAux t ρ y).positiveRelationsIn = L.graphRelSym '' t.functionsIn

Term graphs put every graph relation positively.

theorem FirstOrder.Language.negativeRelationsIn_termGraphAux {L : Language} {α β : Type} {m : ℕ} (t : L.Term β) (ρ : β → L.graphLanguage.Term (α ⊕ Fin m)) (y : L.graphLanguage.Term (α ⊕ Fin m)) : (termGraphAux t ρ y).negativeRelationsIn = ∅

Term graphs put nothing negatively.

theorem FirstOrder.Language.relationsInSigned_equalGraph {L : Language} {α : Type} {n : ℕ} (t u : L.Term (α ⊕ Fin n)) : BoundedFormulaω.relationsInSigned true (equalGraph t u) = L.graphRelSym '' (t.functionsIn ∪ u.functionsIn) ∧ BoundedFormulaω.relationsInSigned false (equalGraph t u) = ∅

The equality atom's translation is positive-only, with exactly the two terms' graph relations.

theorem FirstOrder.Language.relationsInSigned_relGraph {L : Language} {α : Type} {n k : ℕ} (R : L.Relations k) (ts : Fin k → L.Term (α ⊕ Fin n)) : BoundedFormulaω.relationsInSigned true (relGraph R ts) = (L.graphRelSym '' ⋃ (i : Fin k), (ts i).functionsIn) ∪ {L.baseRelSym ⟨k, R⟩} ∧ BoundedFormulaω.relationsInSigned false (relGraph R ts) = ∅

The relation atom's translation is positive-only: the arguments' graph relations and the base symbol itself, all positive; nothing negative.

theorem FirstOrder.Language.preimage_baseRelSym_graphRelSym_image {L : Language} (X : Set ((n : ℕ) × L.Functions n)) : L.baseRelSym ⁻¹' L.graphRelSym '' X = ∅

Preimage form of range-disjointness: no base symbol pulls back from a graph image.

theorem FirstOrder.Language.preimage_baseRelSym_relationsInSigned_graphAxioms {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (graphAxioms F) = ∅

The graph axioms have no base-relation occurrence in either sign — the fact that makes the base-polarity identities insensitive to which side the axioms sit on.

theorem FirstOrder.Language.relationsInSigned_graphAxioms_inter_base {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] : BoundedFormulaω.relationsInSigned s (graphAxioms F) ∩ Set.range L.baseRelSym = ∅

Intersection form of the same fact.

Gate 2: base-polarity preservation (the stop/go equation)

theorem FirstOrder.Language.mem_relationsInSigned_relationalizeFormula {L : Language} {α : Type} (s : Bool) (p : (n : ℕ) × L.Relations n) {n : ℕ} (φ : L.BoundedFormulaω α n) : L.baseRelSym p ∈ BoundedFormulaω.relationsInSigned s (relationalizeFormula φ) ↔ p ∈ BoundedFormulaω.relationsInSigned s φ

The D6 stop/go equation, membership form — the workhorse. A base symbol occurs with sign s in the relationalization exactly when it occurs with sign s in the original. Phrased as a membership equivalence so the induction never touches set operations at the two (definitionally equal but syntactically distinct) relation-symbol types.

theorem FirstOrder.Language.preimage_baseRelSym_relationalizeFormula {L : Language} {α : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (relationalizeFormula φ) = BoundedFormulaω.relationsInSigned s φ

The D6 stop/go equation, preimage form: pulling the translated signed occurrences back along the base embedding recovers the original signed occurrences exactly.

theorem FirstOrder.Language.relationsInSigned_relationalizeFormula_inter_base {L : Language} {α : Type} (s : Bool) {n : ℕ} (φ : L.BoundedFormulaω α n) : BoundedFormulaω.relationsInSigned s (relationalizeFormula φ) ∩ Set.range L.baseRelSym = L.baseRelSym '' BoundedFormulaω.relationsInSigned s φ

The D6 stop/go equation, in the audit's image/intersection form.

theorem FirstOrder.Language.positiveRelationsIn_relationalizeFormula_inter_base {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : (relationalizeFormula φ).positiveRelationsIn ∩ Set.range L.baseRelSym = L.baseRelSym '' φ.positiveRelationsIn

Gate 2, positive corollary (the audit's stated form).

theorem FirstOrder.Language.negativeRelationsIn_relationalizeFormula_inter_base {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : (relationalizeFormula φ).negativeRelationsIn ∩ Set.range L.baseRelSym = L.baseRelSym '' φ.negativeRelationsIn

Gate 2, negative corollary.

Gate 3: back-translation

theorem FirstOrder.Language.mem_relationsInSigned_backTranslateFormula {L : Language} {α : Type} (s : Bool) (p : (n : ℕ) × L.Relations n) {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : p ∈ BoundedFormulaω.relationsInSigned s (backTranslateFormula θ) ↔ L.baseRelSym p ∈ BoundedFormulaω.relationsInSigned s θ

The back-translation signed identity, membership form: a base symbol occurs with sign s in the back-translation exactly when its graph image occurs with sign s upstream. The graph atom case is the acceptance fact: it back-translates to an equality, contributing to neither sign, so graph relations may carry arbitrary polarity upstream and still vanish.

theorem FirstOrder.Language.relationsInSigned_backTranslateFormula {L : Language} {α : Type} (s : Bool) {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : BoundedFormulaω.relationsInSigned s (backTranslateFormula θ) = L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s θ

Gate 3: the signed occurrences of a back-translation are the base-embedding preimage of the graph formula's signed occurrences.

theorem FirstOrder.Language.positiveRelationsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : (backTranslateFormula θ).positiveRelationsIn = L.baseRelSym ⁻¹' θ.positiveRelationsIn

Gate 3, positive corollary.

theorem FirstOrder.Language.negativeRelationsIn_backTranslateFormula {L : Language} {α : Type} {n : ℕ} (θ : L.graphLanguage.BoundedFormulaω α n) : (backTranslateFormula θ).negativeRelationsIn = L.baseRelSym ⁻¹' θ.negativeRelationsIn

Gate 3, negative corollary.

The base-polarity identities for Craig's graph roots

theorem FirstOrder.Language.relationsInSigned_graphAnd_inter_base {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : BoundedFormulaω.relationsInSigned s (BoundedFormulaω.and (graphAxioms F) (relationalizeFormula φ)) ∩ Set.range L.baseRelSym = L.baseRelSym '' BoundedFormulaω.relationsInSigned s φ

The graph antecedent (graphAxioms F).and (relationalizeFormula r) has exactly the base polarity of r, in either sign.

theorem FirstOrder.Language.relationsInSigned_graphImp_inter_base {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : BoundedFormulaω.relationsInSigned s (BoundedFormulaω.imp (graphAxioms F) (relationalizeFormula φ)) ∩ Set.range L.baseRelSym = L.baseRelSym '' BoundedFormulaω.relationsInSigned s φ

The graph consequent (graphAxioms F).imp (relationalizeFormula r) likewise: the axioms contribute nothing to the base part even though the implication flips their sign.

theorem FirstOrder.Language.preimage_baseRelSym_graphAnd {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (BoundedFormulaω.and (graphAxioms F) (relationalizeFormula φ)) = BoundedFormulaω.relationsInSigned s φ

Preimage form of the graph-antecedent identity — the shape the endpoint consumes, so that no Sigma/definitional-equality friction leaks into the assembly.

theorem FirstOrder.Language.preimage_baseRelSym_graphImp {L : Language} (s : Bool) (F : Set ((n : ℕ) × L.Functions n)) [Countable ↑F] (φ : L.Sentenceω) : L.baseRelSym ⁻¹' BoundedFormulaω.relationsInSigned s (BoundedFormulaω.imp (graphAxioms F) (relationalizeFormula φ)) = BoundedFormulaω.relationsInSigned s φ

Preimage form of the graph-consequent identity: the axioms sit in an antecedent, so the implication flips their sign — and they still contribute nothing to the base part.