CofactorKernel

Abstract

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Definition 1.1 (IsMinimalZeroSum).

$\forall {d : N}, \forall (f : (Fin d \to Z) \to_{0} N), IsMinimalZeroSum f = (f \neq = 0 \land (fun f : (Fin d \to Z) \to_{0} N \mapsto f . sum (fun v n \mapsto (n : Z) \cdot v)) f = 0 \land \forall g : (Fin d \to Z) \to_{0} N, g \leq f \to g \neq = 0 \to g \neq = f \to (fun f : (Fin d \to Z) \to_{0} N \mapsto f . sum (fun v n \mapsto (n : Z) \cdot v)) g \neq = 0)$

Formalization. D5/S3/Arith/Lattices/CofactorKernel.IsMinimalZeroSum (✓ std3).

Citation. Benjamin Girard and Alain Plagne (2026). The Davenport constant of low-dimensional boxes. DOI: 10.48550/arXiv.2610.16562. URL: https://arxiv.org/abs/2610.16562v1.

Commentary.

Section 1, printed page 1: “Moreover, if S is a zero-sum sequence such that ∑ᵢ∈ᴵ xᵢ ≠ 0 for every ∅ ≠ I ⊊ ⟦1, ℓ⟧, it will be called a minimal zero-sum sequence.” A multiplicity function is nonzero, has zero total, and has no nonempty proper zero-sum subfunction.

Definition 1.2 (lengths).

$\forall (d mk : N), lengths d mk = ({L ∣\exists f : (Fin d \to Z) \to_{0} N, IsMinimalZeroSum f \land (CoeTC . coe f . support : Set (Fin d \to Z)) \subseteq (fun d m \mapsto {v : Fin d \to Z ∣\forall i, ∣ v i ∣ \leq (m : N)}) d m \land f . support . card = k \land (f . sum fun_{n} \mapsto n) = L})$

Formalization. D5/S3/Arith/Lattices/CofactorKernel.lengths (✓ std3).

Citation. Benjamin Girard and Alain Plagne (2026). The Davenport constant of low-dimensional boxes. DOI: 10.48550/arXiv.2610.16562. URL: https://arxiv.org/abs/2610.16562v1.

Commentary.

Section 2, printed page 2: “we study the quantity D^(d+1)(⟦−m, m⟧^d) which is defined as the maximal length of a minimal zero-sum sequence over ⟦−m, m⟧^d having a support of size d + 1.” Multiplicity functions use pointwise subsequence order; support cardinality counts distinct vectors.

Definition 1.3 (augment).

$\forall {R : Type}, [One R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), augment M = (Fin . cases (fun_{\mapsto} 1) M)$

Formalization. D5/S3/Arith/Lattices/CofactorKernel.augment (✓ std3).

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.4 (augment zero).

$\forall {R : Type}, [One R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), \forall (j : Fin (d + 1)), augment M 0 j = 1$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.augment_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.5 (augment succ).

$\forall {R : Type}, [One R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), \forall (i : Fin d), \forall (j : Fin (d + 1)), augment M i . succ j = M ij$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.augment_succ (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Definition 1.6 (cofactor).

$\forall {R : Type}, [CommRing R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), \forall (j : Fin (d + 1)), cofactor M j = ((- 1)^{j . val} * (M . submatrix id j . succAbove) . det)$

Formalization. D5/S3/Arith/Lattices/CofactorKernel.cofactor (✓ std3).

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.7 (cofactor eq adjugate).

$\forall {R : Type}, [CommRing R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), \forall (j : Fin (d + 1)), cofactor M j = (augment M) . adjugate j 0$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.cofactor_eq_adjugate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.8 (cofactor mulVec eq zero).

$\forall {R : Type}, [CommRing R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), M *_{v} cofactor M = 0$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.cofactor_mulVec_eq_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.9 (sum cofactor eq det).

$\forall {R : Type}, [CommRing R] \forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) R), \sum j, cofactor M j = (augment M) . det$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.sum_cofactor_eq_det (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.10 (Cofactor cross identity for a kernel vector).

$(augment M) . det \cdot x i = (\sum j x j) \cdot cofactor M i$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.kernel_cross_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact compiled declaration retains an arbitrary commutative ring R, d, the full d by d+1 matrix M, vector x, original kernel equation hx, and coordinate i. For a d by d+1 matrix over any commutative ring and a vector in its kernel, the determinant of the matrix augmented by a first row of ones times coordinate i equals the sum of the vector coordinates times signed cofactor i. The sign is (-1) to the column index and the minor deletes that column by succAbove. This is the classical adjugate/cofactor expansion identity used by the integer-kernel results. Over the reals, a strictly positive kernel vector and one nonzero cofactor force a nonzero augmented determinant and positive proportionality after choosing an orientation. The nonnegative-kernel cofactor completeness theorem consumes this identity; selected-row kernel membership alone does not establish the original row equations.

Definition 1.11 (fromWeights).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), fromWeights vx = (Finsupp . embDomain v (Finsupp . equivFunOnFinite . symm x))$

