Constructive signed matrix multiplication — Exact Proof Explorer

Extend an affine beta-coded matrix slice while preserving every earlier decoded value.

Every finite affine reindexing of a beta-coded natural matrix has its own complete beta code.

Every requested finite matrix row has an explicitly encoded row-major beta slice.

Every requested finite matrix column has an explicitly encoded stride-width beta slice.

Every row and column of two arbitrary finite coded natural matrices has an exactly witnessed product cell.

A nonempty output width constructs the exact row, column and product value of every flat output index.

Append one computed matrix-product cell to a beta-coded row-major prefix without losing any earlier exact cell.

Every finite prefix of the product of arbitrary coded natural matrices admits one complete output beta code.

Arbitrary finite natural matrix multiplication with a nonzero output width has a fully coded row-major output.

Every empty matrix-output prefix has a constructive beta code regardless of the declared dimensions.

Every pair of arbitrary finite natural matrices, including zero-width boundaries, has a complete beta-coded product.

Extend a beta-coded pointwise sum while preserving every earlier decoded summand and sum.

Every pair of finite beta-coded natural vectors has a fully coded exact pointwise sum.

Every pair of arbitrary finite signed natural-pair matrices has a complete exact beta-coded signed matrix product, including all zero-dimensional boundaries.

Every pair of signed natural-pair integers has exact positive and negative multiplication components.

Exact positive and negative multiplication components of two signed pairs are independently unique.

Every pair of arbitrarily long beta-coded signed vectors has an exact constructive signed dot product.

Both natural components of the arbitrary finite signed dot product are independent of all product-code witnesses.

Every arbitrarily long beta-coded signed vector pair has exactly one positive/negative dot-product pair.

Every genuinely signed two-by-two integer matrix has an exact subtraction-free signed determinant pair.

Both natural components of a genuinely signed two-by-two determinant are unique.

Every genuinely signed three-by-three integer matrix has its exact constructive cofactor-expansion determinant pair.

Both exact constructive cofactor components of every signed three-by-three determinant are unique.