Beta-coded slices · arbitrary signed products · exact signed determinants · Constructive arithmetic

Constructive signed matrix multiplication

(A⁺−A⁻)(B⁺−B⁻) = (A⁺B⁺+A⁻B⁻) − (A⁺B⁻+A⁻B⁺)

Twenty-three independently checked constructive theorems establish arbitrary natural and signed matrix multiplication, unique signed dot products, and genuine signed two- and three-dimensional 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 998 native tactic lines and 41 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MC000E and follow only the lemmas and conservative definitions supporting beta_signed_matrix_product_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → T13 milestone → theorem and definition dependencies.
Major independently established statements: MC000B beta_matrix_product_exists · MC0013 beta_signed_dot_product_exists_unique · MC0016 signed_matrix_three_full_determinant_exists · MC000E beta_signed_matrix_product_exists.
Independently verified Alpha v34 checked-use theorem family: 23 dependency-curried kernel-checked theorem bodies · 41 proof prerequisites · 13 linked definitions · 18 definition-dependency arrows · 998 exact tactic lines · first admitted v21 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 209 bundle nodes; SHA-256 65ecae7cb6b3e102790efa281451db3da5ab83868afcf9d57e6656f7a3eafda0.
Exact mathematical boundary: Historical partial components only: this chapter proves arbitrary natural and signed matrix multiplication and signed two-/three-dimensional determinants. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with arbitrary determinant data, rank, and integer column spans; lattice index and normal forms are outside that scope.

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