Documentation

TauCeti.KnotTheory.Grid.JFunction.Count

The grid J-function as a neighbor count #

The ordered southwest count GridPoint.I s t and the symmetrized J-function are defined in JFunction.lean as cardinalities of a filtered product of point sets. This file records their fiberwise reading: I s t is the sum over the left points of the number of right points strictly northeast of them, and dually over the right points. Specializing the left (or right) argument to a singleton turns each J-pairing against a single grid point into a plain count of the strictly comparable points of the other set.

The fiberwise statements are proved first for the relation-parametric GridPoint.ICount, so the strict I-pairing here and the weak half of the marking pairing in JFunction/Center.lean share the same counting API. That companion module records the resulting JCenter singleton formulas.

Main results #

References #

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

source
theorem TauCeti.GridPoint.ICount_eq_sum_card_filter {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) :
ICount r s t = ∑ p ∈ s, {q ∈ t | r p q}.card

An ordered relation count is the sum, over the left points, of its right fibers.

source
theorem TauCeti.GridPoint.ICount_eq_sum_card_filter_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) :
ICount r s t = ∑ q ∈ t, {p ∈ s | r p q}.card

An ordered relation count is the sum, over the right points, of its left fibers.

source
theorem TauCeti.GridPoint.ICount_singleton_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
ICount r {p} t = {q ∈ t | r p q}.card

The ordered relation count of a singleton on the left is the corresponding right fiber.

source
theorem TauCeti.GridPoint.ICount_singleton_right {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s : Finset (Fin n × Fin n)) (p : Fin n × Fin n) :
ICount r s {p} = {q ∈ s | r q p}.card

The ordered relation count of a singleton on the right is the corresponding left fiber.

source
theorem TauCeti.GridPoint.I_eq_sum_card_filter {n : ℕ} (s t : Finset (Fin n × Fin n)) :
I s t = ∑ p ∈ s, {q ∈ t | IsSouthWest p q}.card

The ordered southwest count I s t is the sum, over the left points p ∈ s, of the number of points of t strictly northeast of p.

source
theorem TauCeti.GridPoint.I_eq_sum_card_filter_right {n : ℕ} (s t : Finset (Fin n × Fin n)) :
I s t = ∑ q ∈ t, {p ∈ s | IsSouthWest p q}.card

The ordered southwest count I s t is the sum, over the right points q ∈ t, of the number of points of s strictly southwest of q.

source
theorem TauCeti.GridPoint.I_singleton_left {n : ℕ} (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
I {p} t = {q ∈ t | IsSouthWest p q}.card

The ordered southwest count of a single grid point against a point set t is the number of points of t strictly northeast of it.

source
theorem TauCeti.GridPoint.I_singleton_right {n : ℕ} (s : Finset (Fin n × Fin n)) (p : Fin n × Fin n) :
I s {p} = {q ∈ s | IsSouthWest q p}.card

The ordered southwest count of a point set s against a single grid point is the number of points of s strictly southwest of it.

source
theorem TauCeti.GridPoint.JNumMixed_eq_sum_singleton_left {n : ℕ} (r : Fin n × Fin n → Fin n × Fin n → Prop) [DecidableRel r] (s t : Finset (Fin n × Fin n)) :
JNumMixed r s t = ∑ p ∈ s, JNumMixed r {p} t

A mixed numerator is the sum, over the left point set, of its singleton-left contributions.

source
theorem TauCeti.GridPoint.JNum_singleton_left {n : ℕ} (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
JNum {p} t = {q ∈ t | IsSouthWest p q}.card + {q ∈ t | IsSouthWest q p}.card

The symmetrized numerator of the J-function against a single grid point splits into the two directed counts: the points of t strictly northeast of the point and the points strictly southwest of it.

source
theorem TauCeti.GridPoint.JNum_singleton_left_eq_card {n : ℕ} (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
JNum {p} t = {q ∈ t | IsSouthWest p q ∨ IsSouthWest q p}.card

The symmetrized numerator of the J-function against a single grid point is the number of points of t strictly comparable to it: those either strictly northeast or strictly southwest. The two directions never overlap, so the two counts combine into a single filter cardinality.

source
theorem TauCeti.GridPoint.J_singleton_left {n : ℕ} (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
J {p} t = ↑{q ∈ t | IsSouthWest p q ∨ IsSouthWest q p}.card / 2

The J-pairing of a single grid point against a point set t is half the number of points of t strictly comparable to it.

source
theorem TauCeti.GridPoint.two_mul_J_singleton_left {n : ℕ} (p : Fin n × Fin n) (t : Finset (Fin n × Fin n)) :
2 * J {p} t = ↑{q ∈ t | IsSouthWest p q ∨ IsSouthWest q p}.card

Twice the J-pairing of a single grid point against a point set t is the number of points of t strictly comparable to it: in particular this pairing is a half-integer whose double is a natural number.