Formalization. D5/S3/Arith/Lattices/CofactorKernel.fromWeights (✓ std3).

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.12 (fromWeights apply).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), \forall (i : Fin k), fromWeights vx (v i) = x i$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.fromWeights_apply (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.13 (fromWeights support subset).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), (CoeTC . coe (fromWeights vx) . support : Set (Fin d \to Z)) \subseteq Set . range v$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.fromWeights_support_subset (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.14 (fromWeights restrict).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (f : (Fin d \to Z) \to_{0} N), ((CoeTC . coe f . support : Set (Fin d \to Z)) \subseteq Set . range v) \to fromWeights v (fun i \mapsto f (v i)) = f$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.fromWeights_restrict (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.15 (length fromWeights).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), Finsupp . degree (fromWeights vx) = \sum j, x j$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.length_fromWeights (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.16 (fromWeights minimal of primitive).

$\forall {d : N}, \forall (v : Function . Embedding (Fin (d + 1)) (Fin d \to Z)), ((augment ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose)) . det \neq = 0) \to \forall (x : Fin (d + 1) \to Z), ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose *_{v} x = 0) \to (\forall i, 0 < x i) \to (Finset . univ . gcd x = 1) \to IsMinimalZeroSum (fromWeights v (fun i \mapsto (x i) . toNat))$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.fromWeights_minimal_of_primitive (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.17 (total fromWeights eq mulVec).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), (fun f : (Fin d \to Z) \to_{0} N \mapsto f . sum (fun v n \mapsto (n : Z) \cdot v)) (fromWeights vx) = (Matrix . of (v : Fin k \to Fin d \to Z)) . transpose *_{v} (fun j \mapsto (x j : Z))$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.total_fromWeights_eq_mulVec (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.18 (fromWeights minimal to vector).

$\forall {d k : N}, \forall (v : Function . Embedding (Fin k) (Fin d \to Z)), \forall (x : Fin k \to N), (IsMinimalZeroSum (fromWeights vx)) \to \forall (y : Fin k \to N), (y \leq x) \to ((Matrix . of (v : Fin k \to Fin d \to Z)) . transpose *_{v} (fun j \mapsto (y j : Z)) = 0) \to y = 0 \lor y = x$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.fromWeights_minimal_to_vector (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.19 (sequence cofactor length).

$\forall {d : N}, \forall (v : Function . Embedding (Fin (d + 1)) (Fin d \to Z)), \forall (x : Fin (d + 1) \to N), (\forall i, 0 < x i) \to (IsMinimalZeroSum (fromWeights vx)) \to ((augment ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose)) . det \neq = 0) \to ∣ (augment ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose)) . det ∣ = (Finsupp . degree (fromWeights vx) : Z) * Finset . univ . gcd (cofactor ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose))$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.sequence_cofactor_length (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.20 (sequence cofactor multiplicities).

$\forall {d : N}, \forall (v : Function . Embedding (Fin (d + 1)) (Fin d \to Z)), \forall (x : Fin (d + 1) \to N), (\forall i, 0 < x i) \to (IsMinimalZeroSum (fromWeights vx)) \to ((augment ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose)) . det \neq = 0) \to (\forall i, (x i : Z) = ∣ cofactor ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose) i ∣/ Finset . univ . gcd (cofactor ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose))) \land (Finsupp . degree (fromWeights vx) : Z) = ∣ (augment ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose)) . det ∣/ Finset . univ . gcd (cofactor ((Matrix . of (v : Fin (d + 1) \to Fin d \to Z)) . transpose))$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.sequence_cofactor_multiplicities (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.21 (positive kernel orientation).

$\forall {d : N}, \forall (A : Matrix (Fin d) (Fin (d + 1)) Z), ((augment A) . det \neq = 0) \to \forall (x : Fin (d + 1) \to Z), (\forall j, 0 < x j) \to (A *_{v} x = 0) \to \exists s : Z, (s = 1 \lor s = - 1) \land \forall j, 0 < s * cofactor A j$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.positive_kernel_orientation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.22 (augmented det ne zero of oriented cofactors).

$\forall {d : N}, \forall (A : Matrix (Fin d) (Fin (d + 1)) Z), \forall (s : Z), (\forall j, 0 < s * cofactor A j) \to (augment A) . det \neq = 0$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.augmented_det_ne_zero_of_oriented_cofactors (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.23 (cofactor gcd one mul right).

$\forall {d : N}, \forall (M : Matrix (Fin d) (Fin (d + 1)) Z), \forall (W : Matrix (Fin (d + 1)) (Fin (d + 1)) Z), (IsUnit W . det) \to (Finset . univ . gcd (cofactor M) = 1) \to Finset . univ . gcd (cofactor (M * W)) = 1$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.cofactor_gcd_one_mul_right (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

Theorem 1.24 (cofactor gcd one mul left).

$\forall {d : N}, \forall (U : Matrix (Fin d) (Fin d) Z), \forall (M : Matrix (Fin d) (Fin (d + 1)) Z), (IsUnit U . det) \to (Finset . univ . gcd (cofactor M) = 1) \to Finset . univ . gcd (cofactor (U * M)) = 1$

Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/CofactorKernel.cofactor_gcd_one_mul_left (✓ std3). ∎

Source. Repository-derived.

Commentary.

Primitive positive integer kernels give the multiplicities and lengths of minimal zero-sum sequences.

References

Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.IsMinimalZeroSum
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.augment
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.augment_succ
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.augment_zero
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.augmented_det_ne_zero_of_oriented_cofactors
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.cofactor
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.cofactor_eq_adjugate
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.cofactor_gcd_one_mul_left
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.cofactor_gcd_one_mul_right
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.cofactor_mulVec_eq_zero
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights_apply
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights_minimal_of_primitive
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights_minimal_to_vector
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights_restrict
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.fromWeights_support_subset
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.kernel_cross_identity
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.length_fromWeights
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.lengths
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.positive_kernel_orientation
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.sequence_cofactor_length
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.sequence_cofactor_multiplicities
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.sum_cofactor_eq_det
Truth anchor: D5/S3/Arith/Lattices/CofactorKernel.total_fromWeights_eq_mulVec

Keyboard shortcuts

trureturing — Discovering truth

CofactorKernel

Abstract

References