Mathlib-grounded team-set closure substrate

@cite{anttila-2021} @cite{vaananen-2007}

The deep mathematical content of Core/Logic/Team/Properties re-expressed as facts about subsets of Finset α using mathlib's existing primitives:

linglib name	mathlib name
downwardClosed-shape	IsLowerSet (T : Set (Finset α))
unionClosed-shape	SupClosed (T : Set (Finset α))
emptyTeam-shape	∅ ∈ T
flat-shape	(defined below)

Properties.lean's API is parameterised over Model → Form → Finset α → Prop for consumer ergonomics, but the content of every closure-property theorem reduces to a fact about Set (Finset α) independent of formula or model. This file states those facts at the parametric-content-free level. Properties.lean becomes a thin wrapper exporting the consumer form.

Why this matters

The Form/Model parameters in Properties.lean are decorative: every theorem unionClosed support φ ↔ ... reduces to "the set { t | support M φ t } is SupClosed." Hoisting to the mathlib level exposes:

1. The theorem is about lattice structure on Finset α, not about logic. The flatness theorem is "principal lower set generated by atoms" — pure powerset combinatorics.
2. Cross-carrier portability: Set α (used by Question) carries the same lattice structure (Set α is a CompleteBooleanAlgebra with ⊔ = ∪, ⊥ = ∅). The same flatness theorem holds for Set (Set α) with mathlib IsLowerSet and arbitrary-union closure. The Question bridge in Core/Question/Flatness.lean is the Set carrier instance.
3. No re-proof per consumer: BSML, QBSML, and any future team-semantic logic with Finset α carrier inherit the flatness theorem at zero substrate cost.

Mathlib alignment

• IsLowerSet (s : Set α) [LE α] — Mathlib.Order.Defs.Unbundled. For Finset α, the LE instance is ⊆.
• SupClosed (s : Set α) [SemilatticeSup α] — Mathlib.Order.SupClosed. For Finset α, ⊔ = ∪.
• Finset α is a SemilatticeSup with OrderBot (⊥ = ∅), so all three predicates apply directly.

@[reducible, inline]

abbrev Core.Logic.Team.TeamSet (α : Type u_2) : Type u_2

A team-set: a subset of teams (each team is a Finset α).

Equivalently, the extension of a team-semantic predicate at a fixed model + formula: { t : Finset α | support M φ t }.

Equations

• Core.Logic.Team.TeamSet α = Set (Finset α)

def Core.Logic.Team.IsTeamFlat {α : Type u_1} (T : TeamSet α) : Prop

A team-set T is flat iff its membership reduces pointwise: s ∈ T ↔ every singleton drawn from s is in T.

Anttila Definition 2.2.1 (using "for all w ∈ s" — the standard Yang-Väänänen formulation).

Equivalently: T is the principal lower set generated by its singletons (proved by isTeamFlat_iff_lower_supClosed_empty).

Equations

• Core.Logic.Team.IsTeamFlat T = ∀ (s : Finset α), s ∈ T ↔ ∀ w ∈ s, {w} ∈ T

theorem Core.Logic.Team.isTeamFlat_iff_isLowerSet_supClosed_empty {α : Type u_1} [DecidableEq α] (T : TeamSet α) : IsTeamFlat T ↔ IsLowerSet T ∧ SupClosed T ∧ ∅ ∈ T

Anttila Proposition 2.2.2 at the substrate level: a team-set is flat iff it is downward-closed under inclusion (IsLowerSet), closed under binary union (SupClosed), and contains the empty team.

No formula or model parameters — this is a pure lattice-theoretic fact about subsets of Finset α under inclusion + union.

The forward direction (flatness implies the three closure properties) is by case analysis on s ∈ T. The backward direction (the three properties imply flatness) inducts on s (Finset induction): empty case uses HasEmpty, insert case uses SupClosed to combine the singleton with the inductive hypothesis.

theorem Core.Logic.Team.isTeamFlat_of_isLowerSet_supClosed_empty {α : Type u_1} [DecidableEq α] (T : TeamSet α) (hLower : IsLowerSet T) (hSup : SupClosed T) (hEmpty : ∅ ∈ T) : IsTeamFlat T

Backward direction extracted as a constructor: the three closure properties imply flatness. The most-used direction in consumers.

theorem Core.Logic.Team.IsTeamFlat.isLowerSet {α : Type u_1} [DecidableEq α] {T : TeamSet α} (h : IsTeamFlat T) : IsLowerSet T

Forward extraction: flat team-sets are downward-closed.

theorem Core.Logic.Team.IsTeamFlat.supClosed {α : Type u_1} [DecidableEq α] {T : TeamSet α} (h : IsTeamFlat T) : SupClosed T

Forward extraction: flat team-sets are sup-closed.

theorem Core.Logic.Team.IsTeamFlat.hasEmpty {α : Type u_1} [DecidableEq α] {T : TeamSet α} (h : IsTeamFlat T) : ∅ ∈ T

