The three-antichain path in finite poset spaces

This file formalizes the characteristic-free five-object path through the two-dimensional three-line configuration used in the equality argument of the frozen manuscript.

inductive MagnitudeConjecture.PosetSpace.Three (α : Type u) : Type u

The discrete three-element poset underlying the local antichain obstruction. The phantom parameter keeps it in the same universe as the field, as required by the literal T-space category.

• first {α : Type u} : Three α
• second {α : Type u} : Three α
• third {α : Type u} : Three α

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instDecidableEqThree {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Three α✝)

def MagnitudeConjecture.PosetSpace.instDecidableEqThree.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Three α✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance MagnitudeConjecture.PosetSpace.instPartialOrderThree {α : Type u} : PartialOrder (Three α)

theorem MagnitudeConjecture.PosetSpace.three_isUpperSet {α : Type u} (U : Set (Three α)) : IsUpperSet U

def MagnitudeConjecture.PosetSpace.firstAxis (k : Type u) [Field k] : Submodule k (k × k)

The first coordinate axis in k².

def MagnitudeConjecture.PosetSpace.secondAxis (k : Type u) [Field k] : Submodule k (k × k)

The second coordinate axis in k².

def MagnitudeConjecture.PosetSpace.diagonal (k : Type u) [Field k] : Submodule k (k × k)

The diagonal line in k².

@[simp]

theorem MagnitudeConjecture.PosetSpace.mem_firstAxis_iff (k : Type u) [Field k] (x : k × k) : x ∈ firstAxis k ↔ x.2 = 0

@[simp]

theorem MagnitudeConjecture.PosetSpace.mem_secondAxis_iff (k : Type u) [Field k] (x : k × k) : x ∈ secondAxis k ↔ x.1 = 0

@[simp]

theorem MagnitudeConjecture.PosetSpace.mem_diagonal_iff (k : Type u) [Field k] (x : k × k) : x ∈ diagonal k ↔ x.1 = x.2

@[reducible, inline]

abbrev MagnitudeConjecture.PosetSpace.threeLinePlane (k : Type u) [Field k] : Obj k (Three k)

The manuscript's indecomposable two-dimensional three-line space.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathObj0 (k : Type u) [Field k] : Obj k (Three k)

Empty-support scalar space.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathObj1 (k : Type u) [Field k] : Obj k (Three k)

Scalar space supported at the first antichain point.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathObj3 (k : Type u) [Field k] : Obj k (Three k)

Scalar space supported at the first two antichain points.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathObj4 (k : Type u) [Field k] : Obj k (Three k)

Full-support scalar space.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathMap01 (k : Type u) [Field k] : threePathObj0 k ⟶ threePathObj1 k

First strict support inclusion in the three-antichain path.

def MagnitudeConjecture.PosetSpace.threePathMap12 (k : Type u) [Field k] : threePathObj1 k ⟶ threeLinePlane k

The map 1 ↦ e₁ into the three-line plane.

def MagnitudeConjecture.PosetSpace.threePathMap23 (k : Type u) [Field k] : threeLinePlane k ⟶ threePathObj3 k

The map (x,y) ↦ x-y; it kills the diagonal line even in characteristic two.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.threePathMap34 (k : Type u) [Field k] : threePathObj3 k ⟶ threePathObj4 k

Final strict support inclusion in the three-antichain path.

@[simp]

theorem MagnitudeConjecture.PosetSpace.threePathMap12_apply (k : Type u) [Field k] (x : k) : (threePathMap12 k).linear x = (x, 0)

@[simp]

theorem MagnitudeConjecture.PosetSpace.threePathMap23_apply (k : Type u) [Field k] (x : k × k) : (threePathMap23 k).linear x = x.1 - x.2

theorem MagnitudeConjecture.PosetSpace.threePathMap12_ne_zero (k : Type u) [Field k] : threePathMap12 k ≠ 0

theorem MagnitudeConjecture.PosetSpace.threePathMap01_ne_zero (k : Type u) [Field k] : threePathMap01 k ≠ 0

theorem MagnitudeConjecture.PosetSpace.threePathMap34_ne_zero (k : Type u) [Field k] : threePathMap34 k ≠ 0

theorem MagnitudeConjecture.PosetSpace.threePathMap23_ne_zero (k : Type u) [Field k] : threePathMap23 k ≠ 0

noncomputable def MagnitudeConjecture.PosetSpace.linearEquivOfIsIso (k : Type u) [Field k] {S : Type u} [PartialOrder S] {X Y : Obj k S} (f : X ⟶ Y) [CategoryTheory.IsIso f] : X.carrier ≃ₗ[k] Y.carrier

An isomorphism of T-spaces induces a linear equivalence of total spaces.

theorem MagnitudeConjecture.PosetSpace.not_isIso_of_finrank_ne (k : Type u) [Field k] {S : Type u} [PartialOrder S] {X Y : Obj k S} (f : X ⟶ Y) (hfinrank : Module.finrank k X.carrier ≠ Module.finrank k Y.carrier) : ¬CategoryTheory.IsIso f

theorem MagnitudeConjecture.PosetSpace.threePathMap12_not_isIso (k : Type u) [Field k] : ¬CategoryTheory.IsIso (threePathMap12 k)

