Arbitrary dimensions · genuine minors · integer coefficient witnesses · Constructive arithmetic

Integer determinants, rank, and lattice data

det(M) exists · ∃!r.Rank(M,r) · u,v∈Span(M) ⇒ u+v,−u∈Span(M)

Construct actual recursive determinants, exhaustive rectangular rank witnesses, and integer column spans, with representation-independent signed arithmetic and explicit finite codes.

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 9921 native tactic lines and 415 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DL00B4 and follow only the lemmas and conservative definitions supporting positive_determinant_matrix_data_full_rank.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → T13 milestone → theorem and definition dependencies.
Major independently established statements: DL0028 signed_recursive_determinant_exists_unique · DL0083 integer_column_span_add_exists · DL0084 integer_column_span_negate_exists · DL0060 rectangular_matrix_rank_exists_unique · DL0094 signed_recursive_determinant_integer_invariant · DL009F rectangular_matrix_rank_integer_invariant · DL00B5 absolute_recursive_determinant_exists_unique · DL00B6 positive_determinant_matrix_data_exists_unique · DL00B4 positive_determinant_matrix_data_full_rank.
Independently verified Alpha v34 checked-use theorem family: 182 dependency-curried kernel-checked theorem bodies · 415 proof prerequisites · 46 linked definitions · 83 definition-dependency arrows · 9921 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: This branch proves the finite determinant/rank/span substrate. It does not claim Smith or Hermite normal form, lattice index equals determinant, determinant multiplicativity, lattice reduction, or geometry-of-numbers theorems.