Two upper-set squares exclude three-element antichains

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveDirectedBoundaryData.directAntichain_card_le_two {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] {S : FiniteIndecomposableSkeleton k A} {e : A} {D : PrimitiveIdempotentData e} (B : S.PrimitiveDirectedBoundaryData (S.primitiveMultiplicityInput D)) (hz : DirectedDeletion.intrinsicEulerExcess (FiniteTauMatrix.meshMatrix (S.factorFiniteTauCategoryData (S.primitiveKilledLabels D))) = 0) (F : Finset B.ProjectivePoset) (hF : ∀ a ∈ F, ∀ b ∈ F, a ≤ b → a = b) : F.card ≤ 2

At zero excess every antichain in the projective poset has at most two elements. Two upper-set squares would otherwise give distinct targets with the same AR translate.