theorem MagnitudeConjecture.PosetSpace.threePathMap01_not_isIso (k : Type u) [Field k] : ¬CategoryTheory.IsIso (threePathMap01 k)

theorem MagnitudeConjecture.PosetSpace.threePathMap34_not_isIso (k : Type u) [Field k] : ¬CategoryTheory.IsIso (threePathMap34 k)

theorem MagnitudeConjecture.PosetSpace.threePathMap23_not_isIso (k : Type u) [Field k] : ¬CategoryTheory.IsIso (threePathMap23 k)

@[simp]

theorem MagnitudeConjecture.PosetSpace.threePathComposite_apply (k : Type u) [Field k] : (CategoryTheory.CategoryStruct.comp (threePathMap01 k) (CategoryTheory.CategoryStruct.comp (threePathMap12 k) (CategoryTheory.CategoryStruct.comp (threePathMap23 k) (threePathMap34 k)))).linear 1 = 1

The four displayed arrows have nonzero total composite.

theorem MagnitudeConjecture.PosetSpace.threePathComposite_ne_zero (k : Type u) [Field k] : CategoryTheory.CategoryStruct.comp (threePathMap01 k) (CategoryTheory.CategoryStruct.comp (threePathMap12 k) (CategoryTheory.CategoryStruct.comp (threePathMap23 k) (threePathMap34 k))) ≠ 0

The four displayed arrows have nonzero total composite.

theorem MagnitudeConjecture.PosetSpace.threeLinePlane_isSchur (k : Type u) [Field k] : IsSchur k (Three k) (threeLinePlane k)

The two-dimensional three-line configuration is Schur. Preserving the two coordinate axes makes an endomorphism diagonal, and preserving the third line forces the two diagonal entries to agree. This is the manuscript's indecomposability argument in a stronger endomorphism-ring form.

theorem MagnitudeConjecture.PosetSpace.four_le_of_three_schurPositiveGrading (k : Type u) [Field k] {L : ℕ} (G : PositiveGrading (Obj k (Three k)) (IsSchur k (Three k)) L) : 4 ≤ L

A positive grading on the Schur objects of the discrete three-point poset-space category has length at least four. This is one more than the three ordinary support additions.

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

A consecutive three-element block in the chosen reverse linear extension which is an antichain in the original poset.

• le_eq_of_mem_block {s t : T} : q ≤ ↑(reverseIndex T s) → ↑(reverseIndex T s) ≤ q + 2 → q ≤ ↑(reverseIndex T t) → ↑(reverseIndex T t) ≤ q + 2 → s ≤ t → s = t

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

The global three-line subspace configuration: elements before the antichain block receive the whole plane, the block receives the two axes and diagonal, and later elements receive zero.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.PosetSpace.blockThreeLinePlane (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : Obj k T

The global two-dimensional T-space attached to a consecutive three-antichain block.

def MagnitudeConjecture.PosetSpace.blockInMap (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : supportLine k T ⟨q + 1, ⋯⟩ ⟶ blockThreeLinePlane k q hq D

The first inserted map, with underlying linear map 1 ↦ e₁.

def MagnitudeConjecture.PosetSpace.blockOutMap (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : blockThreeLinePlane k q hq D ⟶ supportLine k T ⟨q + 2, ⋯⟩

The second inserted map, with underlying linear map (x,y) ↦ x-y.

@[simp]

theorem MagnitudeConjecture.PosetSpace.blockInMap_apply (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) (x : k) : (blockInMap k q hq D).linear x = (x, 0)

@[simp]

theorem MagnitudeConjecture.PosetSpace.blockOutMap_apply (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) (x : k × k) : (blockOutMap k q hq D).linear x = x.1 - x.2

theorem MagnitudeConjecture.PosetSpace.blockInMap_ne_zero (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : blockInMap k q hq D ≠ 0

theorem MagnitudeConjecture.PosetSpace.blockOutMap_ne_zero (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : blockOutMap k q hq D ≠ 0

theorem MagnitudeConjecture.PosetSpace.blockInMap_not_isIso (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : ¬CategoryTheory.IsIso (blockInMap k q hq D)

theorem MagnitudeConjecture.PosetSpace.blockOutMap_not_isIso (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : ¬CategoryTheory.IsIso (blockOutMap k q hq D)

theorem MagnitudeConjecture.PosetSpace.blockThreeLinePlane_isSchur (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : IsSchur k T (blockThreeLinePlane k q hq D)

The global three-line plane remains Schur: the surrounding full and zero subspaces add no endomorphism freedom, while the three block positions impose the same axis/diagonal constraints as the local construction.

noncomputable def MagnitudeConjecture.PosetSpace.ConsecutiveAntichainBlock.schurDetour (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] (q : ℕ) (hq : q + 2 < Fintype.card T) (D : ConsecutiveAntichainBlock q hq) : SchurDetour k T q hq

A consecutive antichain block constructs the global Schur detour through the three-line plane.

theorem MagnitudeConjecture.PosetSpace.card_add_one_le_of_consecutiveAntichainBlock (k : Type u) [Field k] {T : Type u} [PartialOrder T] [Fintype T] {L q : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) {hq : q + 2 < Fintype.card T} (D : ConsecutiveAntichainBlock q hq) : Fintype.card T + 1 ≤ L

The manuscript's strict equality obstruction for an antichain block in the chosen reverse extension.