MN0001 matrix_skip_index_existsEvery minor coordinate has a constructive source coordinate that skips an arbitrary deleted index.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableArbitrary signed cofactor minors · exact 4×4 determinants · T13 partial
Seventeen independently checked constructive theorems delete arbitrary rows and columns from genuinely signed beta-coded matrices of every finite dimension and construct exact signed four-by-four determinants.
Alpha v34 checked-use · first admitted v24 · 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.
MN0001 matrix_skip_index_existsEvery minor coordinate has a constructive source coordinate that skips an arbitrary deleted index.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0002 matrix_skip_index_functionalDeleting one coordinate induces a unique source coordinate, including both threshold branches.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0003 matrix_skip_index_avoids_removedA skipped matrix coordinate never equals the row or column that was actually deleted.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0004 matrix_skip_index_boundedEvery minor coordinate below width q maps to an original coordinate strictly below S q.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0005 beta_matrix_minor_cell_existsEvery coordinate of an arbitrary deleted-row/deleted-column matrix minor has its exact decoded source value.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0006 beta_matrix_minor_cell_functionalThe decoded value of a beta-coded cofactor minor is independent of every skipped-coordinate witness.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0007 beta_matrix_minor_point_existsEvery flat index of a nonempty cofactor-minor row has genuine quotient, remainder and skipped-source witnesses.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0008 beta_matrix_minor_prefix_extendExtend one exact row-major beta-coded cofactor minor while preserving every earlier skipped-source entry.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0009 beta_matrix_minor_prefix_exists_nonzeroEvery finite prefix of a nonempty arbitrary-dimensional cofactor minor has one complete beta code.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000A beta_matrix_minor_prefix_empty_existsThe zero-dimensional cofactor minor has an unconditional constructive empty beta code.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000B beta_matrix_minor_prefix_existsEvery arbitrary finite rectangular deleted-row/deleted-column matrix prefix is beta-coded, including width zero.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000C beta_matrix_minor_existsDeleting any valid row and column from an unrestricted square beta-coded natural matrix constructs its complete exact square cofactor minor.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000D beta_signed_matrix_minor_existsEvery arbitrary-dimensional signed integer matrix has the complete exact beta-coded minor obtained by deleting any valid row and column.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000E signed_matrix_four_cofactor_expansion_existsFour arbitrary signed first-row entries and four signed minor determinants have their exact alternating subtraction-free Laplace cofactor expansion.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN000F signed_matrix_four_cofactor_expansion_functionalBoth natural components of a four-term signed Laplace cofactor expansion are unique.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0010 signed_matrix_four_full_determinant_existsEvery genuinely signed four-by-four integer matrix has its exact constructive first-row cofactor determinant with all 32 natural entry components.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StableMN0011 signed_matrix_four_full_determinant_functionalBoth exact subtraction-free components of every signed four-by-four cofactor determinant are independent of the witnesses.
Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not StablePD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0ND0046 MatrixSkipIndex(i,r,s)The unique order-preserving source coordinate that skips one genuinely deleted matrix row or column.
Conservative definition · notation layer 1ND0001 Beta(b,c,i,x)Exact hygienic Gödel-beta extraction; a signature-identical alias of checked BetaAt.
Conservative definition · notation layer 0ND0047 MatrixMinorCell(b,c,w,r,d,i,j,z)The exact beta-decoded source entry after independently skipping the removed row and column.
Conservative definition · notation layer 2ND0048 MatrixMinorPrefix(b,c,w,r,d,u,v,q,l)One complete row-major beta code containing every genuine skipped-row/skipped-column matrix entry.
Conservative definition · notation layer 3ND0049 SignedMatrixMinor(pb,pc,nb,nc,w,r,d,q,up,us,un,ut)Both complete independently beta-coded natural components of a genuine signed square cofactor minor.
Conservative definition · notation layer 4ND0003 MatrixAt(b,c,w,i,j,z)The exact natural matrix entry stored at flattened beta index i*w+j.
Conservative definition · notation layer 1ND0005 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 1PD0013 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 2ND0013 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 1ND0017 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.