Semantic monotonicity under signed reinterpretation (issue #14, Unit 1)

The semantic content of the signed traversal of Lomega1omega/Polarity.lean: over a relational language, growing the relations that occur positively and shrinking those that occur negatively preserves truth.

realize_mono_of_signed φ S₁ S₂ hpos hneg : Realize[S₁] φ v xs → Realize[S₂] φ v xs

The two structures are explicit arguments quantified after φ, which is what makes the induction go through: the implication case calls the antecedent's inductive hypothesis at the swapped pair (S₂, S₁), where the two hypotheses exchange roles exactly as positiveRelationsIn (φ.imp ψ) = negativeRelationsIn φ ∪ positiveRelationsIn ψ predicts. This is the semantic stop/go gate for the polarity definition: if the traversal had the wrong sign convention anywhere, this induction would not close.

Only the forward monotonicity theorem is exported. The dual (shrink positives, grow negatives, reflect truth) is the same statement with the structures swapped — it is already encoded in the hypotheses and in the implication recursion, so a separate theorem would only duplicate the API.

Relationality is used exactly once, to make term realization structure-independent (realize_term_of_isRelational); the public statement therefore needs no function-agreement hypothesis.

theorem FirstOrder.Language.BoundedFormulaω.realize_mono_of_signed {L : Language} {α M : Type} [L.IsRelational] {n : ℕ} (φ : L.BoundedFormulaω α n) (S₁ S₂ : L.Structure M) : (∀ p ∈ φ.positiveRelationsIn, ∀ (a : Fin p.fst → M), Structure.RelMap p.snd a → Structure.RelMap p.snd a) → (∀ p ∈ φ.negativeRelationsIn, ∀ (a : Fin p.fst → M), Structure.RelMap p.snd a → Structure.RelMap p.snd a) → ∀ {v : α → M} {xs : Fin n → M}, φ.Realize v xs → φ.Realize v xs

Semantic monotonicity under signed reinterpretation (the Unit-1 acceptance gate): if S₂ interprets every relation occurring positively in φ at least as widely as S₁, and every relation occurring negatively in φ at most as widely, then truth of φ transports from S₁ to S₂.

The structures are quantified after φ on purpose: the imp case applies the inductive hypothesis for the antecedent at the swapped pair (S₂, S₁).