How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The naive quaternionic formula is not row-alternating: a matrix with equal rows can have value
Statement refuted
The commutative-ring formula does not define a row-alternating determinant for quaternionic matrices. A matrix with two equal rows can have naive value .
Facts & Assumptions
Given: The quaternionic matrix and the naive expression .
The quaternions have basis elements and real scalar multiplication (The quaternions : real quadruples with componentwise addition and an explicit multiplication formula matching the table on ).
Quaternion multiplication satisfies , , and ( is a division ring that is not commutative, hence not a field: for , while and ).
Over a commutative ring the genuine determinant formula is (The Leibniz formula gives ).
Counterexample
The two rows of are both , so a row-alternating function would vanish on .
The naive expression instead gives . If , then , contrary to [L2]; hence .
Depends on
- The quaternions $\mathbb{H}$: real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$
- $\mathbb{H}$ is a division ring that is not commutative, hence not a field: $q^{-1} = \bar q / N(q)$ for $q \ne 0$, while $ij = k$ and $ji = -k$
- The Leibniz formula gives $\det\begin{pmatrix}a&b\\c&d\end{pmatrix}=ad-bc$
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 72 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Ch. 4 (standard reference, not scraped)