Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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 content of a concrete three-dimensional parallelepiped computed from its spanning matrix

Example

Let v1=(2,0,0),v2=(1,3,0),v3=(0,1,−2).v_1=(2,0,0),\qquad v_2=(1,3,0),\qquad v_3=(0,1,-2). The parallelepiped spanned by these vectors has Jordan content 1212.

Facts & Assumptions

Given: The three spanning vectors in the statement.

[L1]

The content of a square-matrix parallelepiped is the absolute value of its determinant (The Jordan content of the parallelepiped spanned by the columns of a square real matrix is the absolute value of its determinant).

[L2]

For a commutative ring RR, n≥1n\ge1, and A=(aij)∈Mn(R)A=(a_{ij})\in M_n(R), the determinant is the finite signed-permutation sum det⁡(A)=∑σ∈Snsgn⁡(σ)∏i<naσ(i),i\det(A)=\sum_{\sigma\in S_n}\operatorname{sgn}(\sigma)\prod_{i<n}a_{\sigma(i),i} (For n≥1n\ge1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣|\det A| for a real matrix).

Verification

technique · computation
1.1

Put the vectors into the columns of the upper-triangular matrix A=(21003100−2).A=\begin{pmatrix}2&1&0\\0&3&1\\0&0&-2\end{pmatrix}.

given
2.1

The signed-permutation formula [L2] leaves only the diagonal term, so det⁡A=2⋅3⋅(−2)=−12\det A=2\cdot3\cdot(-2)=-12.

L2step 1.1
3.1

By [L1], the content is ∣−12∣=12|-12|=12. Directly, the first two vectors span a base of area 66 in the horizontal plane and the third has perpendicular height 22, again giving 1212.

L1step 2.1∎

Depends on

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: 73 results over 14 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