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

Constructive signed matrix minors and determinants

∀M,q,r,d. r,d<S(q) ⇒ ∃N. SignedMinor(M,S(q),r,d,N,q)

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.

Open the definition-aware map Read the final theorem See campaign milestone T13

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.

Exact certificate

Fully expanded arithmetic

Inspect all 602 native tactic lines and 28 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MN000D and follow only the lemmas and conservative definitions supporting beta_signed_matrix_minor_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → T13 milestone → theorem and definition dependencies.
Major independently established statements: MN0003 matrix_skip_index_avoids_removed · MN0006 beta_matrix_minor_cell_functional · MN000E signed_matrix_four_cofactor_expansion_exists · MN0010 signed_matrix_four_full_determinant_exists · MN0011 signed_matrix_four_full_determinant_functional · MN000C beta_matrix_minor_exists · MN000D beta_signed_matrix_minor_exists.
Independently verified Alpha v34 checked-use theorem family: 17 dependency-curried kernel-checked theorem bodies · 28 proof prerequisites · 17 linked definitions · 25 definition-dependency arrows · 602 exact tactic lines · first admitted v24 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 203 bundle nodes; SHA-256 627e39ed29b10db48bf37d5bef8750d48009a7524c822a7c5e7c83e96a8e9cf9.
Exact mathematical boundary: Historical partial components only: this chapter proves arbitrary signed cofactor minors and exact signed determinants through dimension four. T13 is now closed by the separate Alpha-v27 integer-linear-algebra branch: arbitrary determinant data, rank, and integer column spans, without a claim of lattice index or normal forms.

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