The flat domain

Flat α is Option α carrying the flat order: ⊥ (none, no information) below everything, distinct values incomparable. An order-carrying alias in the WithBot mold, but the underlying order is discrete, not lifted — committed values are an antichain.

This is the free (Scott) domain on a set: the lift of the discrete order, Flat = lift ∘ discrete, equivalently 1 + α as an object. Two facts make it the canonical small domain rather than an ad-hoc gadget:

• it is bounded-complete but not a lattice — meets are total (SemilatticeInf, agreement or ⊥) while joins are partial (PartialUnify: ⊥ is identity, equal commitments merge, distinct commitments have no upper bound). Bounded-completeness is the join being partial-yet-unique-when-defined;
• it is ω-complete (OmegaCompletePartialOrder) — chains are eventually constant, so they have suprema. Flat is the generator of domain theory and the order side of the lifting/partiality monad (Option), whose Kleisli arrows α → Flat β are partial functions — PartialUnify.unify among them.

Linguistically it is one atomic feature slot: the order is [Shi86]'s and [Car92]'s subsumption order (an information order — ⊥ = unmarked, a wildcard for agreement), and Flat Bool is the knowledge order of Kleene three-valued logic. Feature bundles are built from it by the Pi PartialUnify instance; Compat is consistency.

The order skeleton (Option.FlatLE, Flat, the PartialOrder/OrderBot/ SemilatticeInf/OmegaCompletePartialOrder instances) is an [UPSTREAM] candidate for Mathlib/Order/Flat.lean — root-level Flat as with WithBot, coexisting with the existing namespaced Module.Flat and ConvexCone.Flat (write _root_.Flat under open Module). The PartialUnify instance and compat_iff stay here: PartialUnify is linglib's, not mathlib's.

Main declarations

• Option.FlatLE — the flat order as a relation on Option α
• Flat — the order-carrying alias, with PartialOrder, OrderBot, SemilatticeInf, OmegaCompletePartialOrder, and PartialUnify instances
• Flat.coe_le_coe, Flat.not_coe_le_bot — the order, characterized
• Flat.ωSup_mem_range — chains attain their supremum (the domain has height ≤ 2)
• Flat.ωScottContinuous_of_monotone — monotone maps out of Flat are continuous
• Flat.liftEquiv — the free-domain universal property: functions α → D are exactly strict continuous maps Flat α →𝒄 D
• Flat.compat_iff — slot compatibility (Compat), characterized
• Flat.unify_distinct_eq_none — distinct atoms do not unify (the non-distributivity witness)

TODO

The free-domain universal property is now liftEquiv (with its enabling lemma ωScottContinuous_of_monotone). The remaining domain-theoretic program:

• Categorical freeness. Package liftEquiv as a free–forgetful adjunction between Type and the pointed ωCPO category — Flat ⊣ U (template: mathlib's latToBddLatForgetAdjunction, the free bounded lattice via WithBot).
• Lifting monad. Give Flat (= Option) its ω-CPO monad structure — the partiality/lifting monad — whose Kleisli arrows α → Flat β are partial continuous functions; PartialUnify.unify is one, which is why it composes through Option.bind (unify_assoc). (mathlib has this for Part.)
• Algebraicity / bounded-completeness. Every element of Flat α is compact, making it an algebraic (finite-height) bounded-complete domain — the Scott-domain packaging of the partial join PartialUnify provides.
• Three-valued logic. Flat Bool is the knowledge order of Kleene three-valued logic; the strong-Kleene connectives are exactly its continuous maps. Connects this substrate to the trivalence/presupposition layer.

Ergonomics, separately: add a coercion ↑ : α → Flat α (as WithBot.some) so coe_le_coe/not_coe_le_bot need no explicit @LE.le, and move the order relation out of the Option namespace (Option.FlatLE → Flat.LE).

def Option.FlatLE {α : Type u_1} (a b : Option α) : Prop

The flat information order on an atomic feature slot: every committed value persists upward, so none is below everything and distinct atoms are incomparable.

Equations

• a.FlatLE b = ∀ (x : α), a = some x → b = some x

theorem Option.FlatLE.refl {α : Type u_1} (a : Option α) : a.FlatLE a

theorem Option.FlatLE.trans {α : Type u_1} {a b c : Option α} (h1 : a.FlatLE b) (h2 : b.FlatLE c) : a.FlatLE c

theorem Option.FlatLE.antisymm {α : Type u_1} {a b : Option α} (h1 : a.FlatLE b) (h2 : b.FlatLE a) : a = b

theorem Option.FlatLE.none_le {α : Type u_1} (b : Option α) : none.FlatLE b

@[implicit_reducible]

instance Option.FlatLE.instDecidableOfDecidableEq {α : Type u_1} {a b : Option α} [DecidableEq α] : Decidable (a.FlatLE b)

Equations

• Option.FlatLE.instDecidableOfDecidableEq = isTrue ⋯
• Option.FlatLE.instDecidableOfDecidableEq = if h : x = y then isTrue ⋯ else isFalse ⋯
• Option.FlatLE.instDecidableOfDecidableEq = isFalse ⋯

def Flat (α : Type u_1) : Type u_1

An atomic feature slot: Option α carrying the flat information order as its ≤. A def, not an abbrev, so the order instances do not leak onto bare Option.

Equations

• Flat α = Option α

@[implicit_reducible]

instance Flat.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Flat α)

Equations

• Flat.instDecidableEq = Flat.instDecidableEq._aux_1

@[implicit_reducible]

instance Flat.instBEq {α : Type u_1} [BEq α] : BEq (Flat α)

Equations

• Flat.instBEq = { beq := Flat.instBEq._aux_1 }

