The grid J-function

This file adds the finite point-pair count used in the Maslov and Alexander gradings of grid homology. For finite sets of grid points, GridPoint.ICount r s t counts the ordered pairs (p, q) ∈ s × t with r p q; GridPoint.I s t is its value at the strict southwest relation, and GridPoint.J s t is the symmetrized half-count. Keeping the count parametric in the relation lets the pairing against markings at the centres of their squares (JFunction/Center.lean), which weakens the comparison, share this API.

The API is deliberately point-set level: later grading definitions apply it to grid-state and marking point sets, which the Maslov and Alexander gradings are then assembled from.

Main definitions

• TauCeti.GridPoint.IsSouthWest: the strict southwest relation on grid squares.
• TauCeti.GridPoint.ICount: the ordered count of pairs of grid points related by a given decidable relation.
• TauCeti.GridPoint.I: the ordered southwest pair count, ICount at the strict southwest relation.
• TauCeti.GridPoint.JNumMixed, TauCeti.GridPoint.JMixed: the mixed numerator with a variable forward relation and strict southwest reverse relation, and its rational half.
• TauCeti.GridPoint.JNum: the numerator of the symmetrized J-function.
• TauCeti.GridPoint.J: the rational-valued symmetrized J-function.
• TauCeti.GridState.J: the specialized form for a pair of grid states.

Main results

• TauCeti.GridPoint.I_image_swap, TauCeti.GridPoint.J_image_swap, TauCeti.GridState.J_transpose: the southwest counts and the J-function are invariant under reflecting the point sets across the diagonal.
• TauCeti.GridPoint.I_image_rev, TauCeti.GridPoint.JNum_image_rev, TauCeti.GridPoint.J_image_rev, TauCeti.GridState.J_rotate: reversing both coordinates of the point sets exchanges the two arguments of the ordered count I, while the symmetrized JNum and J are invariant.
• TauCeti.GridPoint.I_graph_eq_card, TauCeti.GridState.J_pointSet_eq_card: graph point-set J-pairings as column-index counts.

References

This supplies a prerequisite for CombinatorialHeegaardFloer/README.md in TauCetiRoadmap, Lane G.2, "Gradings. The J-function, M_O, M_X, A; integer-valuedness of A; grading-change formulas across a rectangle." The definition follows Ozsváth--Stipsicz--Szabó, Grid Homology for Knots and Links, Chapter 4.3, where J is the symmetrization of the northeast/southwest point-pair count.

def TauCeti.GridPoint.IsSouthWest {n : ℕ} (p q : Fin n × Fin n) : Prop

A grid point is strictly southwest of another when both its column and row coordinates are strictly smaller. This is the affine point-pair relation used in the grid J-function; it is not the toroidal cyclic order used for rectangles.

@[instance_reducible]

instance TauCeti.GridPoint.decidableIsSouthWest {n : ℕ} (p q : Fin n × Fin n) : Decidable (IsSouthWest p q)

The strict southwest relation has a decidable instance.

@[simp]

theorem TauCeti.GridPoint.isSouthWest_iff {n : ℕ} (p q : Fin n × Fin n) : IsSouthWest p q ↔ ↑p.1 < ↑q.1 ∧ ↑p.2 < ↑q.2

The southwest relation in coordinate form.

theorem TauCeti.GridPoint.not_isSouthWest_self {n : ℕ} (p : Fin n × Fin n) : ¬IsSouthWest p p

A point is not strictly southwest of itself.

theorem TauCeti.GridPoint.ne_of_isSouthWest {n : ℕ} {p q : Fin n × Fin n} (h : IsSouthWest p q) : p ≠ q

A strictly southwest pair has distinct endpoints.

theorem TauCeti.GridPoint.not_isSouthWest_swap {n : ℕ} {p q : Fin n × Fin n} (h : IsSouthWest p q) : ¬IsSouthWest q p

The strict southwest relation is asymmetric.

