MD0001 beta_matrix_cell_existsEvery requested finite matrix coordinate has a witnessed beta-decoded entry.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableCurrent 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.
MD0002 beta_matrix_cell_functionalThe decoded natural value of every flattened matrix cell is unique.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0003 beta_matrix_cell_exists_uniqueEvery finite beta-coded matrix entry has exactly one actual value.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0004 beta_dot_product_existsTwo arbitrary finite coded vectors have an exactly witnessed dot product.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0005 beta_dot_product_functionalThe exact finite dot-product value is independent of its coding witness.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0006 beta_dot_product_exists_uniqueEvery pair of coded finite vectors has exactly one natural dot product.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0007 beta_dot_product_emptyThe exact dot product of two empty finite vectors is zero.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0008 beta_dot_product_commutativeFinite natural dot products are constructively symmetric.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD0009 signed_matrix_two_determinant_existsEvery natural 2-by-2 matrix has an exact signed-pair determinant witness.
Alpha v34 checked-use · first admitted v20 · independently kernel and Lean verified; not StableMD000A signed_matrix_two_determinant_functionalThe positive/negative natural components of a 2-by-2 determinant are unique.
Alpha v34 checked-use · first admitted v20 · 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 0PD0002 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 1ND0003 MatrixAt(b,c,w,i,j,z)The exact natural matrix entry stored at flattened beta index i*w+j.
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 0Only 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.