The remaining negative-side Grassmannian envelope

GrassmannianAsp proves that the ordinary Young-diagram corners dominate all rows with b ≥ 0. This module isolates the complementary half without silently replacing it by a finite experiment. The only extra datum is the cardinality of a finite interval of negative inputs; for a Grassmannian permutation its membership predicate is the explicit column-length formula.

The Young-diagram counting inequality is proved below, so the resulting corner envelope and once-marked dictionary are unconditional facts about the explicitly reconstructed ASP permutation.

The cut determined by the zero-row slipface

theorem Utilities.grassmannianPerm_se_finset_zero_eq_Ico_s (lambda : YoungDiagram) (a : ℤ) : (grassmannianPermOfYoungDiagram lambda).seFinset (a + 1) 0 = Finset.Ico 0 ((grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0)

On the nonnegative ray, the inputs below a fixed output threshold form the initial interval whose length is the zero-cut slipface value.

theorem Utilities.grassmannianRowLen_at_zeroCut_le (lambda : YoungDiagram) (a : ℤ) : have r := (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0; ↑(lambda.rowLen r.toNat) ≤ r - a - 1

If r = s(a+1,0), then the first row omitted from the initial segment has length at most r-a-1.

theorem Utilities.grassmannianRowLen_before_zeroCut_ge (lambda : YoungDiagram) (a : ℤ) (hr : 0 < (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0) : have r := (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0; r - a - 1 ≤ ↑(lambda.rowLen (r - 1).toNat)

When the zero-cut is nonempty, its last included row has length at least r-a-1, where r is the slipface value.

theorem Utilities.grassmannianPerm_apply_neg_lt_iff_le_zeroCut (lambda : YoungDiagram) (a n : ℤ) (hn : n < 0) : (grassmannianPermOfYoungDiagram lambda).func n < a + 1 ↔ n ≤ a - (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0

The negative ray crosses the output threshold exactly at the conjugate column determined by the zero-cut. This is the row/column-conjugacy heart of the negative envelope.

noncomputable def Utilities.grassmannianNegativeContribution (lambda : YoungDiagram) (a b : ℤ) : ℤ

The finite negative-input contribution when a transmission row is moved from the cut b = 0 to b < 0.

Equations

• Utilities.grassmannianNegativeContribution lambda a b = ↑{n ∈ Finset.Ico b 0 | n + ↑(lambda.colLen (-n - 1).toNat) < a + 1}.card

theorem Utilities.grassmannianPerm_negative_row_formula (lambda : YoungDiagram) (a b : ℤ) (hb : b ≤ 0) : (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 = (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0 - 1 + grassmannianNegativeContribution lambda a b

Moving a Grassmannian row from a negative second coordinate to zero adds exactly the displayed finite column-length count.

theorem Utilities.grassmannianNegativeContribution_eq (lambda : YoungDiagram) (a b : ℤ) : have r := (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0; grassmannianNegativeContribution lambda a b = if b ≤ a - r then a - r - b + 1 else 0

The negative contribution is the length of a single terminal interval. Here r = s(a+1,0), so its first contributing column is r-a-1.

theorem Utilities.grassmannianPerm_negative_row_dichotomy (lambda : YoungDiagram) (a b : ℤ) (hb : b < 0) : have r := (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) 0; (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 = r - 1 ∨ (grassmannianPermOfYoungDiagram lambda).s.func (a + 1) b - 1 = a - b

At a negative cut, the Grassmannian slipface is forced onto one of two lines: it is unchanged from b=0, or it lies exactly on the Riemann line.

def Utilities.GrassmannianNegativeEnvelope (lambda : YoungDiagram) : Prop

The precise residual Young-diagram inequality needed on the negative side of the corner envelope. It contains no ASP-set or reconstruction predicate: only a finite interval count using column lengths remains.

Equations

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

theorem Utilities.grassmannianNegativeEnvelope (lambda : YoungDiagram) : GrassmannianNegativeEnvelope lambda

The negative Ferrers-count envelope holds for every Young diagram. The proof uses the dichotomy above: either moving below b=0 adds no inputs, or the resulting slipface value is exactly the Riemann bound.

theorem Utilities.grassmannianPerm_cornersDominate_of_negativeEnvelope (lambda : YoungDiagram) (hNegative : GrassmannianNegativeEnvelope lambda) : CornersDominate (grassmannianPermOfYoungDiagram lambda) (onceMarkedCorners lambda)

A negative-side Young-diagram envelope, together with the already-proved nonnegative theorem, gives the full ASP corner envelope.

theorem Utilities.grassmannianPerm_cornersDominate (lambda : YoungDiagram) : CornersDominate (grassmannianPermOfYoungDiagram lambda) (onceMarkedCorners lambda)

Unconditional full corner domination for the Grassmannian permutation of an arbitrary Young diagram.

theorem Utilities.grassmannianPartitionProfile_of_negativeEnvelope (lambda : YoungDiagram) (hNegative : GrassmannianNegativeEnvelope lambda) : GrassmannianPartitionProfile (grassmannianPermOfYoungDiagram lambda) lambda

The explicit Grassmannian constructor has a partition profile as soon as the finite negative-side Young-diagram envelope is supplied.

theorem Utilities.grassmannianPartitionProfile (lambda : YoungDiagram) : GrassmannianPartitionProfile (grassmannianPermOfYoungDiagram lambda) lambda

Every explicit Grassmannian permutation has the partition profile of its defining Young diagram.

theorem Utilities.transmissionExists_grassmannianPerm_iff_onceMarkedBNExists_of_negativeEnvelope {G : CFGraph} (hG : graphConnected G) (u v : G.V) (lambda : YoungDiagram) (hNegative : GrassmannianNegativeEnvelope lambda) : TransmissionExists G u v (grassmannianPermOfYoungDiagram lambda) ↔ OnceMarkedBNExists G u lambda

Factored form of the full Grassmannian/once-marked dictionary, useful when reusing a separately supplied negative-envelope proof.

theorem Utilities.transmissionExists_grassmannianPerm_iff_onceMarkedBNExists {G : CFGraph} (hG : graphConnected G) (u v : G.V) (lambda : YoungDiagram) : TransmissionExists G u v (grassmannianPermOfYoungDiagram lambda) ↔ OnceMarkedBNExists G u lambda

Unconditional Grassmannian/once-marked existence dictionary.