Matrix cells · dot products · signed 2×2 determinants · Constructive arithmetic

Finite matrices and dot products

DotProduct(b,c,d,e,ℓ,z) · det₂ = ad − bc

Ten independently checked constructive results establish total finite matrix entries, unique natural dot products, commutativity, and exact signed two-by-two determinant components.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MD0006 and follow only the lemmas and conservative definitions supporting beta_dot_product_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → T13 milestone → theorem and definition dependencies.
Major independently established statements: MD0003 beta_matrix_cell_exists_unique · MD000A signed_matrix_two_determinant_functional · MD0006 beta_dot_product_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 10 dependency-curried kernel-checked theorem bodies · 13 proof prerequisites · 7 linked definitions · 6 definition-dependency arrows · 263 exact tactic lines · first admitted v20 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 590 bundle nodes; SHA-256 1b623064f36e362c1a117daa193b1ee33ee7905ec804ee1ac164b42345b67069.
Exact mathematical boundary: Historical partial components only: these ten matrix and dot-product proofs do not themselves establish the full T13 substrate. T13 is now closed in the separate Alpha-v27 integer-linear-algebra branch with arbitrary determinant data, rank, and integer column spans; this does not claim lattice index or normal-form theorems.

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