Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Ordinary zero forcing, symmetric maximum nullity, and minimum rank of unequal-leg spider powers

Abstract

For integers m >= 2 and k >= 1 and independently chosen leg lengths ell_0, …, ell_{m - 1} >= k + 1, the ordinary distance-at-most-k power G = T^k of the spider T on N = 1 + sum_{i = 0}^{m - 1} ell_i vertices has ordinary zero forcing number Z(G) = (m - 1) k, real symmetric maximum nullity M_R(G) = (m - 1) k, and real symmetric minimum rank mr_R(G) = N - (m - 1) k. The upper bound Z(G) <= (m - 1) k is realized by the tail set consisting of the last k vertices on each of the first m - 1 legs, while the matching lower bound and symmetric extremum are realized by one explicit real symmetric matrix combining per-leg sliding-window Gram blocks D_{ell_i}^T D_{ell_i} with cross-leg and center indicator couplings.

Definition 1.1 (Vertex type of a spider with independently chosen leg lengths).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.Vertex (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For m : Nat and leg-length profile ell : Fin m -> Nat, Vertex m ell is Option (Sigma i : Fin m, Fin (ell i)). The constructor none denotes the center vertex c, while some <i, d> denotes the vertex on 1-based leg i_1 = i.val + 1 (1 <= i_1 <= m) at 1-based depth d_1 = d.val + 1 (1 <= d_1 <= ell i) from the center.

Definition 1.2 (Spider tree on independently varying leg lengths).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.spiderTree (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

The simple graph spiderTree m ell joins the center none to some <i, d> precisely when d.val = 0 (1-based depth 1), and joins two leg vertices some <i, d> and some <j, e> precisely when i = j and Nat.dist d.val e.val = 1.

Definition 1.3 (Closed-form spider-tree distance).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.distance (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

The function distance m ell evaluates to 0 at (none, none), to d.val + 1 between none and some <i, d> (matching 1-based depth d_1 = d.val + 1), to Nat.dist d.val e.val = |d_1 - e_1| for two vertices on the same leg i = j, and to d.val + e.val + 2 = d_1 + e_1 for two vertices on distinct legs i != j.

Definition 1.4 (Ordinary distance-at-most-k spider power).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.power (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

The simple graph power m k ell on Vertex m ell joins distinct vertices u != v precisely when distance m ell u v <= k.

Definition 1.5 (Real symmetric matrix family of a simple graph).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.SymGraphMatrices (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For a simple graph G on V : Type, SymGraphMatrices G is the set of real matrices A : Matrix V V R that are symmetric (A.IsSymm) and satisfy A u v != 0 <-> G.Adj u v for all distinct vertices u != v, with diagonal entries unconstrained.

Definition 1.6 (Right-kernel dimension of a real square matrix).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.matrixNullity (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For a finite vertex type V and matrix A : Matrix V V R, matrixNullity A is Module.finrank R (LinearMap.ker A.mulVecLin).

Definition 1.7 (Maximum symmetric nullity of a finite simple graph).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.maxSymNullity (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For a simple graph G on a finite vertex type V, maxSymNullity G is the supremum sSup (matrixNullity ‘’ SymGraphMatrices G) in Nat.

Definition 1.8 (Minimum symmetric rank of a finite simple graph).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.minSymRank (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For a simple graph G on a finite vertex type V, minSymRank G is the infimum sInf (Matrix.rank ‘’ SymGraphMatrices G) in Nat.

Definition 1.9 (One-sided (k + 1)-term zero-sum sliding-window subspace).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.slidingWindowSpace (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For k : Nat, slidingWindowSpace k is the R-submodule of sequences x : Nat -> R such that sum_{t in Finset.range (k + 1)} x(s + t) = 0 for every start index s : Nat.

Definition 1.10 (Initial-coordinate linear equivalence on the sliding-window subspace).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.slidingWindowEquiv (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For k : Nat, slidingWindowEquiv k : slidingWindowSpace k ≃l[R] (Fin k -> R) evaluates a sequence x on its first k coordinates i |-> x.1 i.val, with explicit (k + 1)-periodic inverse sending v : Fin k -> R at index n : Nat to v (n mod (k + 1)) when n mod (k + 1) < k and to -sum{i : Fin k} v i when n mod (k + 1) = k.

Definition 1.11 (Rectangular sliding-window indicator matrix).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.windowMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For k, L : Nat, windowMatrix k L is the (L - k) x L real matrix D_L whose entry at row s : Fin (L - k) and column d : Fin L equals 1 when s.val <= d.val <= s.val + k and 0 otherwise.

Definition 1.12 (Tail zero-forcing set on the first m - 1 legs).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.spiderTailForcingSet (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For m, k : Nat and leg-length profile ell : Fin m -> Nat, spiderTailForcingSet m k ell collects the leg vertices some <i, d> with i.val < m - 1 (the first m - 1 legs) and ell i - k <= d.val (the last k depths on leg i).

Definition 1.13 (Center-to-leg coupling entry).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.centerCoupling (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For k, d : Nat, centerCoupling k d equals 1 when d + 1 <= k (so 1-based depth d_1 = d + 1 lies within distance k of the center) and 0 otherwise.

Definition 1.14 (Cross-leg coupling entry).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.crossCoupling (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

For k, d, e : Nat, crossCoupling k d e equals 1 when d + 1 <= k - 1, e + 1 <= k - 1, and (d + 1) + (e + 1) <= k (equivalently d + e + 2 <= k, matching 1-based cross-leg distance d_1 + e_1 <= k) and 0 otherwise.

Definition 1.15 (Explicit extremal real symmetric matrix for an unequal-leg spider power).

Formalization. D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.spiderSymmMatrix (✓ std3).

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

On Vertex m ell, spiderSymmMatrix m k ell places 0 at (none, none), centerCoupling k p.2.val between none and any leg vertex some p, crossCoupling k p.2.val q.2.val between vertices on distinct legs, and (D_{ell_i}^T D_{ell_i}){d, e} + crossCoupling k d.val e.val between vertices at 0-based depths d, e on the same leg i, where D{ell_i} = windowMatrix k (ell i).

Theorem 1.16 (Recurrence, dimension, truncation annihilation, and Gram band support of sliding windows).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.sliding_window_kernel_and_band_support (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

Every sequence x : Nat -> R belongs to slidingWindowSpace k if and only if it satisfies the order-k recurrence x(s + k) = -sum_{t < k} x(s + t) for all s : Nat. Consequently, initial-coordinate evaluation slidingWindowEquiv k establishes unique extension from Fin k -> R and gives Module.finrank R (slidingWindowSpace k) = k for every k : Nat (including k = 0). Whenever L >= k + 1, truncating any x in slidingWindowSpace k to Fin L lies in the right kernel of windowMatrix k L, while for all distinct d, e : Fin L the Gram entry ((windowMatrix k L)^T * windowMatrix k L) d e is strictly positive if and only if Nat.dist d.val e.val <= k, realized when Nat.dist d.val e.val <= k by the window start s_0 = max(d.val, e.val) - k < L - k.

Theorem 1.17 (Zero forcing number, maximum symmetric nullity, and minimum symmetric rank of unequal-leg spider powers).

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/UnequalSpiderPowerZeroForcing.unequal_spider_power_zero_forcing (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Aida Abiad; Mary Flagg; Sina Ghasemi Nezhad; Sjanne Zeijlemaker (2026). The Zero Forcing Number of Graph Powers. DOI: 10.48550/arXiv.2610.03892. URL: https://arxiv.org/abs/2610.03892v1.

Commentary.

Assume m >= 2, k >= 1, and ell i >= k + 1 for every i : Fin m. Then Vertex m ell has cardinality N = 1 + sum_i ell i, the graph metric (spiderTree m ell).dist equals distance m ell everywhere, and adjacency in power m k ell coincides with distinctness and spider-tree distance at most k. The tail set spiderTailForcingSet m k ell has cardinality (m - 1) k and zero-forces power m k ell in four phases: inward along each of the first m - 1 legs, from 0-based depth k - 1 on leg 0 to the center, from depths k - t - 2 on leg 0 to depths t < k - 1 on leg m - 1, from the center to depth k - 1 on leg m - 1, and outward along leg m - 1. Conversely, spiderSymmMatrix m k ell belongs to SymGraphMatrices (power m k ell) because nonnegativity of crossCoupling and the Gram band support of windowMatrix k (ell i) match same-leg adjacency while crossCoupling and centerCoupling match cross-leg and center adjacency. Assigning arbitrary sequences from slidingWindowSpace k to the first m - 1 legs and their negative sum to leg m - 1 embeds (Fin (m - 1) x Fin k -> R) injectively into ker(spiderSymmMatrix m k ell), giving nullity >= (m - 1) k. For every H in SymGraphMatrices (power m k ell) and every finite zero-forcing set S, induction along Black shows that any kernel vector of H vanishing on S vanishes on all of Vertex m ell, so matrixNullity H <= S.card. Combining both inequalities with rank-nullity yields matrixNullity (spiderSymmMatrix m k ell) = (m - 1) k, (spiderSymmMatrix m k ell).rank = N - (m - 1) k, the universal bounds and extremal characterizations IsGreatest and IsLeast across SymGraphMatrices (power m k ell), and the exact invariants zeroForcingNumber (power m k ell) = maxSymNullity (power m k ell) = (m - 1) k and minSymRank (power m k ell) = N - (m - 1) k.

References