PrimitivePencil

Abstract

Every full row rank integer matrix admits one perturbation with primitive maximal minors for all integer parameters.

Theorem 1.1 (primitive pencil perturbation).

$$\forall \{d:\mathbb{N}\},\forall (A:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z}),(\mathrm{Function}.\mathrm{Injective}(\mathrm{fun}x:\mathrm{Fin}d\to \mathbb{Z}\mapsto A.\mathrm{transpose}{\ast }_{v}x))\to \exists B:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z},\forall t:\mathbb{Z},\mathrm{Finset}.\mathrm{univ}.\gcd (\mathrm{cofactor}(t\cdot A+B))=1$$

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

Source. Repository-derived.

Commentary.

Every full row rank integer matrix admits one perturbation with primitive maximal minors for all integer parameters.

References

• Truth anchor: D5/S3/Arith/Lattices/PrimitivePencil.primitive_pencil_perturbation
• Dependency: D5/S3/Arith/Lattices/CofactorKernel