theorem TauCeti.GridPoint.isSouthWest_swap {n : ℕ} (p q : Fin n × Fin n) : IsSouthWest p.swap q.swap ↔ IsSouthWest p q

The strict southwest relation is invariant under reflecting both points across the diagonal: exchanging the column and row coordinates of both endpoints exchanges the two strict inequalities.

def TauCeti.GridPoint.ICount {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : ℕ

The ordered count of pairs (p, q) ∈ s × t related by r. The two relations used on grids are the strict southwest relation GridPoint.IsSouthWest, giving the J-function of this file, and the weak product order, giving the pairing of grid points against markings sitting at the centres of their squares.

theorem TauCeti.GridPoint.ICount_def {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : ICount r s t = {pq ∈ s ×ˢ t | r pq.1 pq.2}.card

The ordered relation count as the cardinality of the filtered product of point sets.

@[simp]

theorem TauCeti.GridPoint.ICount_empty_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s : Finset (Fin n × Fin n)) : ICount r ∅ s = 0

The ordered relation count is zero when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.ICount_empty_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s : Finset (Fin n × Fin n)) : ICount r s ∅ = 0

The ordered relation count is zero when the right point set is empty.

@[simp]

theorem TauCeti.GridPoint.ICount_singleton_singleton {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (p q : Fin n × Fin n) : ICount r {p} {q} = if r p q then 1 else 0

The ordered relation count of singleton point sets records the single comparison.

theorem TauCeti.GridPoint.ICount_union_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : ICount r (s₁ ∪ s₂) t = ICount r s₁ t + ICount r s₂ t

The ordered relation count is additive in the left point set over disjoint unions.

theorem TauCeti.GridPoint.ICount_union_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : ICount r s (t₁ ∪ t₂) = ICount r s t₁ + ICount r s t₂

The ordered relation count is additive in the right point set over disjoint unions.

theorem TauCeti.GridPoint.ICount_insert_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : ICount r (insert p s) t = ICount r {p} t + ICount r s t

The ordered relation count after inserting a fresh point on the left.

theorem TauCeti.GridPoint.ICount_insert_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : ICount r s (insert p t) = ICount r s {p} + ICount r s t

The ordered relation count after inserting a fresh point on the right.

theorem TauCeti.GridPoint.ICount_mono_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s₁ s₂ t : Finset (Fin n × Fin n)} (h : s₁ ⊆ s₂) : ICount r s₁ t ≤ ICount r s₂ t

The ordered relation count is monotone in its left point set.

theorem TauCeti.GridPoint.ICount_mono_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s t₁ t₂ : Finset (Fin n × Fin n)} (h : t₁ ⊆ t₂) : ICount r s t₁ ≤ ICount r s t₂

The ordered relation count is monotone in its right point set.

