Beta-coded slices · arbitrary signed products · exact signed determinants

Constructive signed matrix multiplication

Twenty-three independently checked constructive theorems establish arbitrary natural and signed matrix multiplication, unique signed dot products, and genuine signed two- and three-dimensional determinants.

23 kernel- and Lean-verified Alpha-closed theorems · 13 conservative definitions · 18 notation dependencies

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

36 items
MC0001 beta_affine_matrix_slice_extend

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0002 beta_affine_matrix_slice_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0003 beta_matrix_row_slice_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0004 beta_matrix_column_slice_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0005 beta_matrix_product_cell_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0006 beta_matrix_product_point_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0007 beta_matrix_product_prefix_extend

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0008 beta_matrix_product_prefix_exists_nonzero

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0009 beta_matrix_product_exists_nonzero_width

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000A beta_matrix_product_empty_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000B beta_matrix_product_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000C beta_pointwise_add_prefix_extend

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000D beta_pointwise_add_prefix_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000E beta_signed_matrix_product_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC000F signed_pair_product_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0010 signed_pair_product_functional

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0011 beta_signed_dot_product_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0012 beta_signed_dot_product_functional

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0013 beta_signed_dot_product_exists_unique

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0014 signed_matrix_two_full_determinant_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
MC0016 signed_matrix_three_full_determinant_exists

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

Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not Stable
ND0001 Beta(b,c,i,x)

Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.

Conservative definition · notation layer 0
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0013 BetaAt(b,c,i,x)

x is the bounded beta-decoded value at index i.

Conservative definition · notation layer 0
PD0015 Sum(b,c,l,z)

z is the sum of a beta-coded prefix of length l.

Conservative definition · notation layer 1
ND0005 SignedDet2(a,b,c,d,p,n)

The exact positive and negative natural components p=ad and n=bc of a signed 2×2 determinant.

Conservative definition · notation layer 0

Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.

Separate complete second-wave branches: Full T13 proof · Alpha v27.