MC0001 beta_affine_matrix_slice_extendExtend 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 StableBeta-coded slices · arbitrary signed products · exact signed determinants
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.
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.
MC0001 beta_affine_matrix_slice_extendExtend 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 StableMC0002 beta_affine_matrix_slice_existsEvery 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 StableMC0003 beta_matrix_row_slice_existsEvery 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 StableMC0004 beta_matrix_column_slice_existsEvery 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 StableMC0005 beta_matrix_product_cell_existsEvery 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 StableMC0006 beta_matrix_product_point_existsA 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 StableMC0007 beta_matrix_product_prefix_extendAppend 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 StableMC0008 beta_matrix_product_prefix_exists_nonzeroEvery 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 StableMC0009 beta_matrix_product_exists_nonzero_widthArbitrary 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 StableMC000A beta_matrix_product_empty_existsEvery 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 StableMC000B beta_matrix_product_existsEvery 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 StableMC000C beta_pointwise_add_prefix_extendExtend 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 StableMC000D beta_pointwise_add_prefix_existsEvery 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 StableMC000E beta_signed_matrix_product_existsEvery 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 StableMC000F signed_pair_product_existsEvery 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 StableMC0010 signed_pair_product_functionalExact 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 StableMC0011 beta_signed_dot_product_existsEvery 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 StableMC0012 beta_signed_dot_product_functionalBoth 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 StableMC0013 beta_signed_dot_product_exists_uniqueEvery 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 StableMC0014 signed_matrix_two_full_determinant_existsEvery 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 StableMC0015 signed_matrix_two_full_determinant_functionalBoth natural components of a genuinely signed two-by-two determinant are unique.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableMC0016 signed_matrix_three_full_determinant_existsEvery 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 StableMC0017 signed_matrix_three_full_determinant_functionalBoth exact constructive cofactor components of every signed three-by-three determinant are unique.
Alpha v34 checked-use · first admitted v21 · independently kernel and Lean verified; not StableND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0ND0003 MatrixAt(b,c,w,i,j,z)The exact natural matrix entry stored at flattened beta index i*w+j.
Conservative definition · notation layer 1PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1ND0004 DotProduct(b,c,d,e,ell,z)The witnessed sum of the pointwise products of two beta-coded natural vectors.
Conservative definition · notation layer 2ND0005 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 0ND0012 MatrixAffineSlice(b,c,s,d,u,v,l)A complete beta-coded affine matrix slice whose exact target entry at i equals the source entry at s+d*i.
Conservative definition · notation layer 1ND0013 MatrixProductCell(lb,lc,rb,rc,w,v,i,j,n)An exact natural matrix multiplication cell with witnessed beta-coded row, column and finite dot product.
Conservative definition · notation layer 3ND0014 MatrixProductPrefix(lb,lc,rb,rc,w,v,tb,tc,l)Every bounded row-major natural matrix product cell together with its exact coordinate, strict column bound and output beta witness.
Conservative definition · notation layer 4ND0015 MatrixPointwiseAdd(mb,mc,sb,sc,tb,tc,l)The complete beta-coded pointwise sum of two exact bounded natural vector prefixes.
Conservative definition · notation layer 1ND0016 SignedDotProduct(ab,ac,db,dc,eb,ec,fb,fc,l,p,n)The exact positive and negative components of an arbitrary finite signed-vector dot product, witnessed by four natural dot products.
Conservative definition · notation layer 3ND0017 SignedMatrixProduct(ab,ac,db,dc,eb,ec,fb,fc,w,v,r,pb,pc,nb,nc)The exact complete signed finite matrix product: four natural coded products and two beta-coded pointwise-summed positive/negative output matrices.
Conservative definition · notation layer 5Only 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.