Forward extraction: flat team-sets contain the empty team.

@[reducible, inline]

abbrev Core.Logic.Team.TeamPred (α : Type u_2) : Type u_2

A team predicate: a Finset α → Prop. Equivalent to TeamSet α via set-builder, but more ergonomic for consumers who think of support M φ as a function from teams to propositions.

The closure properties on a TeamPred are defined as the corresponding properties on { t | P t } : TeamSet α.

Equations

• Core.Logic.Team.TeamPred α = (Finset α → Prop)

def Core.Logic.Team.TeamPred.IsDownward {α : Type u_2} (P : TeamPred α) : Prop

A team-predicate is downward-closed iff { t | P t } is a lower set under inclusion. Wraps mathlib's IsLowerSet; the underlying definition is ∀ a b, a ⊆ b → P b → P a.

Equations

• P.IsDownward = IsLowerSet {t : Finset α | P t}

def Core.Logic.Team.TeamPred.IsSupClosed {α : Type u_2} [DecidableEq α] (P : TeamPred α) : Prop

A team-predicate is sup-closed iff { t | P t } is closed under binary union. Wraps mathlib's SupClosed (with ⊔ = ∪ on Finset); underlying: ∀ a b, P a → P b → P (a ∪ b).

Equations

• P.IsSupClosed = SupClosed {t : Finset α | P t}

def Core.Logic.Team.TeamPred.HasEmpty {α : Type u_2} (P : TeamPred α) : Prop

A team-predicate has empty iff the empty team satisfies it.

Equations

• P.HasEmpty = P ∅

def Core.Logic.Team.TeamPred.IsFlat {α : Type u_2} (P : TeamPred α) : Prop

A team-predicate is flat iff its membership reduces pointwise: P s ↔ ∀ w ∈ s, P {w}. Wraps IsTeamFlat on { t | P t }.

Equations

• P.IsFlat = Core.Logic.Team.IsTeamFlat {t : Finset α | P t}

theorem Core.Logic.Team.TeamPred.isFlat_iff {α : Type u_2} [DecidableEq α] (P : TeamPred α) : P.IsFlat ↔ P.IsDownward ∧ P.IsSupClosed ∧ P.HasEmpty

Anttila Proposition 2.2.2 in TeamPred form: a team-predicate is flat iff it is downward-closed, sup-closed, and has the empty team. Direct corollary of the TeamSet-level theorem.

theorem Core.Logic.Team.TeamPred.isFlat_of_isDownward_isSupClosed_hasEmpty {α : Type u_2} [DecidableEq α] (P : TeamPred α) (h_down : P.IsDownward) (h_sup : P.IsSupClosed) (h_empty : P.HasEmpty) : P.IsFlat

Constructor: combine the three closure properties to get flatness.

theorem Core.Logic.Team.TeamPred.IsFlat.isDownward {α : Type u_2} [DecidableEq α] {P : TeamPred α} (h : P.IsFlat) : P.IsDownward

Forward extraction: flat team-predicates are downward-closed.

theorem Core.Logic.Team.TeamPred.IsFlat.isSupClosed {α : Type u_2} [DecidableEq α] {P : TeamPred α} (h : P.IsFlat) : P.IsSupClosed

Forward extraction: flat team-predicates are sup-closed.

theorem Core.Logic.Team.TeamPred.IsFlat.hasEmpty {α : Type u_2} [DecidableEq α] {P : TeamPred α} (h : P.IsFlat) : P.HasEmpty

Forward extraction: flat team-predicates have the empty team.

theorem Core.Logic.Team.TeamPred.isDownward_iff_pointwise {α : Type u_2} [DecidableEq α] (P : TeamPred α) : P.IsDownward ↔ ∀ ⦃a b : Finset α⦄, a ⊆ b → P b → P a

Pointwise form of IsDownward: a team-predicate is downward-closed iff ∀ a b, a ⊆ b → P b → P a. Just unfolds IsLowerSet for the { t | P t } instance — Finset α's ≤ is ⊆.

theorem Core.Logic.Team.TeamPred.isSupClosed_iff_pointwise {α : Type u_2} [DecidableEq α] (P : TeamPred α) : P.IsSupClosed ↔ ∀ ⦃a : Finset α⦄, P a → ∀ ⦃b : Finset α⦄, P b → P (a ∪ b)

Pointwise form of IsSupClosed: ∀ a b, P a → P b → P (a ∪ b).

theorem Core.Logic.Team.TeamPred.isFlat_iff_pointwise {α : Type u_2} [DecidableEq α] (P : TeamPred α) : P.IsFlat ↔ ∀ (s : Finset α), P s ↔ ∀ w ∈ s, P {w}

Pointwise form of IsFlat: ∀ s, P s ↔ ∀ w ∈ s, P {w}.