instance Flat.instLawfulBEq {α : Type u_1} [BEq α] [LawfulBEq α] : LawfulBEq (Flat α)

@[implicit_reducible]

instance Flat.instRepr {α : Type u_1} [Repr α] : Repr (Flat α)

Equations

• Flat.instRepr = { reprPrec := Flat.instRepr._aux_1 }

@[implicit_reducible]

instance Flat.instInhabited {α : Type u_1} : Inhabited (Flat α)

Equations

• Flat.instInhabited = { default := none }

@[implicit_reducible]

instance Flat.instPartialOrder {α : Type u_1} : PartialOrder (Flat α)

Equations

• Flat.instPartialOrder = { le := fun (a b : Flat α) => Option.FlatLE a b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[implicit_reducible]

instance Flat.instOrderBot {α : Type u_1} : OrderBot (Flat α)

Equations

• Flat.instOrderBot = { bot := none, bot_le := ⋯ }

@[implicit_reducible]

instance Flat.instDecidableLeOfDecidableEq {α : Type u_1} [DecidableEq α] (a b : Flat α) : Decidable (a ≤ b)

Equations

• a.instDecidableLeOfDecidableEq b = Option.FlatLE.instDecidableOfDecidableEq

theorem Flat.le_def {α : Type u_1} {a b : Flat α} : a ≤ b ↔ Option.FlatLE a b

theorem Flat.none_eq_bot {α : Type u_1} : none = ⊥

@[simp]

theorem Flat.coe_le_coe {α : Type u_1} {a b : α} : some a ≤ some b ↔ a = b

@[simp]

theorem Flat.not_coe_le_bot {α : Type u_1} (a : α) : ¬some a ≤ ⊥

def Flat.inf {α : Type u_1} [DecidableEq α] (a b : Flat α) : Flat α

The meet of two slots: their agreement, or nothing.

Equations

• a.inf b = if a = b then a else none

@[implicit_reducible]

instance Flat.instSemilatticeInfOfDecidableEq {α : Type u_1} [DecidableEq α] : SemilatticeInf (Flat α)

Equations

• Flat.instSemilatticeInfOfDecidableEq = { toPartialOrder := Flat.instPartialOrder, inf := Flat.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

The flat domain is ω-complete

A monotone chain in the flat order is eventually constant — ⊥ until it (optionally) commits to a single value, then constant — so it has a supremum. This is the flat domain, the canonical nontrivial example of an OmegaCompletePartialOrder.

@[implicit_reducible]

noncomputable instance Flat.instOmegaCompletePartialOrder {α : Type u_1} : OmegaCompletePartialOrder (Flat α)

The flat domain is an OmegaCompletePartialOrder: chains are eventually constant, so their suprema are the eventual value (or ⊥).

Equations

• Flat.instOmegaCompletePartialOrder = { toPartialOrder := Flat.instPartialOrder, ωSup := Flat.ωSupImpl✝, le_ωSup := ⋯, ωSup_le := ⋯ }

theorem Flat.ωSup_mem_range {α : Type u_1} (c : OmegaCompletePartialOrder.Chain (Flat α)) : OmegaCompletePartialOrder.ωSup c ∈ Set.range ⇑c

Chains in the flat domain attain their supremum — ωSup c is some c i: the domain has height ≤ 2.

theorem Flat.ωScottContinuous_of_monotone {α : Type u_1} {D : Type u_2} [OmegaCompletePartialOrder D] {f : Flat α → D} (hf : Monotone f) : OmegaCompletePartialOrder.ωScottContinuous f

Every monotone map out of the flat domain is ωScottContinuous: chains attain their suprema (ωSup_mem_range), so continuity is automatic. This is the key fact behind the universal property liftEquiv.

noncomputable def Flat.liftEquiv {α : Type u_1} {D : Type u_2} [OmegaCompletePartialOrder D] [OrderBot D] : (α → D) ≃ { f : Flat α →𝒄 D // f ⊥ = ⊥ }

The flat domain is free. Strict continuous maps out of Flat α into a pointed domain D are exactly functions α → D — the universal property of the free domain. The forward map precomposes with some; the inverse extends by ⊥ ↦ ⊥, continuous by ωScottContinuous_of_monotone.

Equations

• One or more equations did not get rendered due to their size.

def Flat.unify {α : Type u_1} [DecidableEq α] (a b : Flat α) : Option (Flat α)

Unify two slots: none is identity, equal commitments merge, distinct commitments clash.

Equations

• Flat.unify none b = some b
• Flat.unify (some x) none = some (some x)
• Flat.unify (some x) (some y) = if x = y then some (some x) else none

@[implicit_reducible]

instance Flat.instPartialUnifyOfDecidableEq {α : Type u_1} [DecidableEq α] : PartialUnify (Flat α)

Equations

• Flat.instPartialUnifyOfDecidableEq = { unify := Flat.unify, isLUB_of_unify_eq_some := ⋯, isSome_unify_of_bddAbove := ⋯ }

theorem Flat.compat_iff {α : Type u_1} [DecidableEq α] {a b : Flat α} : Compat a b ↔ ∀ (x : α), a = some x → ∀ (y : α), b = some y → x = y

Slot compatibility, characterized: committed values must coincide; an uncommitted slot is a wildcard.

Non-distributivity

The flat order is not distributive: three distinct atoms (with a top adjoined) form the diamond M₃ — [Car92] takes subsumption orders to be neither distributive nor modular in general. Flat carries only the partial join (PartialUnify), so the distributive law cannot even be stated on it directly; unify_distinct_eq_none is the witness — distinct atoms have no upper bound, so the join the law would require is undefined.

theorem Flat.unify_distinct_eq_none {α : Type u_1} [DecidableEq α] {a b : α} (h : a ≠ b) : Flat.unify (some a) (some b) = none