MinimalKernelPacking

Abstract

Rounded partial weights encode a minimal nonnegative kernel vector in a finite cube.

Theorem 1.1 (minimal kernel rank deficient bound).

$$\forall \{rkm:\mathbb{N}\},\forall (M:\mathrm{Matrix}(\mathrm{Fin}(r+1))(\mathrm{Fin}k)\mathbb{Z}),(\forall ij,|Mij|\le m)\to (\neg \mathrm{Function}.\mathrm{Injective}(\mathrm{fun}z:\mathrm{Fin}(r+1)\to \mathbb{Z}\mapsto M.\mathrm{transpose}{\ast }_{v}z))\to \forall (x:\mathrm{Fin}k\to \mathbb{N}),(0<\sum j,xj)\to (M{\ast }_v(\mathrm{fun}j\mapsto (xj:\mathbb{Z}))=0)\to (\forall y:\mathrm{Fin}k\to \mathbb{N},y\le x\to M{\ast }_v(\mathrm{fun}j\mapsto (yj:\mathbb{Z}))=0\to y=0\vee y=x)\to \sum j,xj\le (2\ast k\ast m+1{)}^r\ast k$$

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

Source. Repository-derived.

Commentary.

Rounded partial weights encode a minimal nonnegative kernel vector in a finite cube.

Theorem 1.2 (transpose injective of augmented det).

$$\forall \{d:\mathbb{N}\},\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z}),((\mathrm{augment}M).\det \ne 0)\to \mathrm{Function}.\mathrm{Injective}(\mathrm{fun}z:\mathrm{Fin}d\to \mathbb{Z}\mapsto M.\mathrm{transpose}{\ast }_{v}z)$$

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

Source. Repository-derived.

Commentary.

Rounded partial weights encode a minimal nonnegative kernel vector in a finite cube.

Theorem 1.3 (augmented det ne zero of full rank positive).

$$\forall \{d:\mathbb{N}\},\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z}),(\mathrm{Function}.\mathrm{Injective}(\mathrm{fun}z:\mathrm{Fin}d\to \mathbb{Z}\mapsto M.\mathrm{transpose}{\ast }_{v}z))\to \forall (x:\mathrm{Fin}(d+1)\to \mathbb{Z}),(M{\ast }_{v}x=0)\to (\sum j,xj\ne 0)\to (\mathrm{augment}M).\det \ne 0$$

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

Source. Repository-derived.

Commentary.

Rounded partial weights encode a minimal nonnegative kernel vector in a finite cube.

References

• Truth anchor: D5/S3/Arith/Lattices/MinimalKernelPacking.augmented_det_ne_zero_of_full_rank_positive
• Truth anchor: D5/S3/Arith/Lattices/MinimalKernelPacking.minimal_kernel_rank_deficient_bound
• Truth anchor: D5/S3/Arith/Lattices/MinimalKernelPacking.transpose_injective_of_augmented_det
• Dependency: D5/S3/Arith/Lattices/CofactorKernel