theorem TauCeti.GridPoint.ICount_image_swap {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (hr : ∀ (p q : Fin n × Fin n), r p.swap q.swap ↔ r p q) (s t : Finset (Fin n × Fin n)) : ICount r (Finset.image Prod.swap s) (Finset.image Prod.swap t) = ICount r s t

The ordered relation count of a relation invariant under the diagonal reflection is invariant under reflecting both point sets across the diagonal.

theorem TauCeti.GridPoint.ICount_graph_eq_card {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (f g : Fin n → Fin n) : ICount r (Finset.image (fun (c : Fin n) => (c, f c)) Finset.univ) (Finset.image (fun (c : Fin n) => (c, g c)) Finset.univ) = {p : Fin n × Fin n | r (p.1, f p.1) (p.2, g p.2)}.card

The ordered relation count of two graph point sets counts the column pairs whose two prescribed grid points are related. This graph-level statement does not require either row assignment to be a permutation.

def TauCeti.GridPoint.I {n : ℕ} (s t : Finset (Fin n × Fin n)) : ℕ

The ordered count of pairs (p, q) ∈ s × t with p strictly southwest of q.

theorem TauCeti.GridPoint.I_def {n : ℕ} (s t : Finset (Fin n × Fin n)) : I s t = {pq ∈ s ×ˢ t | IsSouthWest pq.1 pq.2}.card

The ordered southwest count as the cardinality of the filtered product of point sets.

theorem TauCeti.GridPoint.mem_filter_product_isSouthWest {n : ℕ} (s t : Finset (Fin n × Fin n)) (pq : (Fin n × Fin n) × Fin n × Fin n) : pq ∈ {pq ∈ s ×ˢ t | IsSouthWest pq.1 pq.2} ↔ pq.1 ∈ s ∧ pq.2 ∈ t ∧ IsSouthWest pq.1 pq.2

Membership in the finite set counted by GridPoint.I.

@[simp]

theorem TauCeti.GridPoint.I_empty_left {n : ℕ} (s : Finset (Fin n × Fin n)) : I ∅ s = 0

The ordered southwest count is zero when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.I_empty_right {n : ℕ} (s : Finset (Fin n × Fin n)) : I s ∅ = 0

The ordered southwest count is zero when the right point set is empty.

@[simp]

theorem TauCeti.GridPoint.I_singleton_singleton {n : ℕ} (p q : Fin n × Fin n) : I {p} {q} = if IsSouthWest p q then 1 else 0

The ordered southwest count of singleton point sets is one exactly for a southwest pair.

theorem TauCeti.GridPoint.I_singleton_self {n : ℕ} (p : Fin n × Fin n) : I {p} {p} = 0

No point contributes a southwest pair with itself.

theorem TauCeti.GridPoint.I_union_left {n : ℕ} {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : I (s₁ ∪ s₂) t = I s₁ t + I s₂ t

The ordered southwest count is additive in the left point set over disjoint unions.

theorem TauCeti.GridPoint.I_union_right {n : ℕ} {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : I s (t₁ ∪ t₂) = I s t₁ + I s t₂

The ordered southwest count is additive in the right point set over disjoint unions.

theorem TauCeti.GridPoint.I_insert_left {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : I (insert p s) t = I {p} t + I s t

The ordered southwest count after inserting a fresh point on the left.

theorem TauCeti.GridPoint.I_insert_right {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : I s (insert p t) = I s {p} + I s t

The ordered southwest count after inserting a fresh point on the right.

def TauCeti.GridPoint.JNumMixed {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : ℕ

The mixed numerator formed from a variable forward relation count and the reverse strict southwest count. This is the common shape of the strict and point-to-marking pairings.

def TauCeti.GridPoint.JMixed {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : ℚ

The rational pairing obtained by halving a mixed numerator.

theorem TauCeti.GridPoint.JNumMixed_def {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : JNumMixed r s t = ICount r s t + I t s

A mixed numerator is the sum of its variable forward count and strict reverse count.

theorem TauCeti.GridPoint.JMixed_def {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) : JMixed r s t = ↑(JNumMixed r s t) / 2

A mixed rational pairing is half its numerator.

@[simp]

theorem TauCeti.GridPoint.JNumMixed_empty_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (t : Finset (Fin n × Fin n)) : JNumMixed r ∅ t = 0

A mixed numerator vanishes when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.JNumMixed_empty_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s : Finset (Fin n × Fin n)) : JNumMixed r s ∅ = 0

A mixed numerator vanishes when the right point set is empty.

theorem TauCeti.GridPoint.JNumMixed_union_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : JNumMixed r (s₁ ∪ s₂) t = JNumMixed r s₁ t + JNumMixed r s₂ t

A mixed numerator is additive in its left point set over disjoint unions.

theorem TauCeti.GridPoint.JNumMixed_union_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : JNumMixed r s (t₁ ∪ t₂) = JNumMixed r s t₁ + JNumMixed r s t₂

A mixed numerator is additive in its right point set over disjoint unions.

theorem TauCeti.GridPoint.JNumMixed_insert_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : JNumMixed r (insert p s) t = JNumMixed r {p} t + JNumMixed r s t

A mixed numerator after inserting a fresh point on the left.

theorem TauCeti.GridPoint.JNumMixed_insert_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : JNumMixed r s (insert p t) = JNumMixed r s {p} + JNumMixed r s t

A mixed numerator after inserting a fresh point on the right.

@[simp]

theorem TauCeti.GridPoint.JMixed_empty_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (t : Finset (Fin n × Fin n)) : JMixed r ∅ t = 0

A mixed rational pairing vanishes when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.JMixed_empty_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s : Finset (Fin n × Fin n)) : JMixed r s ∅ = 0

A mixed rational pairing vanishes when the right point set is empty.

theorem TauCeti.GridPoint.JMixed_union_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : JMixed r (s₁ ∪ s₂) t = JMixed r s₁ t + JMixed r s₂ t

A mixed rational pairing is additive in its left point set over disjoint unions.

theorem TauCeti.GridPoint.JMixed_union_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : JMixed r s (t₁ ∪ t₂) = JMixed r s t₁ + JMixed r s t₂

A mixed rational pairing is additive in its right point set over disjoint unions.

theorem TauCeti.GridPoint.JMixed_insert_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : JMixed r (insert p s) t = JMixed r {p} t + JMixed r s t

A mixed rational pairing after inserting a fresh point on the left.

theorem TauCeti.GridPoint.JMixed_insert_pair_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {S P : Finset (Fin n × Fin n)} {a b : Fin n × Fin n} (hab : a ∉ insert b S) (hb : b ∉ S) : JMixed r (insert a (insert b S)) P = JMixed r {a} P + JMixed r {b} P + JMixed r S P

Splitting a two-point insertion out of the left argument of a mixed pairing.

theorem TauCeti.GridPoint.JMixed_insert_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : JMixed r s (insert p t) = JMixed r s {p} + JMixed r s t

A mixed rational pairing after inserting a fresh point on the right.

theorem TauCeti.GridPoint.JNumMixed_image_swap {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (hr : ∀ (p q : Fin n × Fin n), r p.swap q.swap ↔ r p q) (s t : Finset (Fin n × Fin n)) : JNumMixed r (Finset.image Prod.swap s) (Finset.image Prod.swap t) = JNumMixed r s t

A mixed numerator is invariant under diagonal reflection when its variable relation is.

theorem TauCeti.GridPoint.JMixed_image_swap {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (hr : ∀ (p q : Fin n × Fin n), r p.swap q.swap ↔ r p q) (s t : Finset (Fin n × Fin n)) : JMixed r (Finset.image Prod.swap s) (Finset.image Prod.swap t) = JMixed r s t

A mixed rational pairing is invariant under diagonal reflection when its variable variable relation is.

def TauCeti.GridPoint.JNum {n : ℕ} (s t : Finset (Fin n × Fin n)) : ℕ

The numerator of the symmetrized J-function. Keeping the numerator as a natural number is convenient for parity and integrality lemmas before passing to rational values.

theorem TauCeti.GridPoint.JNum_def {n : ℕ} (s t : Finset (Fin n × Fin n)) : JNum s t = I s t + I t s

The numerator of J is the sum of the two ordered southwest counts.

@[simp]

theorem TauCeti.GridPoint.JNum_self {n : ℕ} (s : Finset (Fin n × Fin n)) : JNum s s = 2 * I s s

The symmetrized numerator of the J-function on a point set with itself is even: it is twice the ordered southwest count.

def TauCeti.GridPoint.J {n : ℕ} (s t : Finset (Fin n × Fin n)) : ℚ

The rational-valued symmetrized grid J-function.

theorem TauCeti.GridPoint.J_def {n : ℕ} (s t : Finset (Fin n × Fin n)) : J s t = ↑(JNum s t) / 2

The rational-valued J-function is half of its symmetrized numerator.

@[simp]

theorem TauCeti.GridPoint.J_self {n : ℕ} (s : Finset (Fin n × Fin n)) : J s s = ↑(I s s)

The J-function on a point set with itself is an integer, namely the ordered southwest count. The two southwest comparisons of a pair contribute symmetrically, so the division by two is exact.

theorem TauCeti.GridPoint.JNum_comm {n : ℕ} (s t : Finset (Fin n × Fin n)) : JNum s t = JNum t s

The numerator of J is symmetric.

theorem TauCeti.GridPoint.J_comm {n : ℕ} (s t : Finset (Fin n × Fin n)) : J s t = J t s

The grid J-function is symmetric.

@[simp]

theorem TauCeti.GridPoint.JNum_empty_left {n : ℕ} (s : Finset (Fin n × Fin n)) : JNum ∅ s = 0

The numerator of J vanishes when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.JNum_empty_right {n : ℕ} (s : Finset (Fin n × Fin n)) : JNum s ∅ = 0

The numerator of J vanishes when the right point set is empty.

theorem TauCeti.GridPoint.JNum_union_left {n : ℕ} {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : JNum (s₁ ∪ s₂) t = JNum s₁ t + JNum s₂ t

The numerator of J is additive in the left point set over disjoint unions.

theorem TauCeti.GridPoint.JNum_union_right {n : ℕ} {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : JNum s (t₁ ∪ t₂) = JNum s t₁ + JNum s t₂

The numerator of J is additive in the right point set over disjoint unions.

theorem TauCeti.GridPoint.JNum_insert_left {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : JNum (insert p s) t = JNum {p} t + JNum s t

The numerator of J after inserting a fresh point on the left.

theorem TauCeti.GridPoint.JNum_insert_right {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : JNum s (insert p t) = JNum s {p} + JNum s t

The numerator of J after inserting a fresh point on the right.

@[simp]

theorem TauCeti.GridPoint.J_empty_left {n : ℕ} (s : Finset (Fin n × Fin n)) : J ∅ s = 0

J vanishes when the left point set is empty.

@[simp]

theorem TauCeti.GridPoint.J_empty_right {n : ℕ} (s : Finset (Fin n × Fin n)) : J s ∅ = 0

J vanishes when the right point set is empty.

theorem TauCeti.GridPoint.J_union_left {n : ℕ} {s₁ s₂ t : Finset (Fin n × Fin n)} (h : Disjoint s₁ s₂) : J (s₁ ∪ s₂) t = J s₁ t + J s₂ t

The grid J-function is additive in the left point set over disjoint unions.

theorem TauCeti.GridPoint.J_union_right {n : ℕ} {s t₁ t₂ : Finset (Fin n × Fin n)} (h : Disjoint t₁ t₂) : J s (t₁ ∪ t₂) = J s t₁ + J s t₂

The grid J-function is additive in the right point set over disjoint unions.

theorem TauCeti.GridPoint.J_insert_left {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ s) : J (insert p s) t = J {p} t + J s t

The grid J-function after inserting a fresh point on the left.

theorem TauCeti.GridPoint.J_insert_right {n : ℕ} {p : Fin n × Fin n} {s t : Finset (Fin n × Fin n)} (h : p ∉ t) : J s (insert p t) = J s {p} + J s t

The grid J-function after inserting a fresh point on the right.

@[simp]

theorem TauCeti.GridPoint.JNum_singleton_singleton {n : ℕ} (p q : Fin n × Fin n) : JNum {p} {q} = (if IsSouthWest p q then 1 else 0) + if IsSouthWest q p then 1 else 0

The numerator of J on singleton point sets records whether either point is southwest of the other.

@[simp]

theorem TauCeti.GridPoint.J_singleton_singleton {n : ℕ} (p q : Fin n × Fin n) : J {p} {q} = ↑((if IsSouthWest p q then 1 else 0) + if IsSouthWest q p then 1 else 0) / 2

The J-function on singleton point sets is half the number of southwest comparisons between the two points.

theorem TauCeti.GridPoint.J_singleton_singleton_of_isSouthWest_or_isSouthWest {n : ℕ} {p q : Fin n × Fin n} (h : IsSouthWest p q ∨ IsSouthWest q p) : J {p} {q} = 1 / 2

The J-function of two comparable singleton point sets is 1 / 2.

theorem TauCeti.GridPoint.J_singleton_self {n : ℕ} (p : Fin n × Fin n) : J {p} {p} = 0

The J-function of a singleton with itself is zero.

theorem TauCeti.GridPoint.I_mono_left {n : ℕ} {s₁ s₂ t : Finset (Fin n × Fin n)} (h : s₁ ⊆ s₂) : I s₁ t ≤ I s₂ t

The ordered southwest count is monotone in its left point set.

theorem TauCeti.GridPoint.I_mono_right {n : ℕ} {s t₁ t₂ : Finset (Fin n × Fin n)} (h : t₁ ⊆ t₂) : I s t₁ ≤ I s t₂

The ordered southwest count is monotone in its right point set.

theorem TauCeti.GridPoint.JNum_mono_left {n : ℕ} {s₁ s₂ t : Finset (Fin n × Fin n)} (h : s₁ ⊆ s₂) : JNum s₁ t ≤ JNum s₂ t

The numerator of J is monotone in its left point set.

theorem TauCeti.GridPoint.JNum_mono_right {n : ℕ} {s t₁ t₂ : Finset (Fin n × Fin n)} (h : t₁ ⊆ t₂) : JNum s t₁ ≤ JNum s t₂

The numerator of J is monotone in its right point set.

theorem TauCeti.GridPoint.I_image_swap {n : ℕ} (s t : Finset (Fin n × Fin n)) : I (Finset.image Prod.swap s) (Finset.image Prod.swap t) = I s t

The ordered southwest count is invariant under reflecting both point sets across the diagonal.

theorem TauCeti.GridPoint.JNum_image_swap {n : ℕ} (s t : Finset (Fin n × Fin n)) : JNum (Finset.image Prod.swap s) (Finset.image Prod.swap t) = JNum s t

The numerator of the J-function is invariant under reflecting both point sets across the diagonal.

theorem TauCeti.GridPoint.J_image_swap {n : ℕ} (s t : Finset (Fin n × Fin n)) : J (Finset.image Prod.swap s) (Finset.image Prod.swap t) = J s t

The symmetrized grid J-function is invariant under reflecting both point sets across the diagonal.

theorem TauCeti.GridPoint.isSouthWest_rev {n : ℕ} (p q : Fin n × Fin n) : IsSouthWest (Prod.map Fin.rev Fin.rev p) (Prod.map Fin.rev Fin.rev q) ↔ IsSouthWest q p

Reversing both coordinates of both points of a pair exchanges the two endpoints of the strict southwest relation: it sends the column and row comparisons to their reverses.

theorem TauCeti.GridPoint.I_image_rev {n : ℕ} (s t : Finset (Fin n × Fin n)) : I (Finset.image (Prod.map Fin.rev Fin.rev) s) (Finset.image (Prod.map Fin.rev Fin.rev) t) = I t s

The ordered southwest count is invariant, up to exchanging the two point sets, under reversing both coordinates of both point sets. The reversal turns each southwest comparison into the opposite comparison, so the count of southwest pairs from s to t becomes the count from t to s.

theorem TauCeti.GridPoint.JNum_image_rev {n : ℕ} (s t : Finset (Fin n × Fin n)) : JNum (Finset.image (Prod.map Fin.rev Fin.rev) s) (Finset.image (Prod.map Fin.rev Fin.rev) t) = JNum s t

The numerator of the J-function is invariant under reversing both coordinates of both point sets. The two ordered counts are exchanged by the reversal, and their sum is symmetric.

theorem TauCeti.GridPoint.J_image_rev {n : ℕ} (s t : Finset (Fin n × Fin n)) : J (Finset.image (Prod.map Fin.rev Fin.rev) s) (Finset.image (Prod.map Fin.rev Fin.rev) t) = J s t

The symmetrized grid J-function is invariant under reversing both coordinates of both point sets.

theorem TauCeti.GridPoint.I_graph_eq_card {n : ℕ} (f g : Fin n → Fin n) : I (Finset.image (fun (c : Fin n) => (c, f c)) Finset.univ) (Finset.image (fun (c : Fin n) => (c, g c)) Finset.univ) = {p : Fin n × Fin n | p.1 < p.2 ∧ f p.1 < g p.2}.card

The ordered southwest count of two graph point sets is the number of column pairs c < d where the source row precedes the target row. This graph-level statement does not require either row assignment to be a permutation.

def TauCeti.GridState.J {n : ℕ} (x y : GridState n) : ℚ

The grid J-function applied to the point sets of two grid states.

@[simp]

theorem TauCeti.GridState.J_def {n : ℕ} (x y : GridState n) : x.J y = GridPoint.J x.pointSet y.pointSet

The state-level grid J-function is the point-set J-function on state point sets.

theorem TauCeti.GridState.J_comm {n : ℕ} (x y : GridState n) : x.J y = y.J x

The state-level grid J-function is symmetric.

theorem TauCeti.GridState.J_transpose {n : ℕ} (x y : GridState n) : x.transpose.J y.transpose = x.J y

The state-level grid J-function is invariant under reflecting both states across the diagonal.

theorem TauCeti.GridState.J_rotate {n : ℕ} (x y : GridState n) : x.rotate.J y.rotate = x.J y

The state-level grid J-function is invariant under the half-turn rotation of both states.

theorem TauCeti.GridState.I_pointSet_eq_card {n : ℕ} (x y : GridState n) : GridPoint.I x.pointSet y.pointSet = {p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < y.toPerm p.2}.card

The ordered southwest count of the point sets of two grid states is the number of column pairs c < d at which the source row precedes the target row.

theorem TauCeti.GridState.JNum_pointSet_eq_card {n : ℕ} (x y : GridState n) : GridPoint.JNum x.pointSet y.pointSet = {p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < y.toPerm p.2}.card + {p : Fin n × Fin n | p.1 < p.2 ∧ y.toPerm p.1 < x.toPerm p.2}.card

The symmetrized numerator of the grid J-function on two state point sets, as a sum of two column-index counts.

theorem TauCeti.GridState.J_pointSet_eq_card {n : ℕ} (x y : GridState n) : x.J y = ↑({p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < y.toPerm p.2}.card + {p : Fin n × Fin n | p.1 < p.2 ∧ y.toPerm p.1 < x.toPerm p.2}.card) / 2

The rational grid J-function on two state point sets is half the sum of the two column-index counts.

theorem TauCeti.GridState.I_self_pointSet_eq_card {n : ℕ} (x : GridState n) : GridPoint.I x.pointSet x.pointSet = {p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < x.toPerm p.2}.card

The self southwest count of a grid state is the number of non-inversions of its permutation: column pairs c < d whose occupied rows are in the same order.

theorem TauCeti.GridState.card_filter_noninversion_add_card_filter_inversion {n : ℕ} (x : GridState n) : {p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.1 < x.toPerm p.2}.card + {p : Fin n × Fin n | p.1 < p.2 ∧ x.toPerm p.2 < x.toPerm p.1}.card = {p : Fin n × Fin n | p.1 < p.2}.card

The non-inversions and the inversions of a grid state partition the ordered column pairs: the number of pairs c < d with x c < x d plus the number with x d < x c is the total number of pairs c < d. The state's permutation is injective, so on each ordered column pair exactly one of the two strict row comparisons holds.