CubeSimplexDeterminant

Abstract

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Definition 1.1 (signMatrix).

$$\forall (d:\mathbb{N}),\forall (V:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathrm{Bool}),\mathrm{signMatrix}dV=(\mathrm{fun}ij\mapsto \mathrm{if}Vij\mathrm{then}1\mathrm{else}-1)$$

Formalization. D5/S3/Arith/Lattices/CubeSimplexDeterminant.signMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Definition 1.2 (delta).

$$\forall (d:\mathbb{N}),\mathrm{delta}d=(\mathrm{Finset}.\mathrm{univ}.\sup (\mathrm{fun}V:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathrm{Bool}\mapsto (\mathrm{augment}(\mathrm{signMatrix}dV)).\det .\mathrm{natAbs}))$$

Formalization. D5/S3/Arith/Lattices/CubeSimplexDeterminant.delta (✓ std3).

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.3 (augment map).

$$\forall \{RS:\mathrm{Type}\},[\mathrm{CommRing}R][\mathrm{CommRing}S]\forall \{d:\mathbb{N}\},\forall (f:\mathrm{RingHom}RS),\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))R),\mathrm{augment}(M.\mathrm{map}f)=(\mathrm{augment}M).\mathrm{map}f$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.4 (augmented det smul).

$$\forall \{R:\mathrm{Type}\},[\mathrm{CommRing}R]\forall \{d:\mathbb{N}\},\forall (c:R),\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))R),(\mathrm{augment}(c\cdot M)).\det =c^d\ast (\mathrm{augment}M).\det$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.5 (augmented det integer box bound).

$$\forall \{dm:\mathbb{N}\},(1\le m)\to \forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z}),(\forall ij,|Mij|\le m)\to |(\mathrm{augment}M).\det |\le (\mathrm{delta}d:\mathbb{Z})\ast (m:\mathbb{Z}{)}^d$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.6 (augmented det affine).

$$\forall \{R:\mathrm{Type}\},[\mathrm{CommRing}R]\forall \{d:\mathbb{N}\},\forall (c:R),\forall (a:\mathrm{Fin}d\to R),\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))R),(\mathrm{augment}(\mathrm{Matrix}.\mathrm{of}(\mathrm{fun}ij\mapsto c\ast Mij+ai))).\det =c^d\ast (\mathrm{augment}M).\det$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.7 (exists maximizing sign simplex).

$$\forall (d:\mathbb{N}),\exists V:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z},(\forall ij,|Vij|\le 1)\wedge |(\mathrm{augment}V).\det |=\mathrm{delta}d\wedge (\mathrm{augment}V).\det \ne 0\wedge (\forall j,0\le (\mathrm{augment}V).\det \ast \mathrm{cofactor}Vj)$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

Theorem 1.8 (primitive cofactor admissible).

$$\forall \{dm:\mathbb{N}\},\forall (M:\mathrm{Matrix}(\mathrm{Fin}d)(\mathrm{Fin}(d+1))\mathbb{Z}),(\forall ij,|Mij|\le m)\to ((\mathrm{augment}M).\det \ne 0)\to \forall (s:\mathbb{Z}),(s=1\vee s=-1)\to (\forall j,0<s\ast \mathrm{cofactor}Mj)\to (\mathrm{Finset}.\mathrm{univ}.\gcd (\mathrm{cofactor}M)=1)\to (\mathrm{augment}M).\det .\mathrm{natAbs}\in \mathrm{lengths}dm(d+1)$$

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

Source. Repository-derived.

Commentary.

The absolute augmented determinant on a cube is bounded by its largest value on sign matrices.

References

• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.augment_map
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.augmented_det_affine
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.augmented_det_integer_box_bound
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.augmented_det_smul
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.delta
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.exists_maximizing_sign_simplex
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.primitive_cofactor_admissible
• Truth anchor: D5/S3/Arith/Lattices/CubeSimplexDeterminant.signMatrix
• Dependency: D5/S3/Arith/Lattices/CofactorKernel