Partial-Rank Orders

The partial order induced by a partial rank function r : α → Option β: ranked elements compare by strict rank comparison, unranked elements are isolated — comparable only to themselves.

This is the order-theoretic gadget behind linguistic hierarchies that are deliberately silent on part of the inventory: Caha's case-containment order (Syntax/Case/Order.lean) ranks NOM < ACC < GEN < DAT < LOC and says nothing about ERG or ABS, and the silence is theoretical content.

No pullback produces this. Preorder.lift through r (the PullbackPreorder construction) would make all unranked elements mutually equivalent — r a = r b = none gives a ≤ b ≤ a — losing antisymmetry and the isolation.

The order structure itself is mathlib's: RankLT is a strict order (IsStrictOrder instance below), so partialOrderOfRank is partialOrderOfSO (RankLT r) and RankLE (a = b ∨ RankLT r a b) is exactly the reflexive-closure shape partialOrderOfSO uses for ≤. This file's value-add is RankLT itself, its decidability, and the isolation lemmas. There is no total variant: isolation precludes totality whenever any element is unranked.

Main declarations

• Core.Order.RankLT — strict comparison through a partial rank
• Core.Order.RankLE — its reflexive closure
• Core.Order.rankLE_iff_eq_left/rankLE_iff_eq_right — isolation: an unranked element is ≤-related only to itself
• Core.Order.partialOrderOfRank — partialOrderOfSO at RankLT r; < is definitionally RankLT and ≤ is RankLE
• Core.Order.rankShells — the canonical down-set decomposition Iic ∘ r, and rankLT_iff_rankShells: the rank order is the shadow of inclusion between the down-sets (the structural fact behind nanosyntactic "feature stack" decompositions, replacing per-instance stipulate-a-table-and-decide)

def Core.Order.RankLT {α : Type u_1} {β : Type u_2} (r : α → Option β) [LT β] (a b : α) : Prop

Strict comparison through a partial rank: both elements are ranked and the ranks compare strictly. Unranked elements relate to nothing.

Equations

• Core.Order.RankLT r a b = match r a, r b with | some x, some y => x < y | x, x_1 => False

def Core.Order.RankLE {α : Type u_1} {β : Type u_2} (r : α → Option β) [LT β] (a b : α) : Prop

Non-strict comparison through a partial rank: the reflexive closure of RankLT. Unranked elements are isolated — ≤-related only to themselves.

Equations

• Core.Order.RankLE r a b = (a = b ∨ Core.Order.RankLT r a b)

@[implicit_reducible]

instance Core.Order.instDecidableRelRankLTOfLt {α : Type u_1} {β : Type u_2} (r : α → Option β) [LT β] [DecidableRel fun (x1 x2 : β) => x1 < x2] : DecidableRel (RankLT r)

Equations

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

@[implicit_reducible]

instance Core.Order.instDecidableRelRankLEOfDecidableEqOfLt {α : Type u_1} {β : Type u_2} (r : α → Option β) [LT β] [DecidableEq α] [DecidableRel fun (x1 x2 : β) => x1 < x2] : DecidableRel (RankLE r)

Equations

• Core.Order.instDecidableRelRankLEOfDecidableEqOfLt r x✝¹ x✝ = Core.Order.instDecidableRelRankLEOfDecidableEqOfLt._aux_1 r x✝¹ x✝

theorem Core.Order.rankLT_iff {α : Type u_1} {β : Type u_2} {r : α → Option β} [LT β] {a b : α} : RankLT r a b ↔ ∃ (x : β) (y : β), r a = some x ∧ r b = some y ∧ x < y

theorem Core.Order.rankLE_iff_eq_left {α : Type u_1} {β : Type u_2} {r : α → Option β} [LT β] {a b : α} (h : r a = none) : RankLE r a b ↔ a = b

An unranked element is ≤-related only to itself (left).

theorem Core.Order.rankLE_iff_eq_right {α : Type u_1} {β : Type u_2} {r : α → Option β} [LT β] {a b : α} (h : r b = none) : RankLE r a b ↔ a = b

An unranked element is ≤-related only to itself (right).

theorem Core.Order.RankLT.trans {α : Type u_1} {β : Type u_2} {r : α → Option β} [Preorder β] {a b c : α} (hab : RankLT r a b) (hbc : RankLT r b c) : RankLT r a c

theorem Core.Order.rankLT_irrefl {α : Type u_1} {β : Type u_2} {r : α → Option β} [Preorder β] (a : α) : ¬RankLT r a a

instance Core.Order.instIsStrictOrderRankLT {α : Type u_1} {β : Type u_2} (r : α → Option β) [Preorder β] : IsStrictOrder α (RankLT r)

RankLT is a strict order — the bridge to mathlib's order constructors.

@[reducible, inline]

abbrev Core.Order.partialOrderOfRank {α : Type u_1} {β : Type u_2} (r : α → Option β) [Preorder β] : PartialOrder α

The partial order induced by a partial rank: partialOrderOfSO at RankLT r, so < is definitionally RankLT r and ≤ is RankLE r. Intended for scoped instances: a theoretical hierarchy is borne by a feature type as an opt-in commitment, never as a global instance.

See note [reducible non-instances].

Equations

• Core.Order.partialOrderOfRank r = partialOrderOfSO (Core.Order.RankLT r)

def Core.Order.rankShells {α : Type u_1} {ι : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] (r : α → Option ι) (a : α) : Option (Finset ι)

The canonical down-set decomposition of a partial rank: an element's content is the initial segment Finset.Iic of its rank (its "shell stack"; cf. the order-theoretic primitive LowerSet.Iic). For a rank into a chain an element is this down-set, and the rank order is the shadow of inclusion between the down-sets (rankLT_iff_rankShells). The structure behind nanosyntactic feature-stack decompositions (Syntax/Case/Order.lean).

Equations

• Core.Order.rankShells r a = Option.map Finset.Iic (r a)

theorem Core.Order.rankLT_iff_rankShells {α : Type u_1} {ι : Type u_3} [Preorder ι] [LocallyFiniteOrderBot ι] (r : α → Option ι) (a b : α) : RankLT r a b ↔ RankLT (rankShells r) a b

The rank order is the shadow of its down-set decomposition. Strict-rank comparison through r coincides with strict inclusion of the shell stacks rankShells r — Finset.Iic being strictly monotone (Finset.Iic_ssubset_Iic). Generic over any rank into a locally-finite-below preorder, replacing per-instance "stipulate a shells table + decide it agrees with the rank".