Arbitrary signed cofactor minors · exact 4×4 determinants · T13 partial

Constructive signed matrix minors and determinants

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.

17 kernel- and Lean-verified Alpha-closed theorems · 17 conservative definitions · 25 notation dependencies

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.

34 items
MN0001 matrix_skip_index_exists

Every 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 Stable
MN0002 matrix_skip_index_functional

Deleting one coordinate induces a unique source coordinate, including both threshold branches.

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

A 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 Stable
MN0004 matrix_skip_index_bounded

Every 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 Stable
MN0005 beta_matrix_minor_cell_exists

Every 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 Stable
MN0006 beta_matrix_minor_cell_functional

The 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 Stable
MN0007 beta_matrix_minor_point_exists

Every 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 Stable
MN0008 beta_matrix_minor_prefix_extend

Extend 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 Stable
MN0009 beta_matrix_minor_prefix_exists_nonzero

Every 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 Stable
MN000A beta_matrix_minor_prefix_empty_exists

The zero-dimensional cofactor minor has an unconditional constructive empty beta code.

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

Every 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 Stable
MN000C beta_matrix_minor_exists

Deleting 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 Stable
MN000D beta_signed_matrix_minor_exists

Every 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 Stable
MN000E signed_matrix_four_cofactor_expansion_exists

Four 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 Stable
MN0010 signed_matrix_four_full_determinant_exists

Every 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 Stable
MN0011 signed_matrix_four_full_determinant_functional

Both 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 Stable
PD0002 Lt(a,b)

Witness-defined strict order on natural numbers.

Conservative definition · notation layer 0
PD0001 Le(a,b)

Witness-defined non-strict order on natural numbers.

Conservative definition · notation layer 0
ND0046 MatrixSkipIndex(i,r,s)

The unique order-preserving source coordinate that skips one genuinely deleted matrix row or column.

Conservative definition · notation layer 1
ND0001 Beta(b,c,i,x)

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

Conservative definition · notation layer 0
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
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

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.