The unconditional three-antichain obstruction

This file combines the selectable consecutive-antichain extension with the global three-line construction and selectable support chain.

structure MagnitudeConjecture.PosetSpace.ConsecutiveAntichainBlockFor {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) : Prop

A consecutive three-position block in a selectable reverse enumeration which is an antichain in the original poset.

• le_eq_of_mem_block {s t : T} : q ≤ ↑(ReverseEnumeration.index T R s) → ↑(ReverseEnumeration.index T R s) ≤ q + 2 → q ≤ ↑(ReverseEnumeration.index T R t) → ↑(ReverseEnumeration.index T R t) ≤ q + 2 → s ≤ t → s = t

theorem MagnitudeConjecture.PosetSpace.consecutiveAntichainBlockForOfThree {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) {a b c : T} (H : IsThreeAntichain a b c) (q : ℕ) (hq : q + 2 < Fintype.card T) (ha : ↑(ReverseEnumeration.index T R a) = q) (hb : ↑(ReverseEnumeration.index T R b) = q + 1) (hc : ↑(ReverseEnumeration.index T R c) = q + 2) : ConsecutiveAntichainBlockFor R q hq

Three prescribed consecutive antichain elements certify that their positions form an antichain block.

def MagnitudeConjecture.PosetSpace.blockPlaneSubspaceFor (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (t : T) : Submodule k (k × k)

The global full/axes/diagonal/zero plane for a block in a selectable enumeration.

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.blockThreeLinePlaneFor (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : Obj k T

The global two-dimensional T-space for a selectable consecutive antichain block.

def MagnitudeConjecture.PosetSpace.blockInMapFor (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : supportLineFor k T R ⟨q + 1, ⋯⟩ ⟶ blockThreeLinePlaneFor k R q hq D

The selected-block map 1 ↦ e₁.

def MagnitudeConjecture.PosetSpace.blockOutMapFor (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : blockThreeLinePlaneFor k R q hq D ⟶ supportLineFor k T R ⟨q + 2, ⋯⟩

The selected-block map (x,y) ↦ x-y.

theorem MagnitudeConjecture.PosetSpace.blockInMapFor_ne_zero (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : blockInMapFor k R q hq D ≠ 0

theorem MagnitudeConjecture.PosetSpace.blockOutMapFor_ne_zero (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : blockOutMapFor k R q hq D ≠ 0

theorem MagnitudeConjecture.PosetSpace.blockInMapFor_not_isIso (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : ¬CategoryTheory.IsIso (blockInMapFor k R q hq D)

theorem MagnitudeConjecture.PosetSpace.blockOutMapFor_not_isIso (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : ¬CategoryTheory.IsIso (blockOutMapFor k R q hq D)

theorem MagnitudeConjecture.PosetSpace.blockThreeLinePlaneFor_isSchur (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : IsSchur k T (blockThreeLinePlaneFor k R q hq D)

The selectable global three-line plane is Schur.

def MagnitudeConjecture.PosetSpace.ConsecutiveAntichainBlockFor.selectableSchurDetour (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (R : ReverseEnumeration T) (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlockFor R q hq) : SelectableSchurDetour k T R q hq

A selected consecutive block constructs the selectable Schur detour.

theorem MagnitudeConjecture.PosetSpace.card_add_one_le_of_threeAntichain (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] {a b c : T} {L : ℕ} (H : IsThreeAntichain a b c) (G : PositiveGrading (Obj k T) (IsSchur k T) L) : Fintype.card T + 1 ≤ L

The manuscript's strict realization bound whenever the poset contains a three-element antichain.