Reverse linear extensions with a consecutive antichain block

This file constructs the order extension invoked in the equality argument of the frozen manuscript: any specified three-element antichain can be made a consecutive block in a reverse linear extension.

structure MagnitudeConjecture.PosetSpace.IsThreeAntichain {T : Type u} [PartialOrder T] (a b c : T) : Prop

Three specified elements are pairwise incomparable.

• not_ab : ¬a ≤ b
• not_ba : ¬b ≤ a
• not_ac : ¬a ≤ c
• not_ca : ¬c ≤ a
• not_bc : ¬b ≤ c
• not_cb : ¬c ≤ b

theorem MagnitudeConjecture.PosetSpace.IsThreeAntichain.ne_ab {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : a ≠ b

theorem MagnitudeConjecture.PosetSpace.IsThreeAntichain.ne_ac {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : a ≠ c

theorem MagnitudeConjecture.PosetSpace.IsThreeAntichain.ne_bc {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : b ≠ c

@[instance_reducible]

noncomputable def MagnitudeConjecture.PosetSpace.instDecidableEq_magnitudeConjecture {T : Type u} : DecidableEq T

@[instance_reducible]

noncomputable def MagnitudeConjecture.PosetSpace.instDecidable_magnitudeConjecture (p : Prop) : Decidable p

def MagnitudeConjecture.PosetSpace.aboveThree {T : Type u} [PartialOrder T] (a b c x : T) : Prop

Elements forced before the antichain block in a reverse extension are those strictly above at least one of its elements.

noncomputable def MagnitudeConjecture.PosetSpace.antichainBlockRank {T : Type u} [PartialOrder T] (a b c x : T) : ℕ

Five-layer rank: elements above the antichain, the three specified elements in order, and all remaining elements.

theorem MagnitudeConjecture.PosetSpace.not_aboveThree_a {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : ¬aboveThree a b c a

theorem MagnitudeConjecture.PosetSpace.not_aboveThree_b {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : ¬aboveThree a b c b

theorem MagnitudeConjecture.PosetSpace.not_aboveThree_c {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : ¬aboveThree a b c c

@[simp]

theorem MagnitudeConjecture.PosetSpace.antichainBlockRank_a {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : antichainBlockRank a b c a = 1

@[simp]

theorem MagnitudeConjecture.PosetSpace.antichainBlockRank_b {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : antichainBlockRank a b c b = 2

@[simp]

theorem MagnitudeConjecture.PosetSpace.antichainBlockRank_c {T : Type u} [PartialOrder T] {a b c : T} (H : IsThreeAntichain a b c) : antichainBlockRank a b c c = 3

theorem MagnitudeConjecture.PosetSpace.antichainBlockRank_anti {T : Type u} [PartialOrder T] {a b c x y : T} (H : IsThreeAntichain a b c) (hxy : y ≤ x) : antichainBlockRank a b c x ≤ antichainBlockRank a b c y

The block rank reverses the original partial order.

def MagnitudeConjecture.PosetSpace.antichainBlockRel {T : Type u} [PartialOrder T] (a b c x y : T) : Prop

Lexicographic refinement of the reverse partial order by the five-layer block rank.

instance MagnitudeConjecture.PosetSpace.antichainBlockRel_isPartialOrder {T : Type u} [PartialOrder T] (a b c : T) : IsPartialOrder T (antichainBlockRel a b c)

theorem MagnitudeConjecture.PosetSpace.antichainBlockRel_of_ge {T : Type u} [PartialOrder T] {a b c x y : T} (H : IsThreeAntichain a b c) (hxy : y ≤ x) : antichainBlockRel a b c x y

structure MagnitudeConjecture.PosetSpace.AntichainBlockCarrier {T : Type u} (a b c : T) : Type u

A wrapped copy of T on which the block-refined reverse order can be installed without replacing the original order on T.

• value : T

def MagnitudeConjecture.PosetSpace.AntichainBlockCarrier.equiv {T : Type u} (a b c : T) : AntichainBlockCarrier a b c ≃ T

Forgetting the wrapper is an equivalence with the original poset.

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.AntichainBlockCarrier.instFintype {T : Type u} [Fintype T] (a b c : T) : Fintype (AntichainBlockCarrier a b c)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.AntichainBlockCarrier.instPartialOrder {T : Type u} [PartialOrder T] (a b c : T) : PartialOrder (AntichainBlockCarrier a b c)

The partial order on the wrapped carrier is the five-layer refinement of the reverse order.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.AntichainBlockLinearExtension {T : Type u} (a b c : T) : Type u

The chosen linear extension of the block-refined reverse order.

def MagnitudeConjecture.PosetSpace.antichainBlockLinearExtensionEquiv {T : Type u} (a b c : T) : AntichainBlockLinearExtension a b c ≃ T

Forgetting both order-extension wrappers recovers the original poset.

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instFintypeAntichainBlockLinearExtension {T : Type u} [Fintype T] (a b c : T) : Fintype (AntichainBlockLinearExtension a b c)

noncomputable def MagnitudeConjecture.PosetSpace.antichainBlockOrderIso {T : Type u} [PartialOrder T] [Fintype T] (a b c : T) : Fin (Fintype.card T) ≃o AntichainBlockLinearExtension a b c

The increasing enumeration of the chosen block-refined linear order.

noncomputable def MagnitudeConjecture.PosetSpace.antichainBlockIndex {T : Type u} [PartialOrder T] [Fintype T] (a b c x : T) : Fin (Fintype.card T)

The position of an original element in the block-refined linear extension.

theorem MagnitudeConjecture.PosetSpace.antichainBlockIndex_le_of_rel {T : Type u} [PartialOrder T] [Fintype T] {a b c x y : T} (hxy : antichainBlockRel a b c x y) : antichainBlockIndex a b c x ≤ antichainBlockIndex a b c y

theorem MagnitudeConjecture.PosetSpace.antichainBlockIndex_lt_of_rel {T : Type u} [PartialOrder T] [Fintype T] {a b c x y : T} (hxy : antichainBlockRel a b c x y) (hne : x ≠ y) : antichainBlockIndex a b c x < antichainBlockIndex a b c y

theorem MagnitudeConjecture.PosetSpace.antichainBlockRel_other {T : Type u} [PartialOrder T] {a b c x : T} (H : IsThreeAntichain a b c) (hxa : x ≠ a) (hxb : x ≠ b) (hxc : x ≠ c) : antichainBlockRel a b c x a ∨ antichainBlockRel a b c c x

Every element outside the chosen triple lies wholly before or wholly after the block in the refined partial order.

noncomputable def MagnitudeConjecture.PosetSpace.antichainBlockReverseEnumeration {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} (H : IsThreeAntichain a b c) : ReverseEnumeration T

The reverse enumeration obtained by linearly extending the block-refined order.

@[simp]

theorem MagnitudeConjecture.PosetSpace.antichainBlockReverseEnumeration_index {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} (H : IsThreeAntichain a b c) (x : T) : ReverseEnumeration.index T (antichainBlockReverseEnumeration H) x = antichainBlockIndex a b c x

theorem MagnitudeConjecture.PosetSpace.antichainBlockIndex_b_eq_add_one {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} (H : IsThreeAntichain a b c) : ↑(antichainBlockIndex a b c b) = ↑(antichainBlockIndex a b c a) + 1

In the selected reverse enumeration, b immediately follows a.

theorem MagnitudeConjecture.PosetSpace.antichainBlockIndex_c_eq_add_one {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} (H : IsThreeAntichain a b c) : ↑(antichainBlockIndex a b c c) = ↑(antichainBlockIndex a b c b) + 1

In the selected reverse enumeration, c immediately follows b.

theorem MagnitudeConjecture.PosetSpace.exists_reverseEnumeration_three_consecutive {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} (H : IsThreeAntichain a b c) : ∃ (R : ReverseEnumeration T) (q : ℕ), q + 2 < Fintype.card T ∧ ↑(ReverseEnumeration.index T R a) = q ∧ ↑(ReverseEnumeration.index T R b) = q + 1 ∧ ↑(ReverseEnumeration.index T R c) = q + 2

Any chosen three-element antichain occurs as a consecutive block in a selectable reverse linear enumeration.