Counting bridges for Dross's cut argument #
The graph's triangle and K₄ counts agree with the edge-node quantities used in the auxiliary flow network.
theorem
LeanPool.DrossFractionalTriangleDecomposition.k4pair_edge_iff
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v : V}
(huv : G.Adj u v)
{c d : V}
(hcd : G.Adj c d)
:
K4pair G s(u, v) s(c, d) ↔ c ∈ G.neighborFinset u ∩ G.neighborFinset v ∧ d ∈ G.neighborFinset u ∩ G.neighborFinset v
A rooted K₄ pair is characterized by both partner endpoints being common neighbours.
theorem
LeanPool.DrossFractionalTriangleDecomposition.k4pair_count_eq
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v : V}
(huv : G.Adj u v)
:
Bridge #K₄-partners = numK4Through. For an edge uv, the number of edges forming a
rooted-K₄ pair with it equals numK4Through G u v (Spine's K₄ count, bounded below by A6).
theorem
LeanPool.DrossFractionalTriangleDecomposition.triThrough_edge
{V : Type u_1}
[Fintype V]
[DecidableEq V]
(G : SimpleGraph V)
[DecidableRel G.Adj]
{u v : V}
(huv : G.Adj u v)
:
Bridge T_e = codeg. The number of triangles through an edge uv equals the number of
common neighbours of u and v (Dross's Tₑ). This links triThrough to A6 (Spine).