Alphabeta Math
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.

✓ 12 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 12 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Tensor Fields Exterior Algebra and Differential Forms — Examples

1 · Prerequisites

2 · Summary

These examples turn the abstract tensor and form operations into coordinate computations, and they isolate the exact places where sign, degree, and functoriality matter.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Tensor product and contraction in a basis

Example

On V=R2 with basis (e1,e2) and dual basis (e1,e2), let

S=e1,T=e2,R=e1⊗e1+e2⊗e2.

Then

S⊗T=e1⊗e2,ctr⁡(R)=2.

Facts & Assumptions

Given: The basis (e1,e2), its dual basis (e1,e2), and the tensors S,T,R above.

[L1]

Tensor product multiplies the factor values on concatenated arguments, and contraction is basis-independent (Tensor product of multilinear tensors is associative and bilinear, Contraction is independent of the basis formula).

Verification

technique · direct
1.1L1givenalgebra

For vectors (a1,a2) and (b1,b2), [L1] gives (S⊗T)((a1,a2),(b1,b2))=S(a1,a2) T(b1,b2)=a1b2, so S⊗T=e1⊗e2.

1.2L1givenalgebra

Again by [L1], ctr⁡(R)=R(e1,e1)+R(e2,e2)=1+1=2.

2.1step 1.1step 1.2∎

This computes the announced tensor product and contraction.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

A bilinear form as a type (0,2) tensor

Example

On R2, the dot product

g((a,b),(c,d)):=ac+bd

is a type (0,2) tensor.

Facts & Assumptions

Given: The bilinear form g on R2 defined above.

[F1]

A type (0,2) tensor is a bilinear map V×V→R (A type (r,s) tensor on a finite-dimensional vector space).

Verification

technique · direct
1.1givenalgebra

The displayed formula is linear in (a,b) and in (c,d) separately, so g is bilinear.

2.1F1step 1.1

By [F1], bilinearity is exactly the requirement for a type (0,2) tensor. Hence g is such a tensor.

3.1step 2.1∎

Therefore the Euclidean dot product is a concrete type (0,2) tensor.

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

An endomorphism as a type (1,1) tensor

Example

Let A:R2→R2 be the linear map

A(x,y)=(x+2y,3x−y).

Then

T(α,v):=α(Av)

defines a type (1,1) tensor on R2.

Facts & Assumptions

Given: The endomorphism A and the function T(α,v)=α(Av).

[F1]

A type (1,1) tensor is bilinear on V∗×V (A type (r,s) tensor on a finite-dimensional vector space).

Verification

technique · direct
1.1givenalgebra

For fixed v, the map α↦α(Av) is linear because evaluation of a fixed vector is linear on V∗. For fixed α, the map v↦α(Av) is linear because A and α are linear. Thus T is bilinear on (R2)∗×R2.

2.1F1step 1.1

By [F1], this means T is a type (1,1) tensor.

3.1step 2.1∎

Therefore an endomorphism gives a concrete type (1,1) tensor through evaluation.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The identity endomorphism and its coordinate-independent trace

Example

For the identity endomorphism id⁡Rn, the associated type (1,1) tensor has contraction n, so its trace is n in every basis.

Facts & Assumptions

Given: A basis e1,…,en of Rn with dual basis e1,…,en, and the identity endomorphism.

[F1]

Contraction is the dual-basis sum ∑iT(ei,ei) (The contraction of a mixed tensor).

[F2]

Trace of an endomorphism is the sum of the diagonal entries in any basis (The basis-independent trace of an endomorphism of a finite-dimensional vector space).

Verification

technique · direct
1.1F1givenalgebra

The tensor associated to id⁡Rn is T(α,v)=α(v). Therefore [F1] gives ctr⁡(T)=∑i=1nei(ei)=n.

2.1F2step 1.1algebra

In the chosen basis, the matrix of the identity endomorphism is the identity matrix, so [F2] gives trace n. This agrees with step 1.1, and neither value depends on the basis.

3.1step 2.1∎

Thus the identity endomorphism has coordinate-independent trace n.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Wedge products of the standard dual basis

Example

On R3 with standard dual basis dx,dy,dz,

dx∧dy=−dy∧dx,dx∧dx=0,dx∧dy∧dz

is a basis of Alt⁡3(R3).

Facts & Assumptions

Given: The standard basis of R3 and its dual basis dx,dy,dz.

[L1]

The wedge product is graded commutative (The wedge product is associative and graded commutative).

[L2]

Increasing wedge monomials in a dual basis form a basis of each exterior-power space (Wedge monomials in a dual basis form a basis).

Verification

technique · direct
1.1L1givenalgebra

Since dx and dy are 1-forms, [L1] gives dx∧dy=−dy∧dx and dx∧dx=−dx∧dx, hence dx∧dx=0.

1.2L2given

By [L2], the unique increasing triple wedge dx∧dy∧dz forms a basis of Alt⁡3(R3).

2.1step 1.1step 1.2∎

These are the standard wedge-product identities in the dual basis.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Determinant as the pairing of top exterior powers

Example

On Rn with standard basis e1,…,en and dual basis e1,…,en, the pairing

⟨e1∧⋯∧en, v1∧⋯∧vn⟩

is exactly det⁡[v1 ⋯ vn].

Facts & Assumptions

Given: Vectors v1,…,vn∈Rn.

[L1]

The exterior-power pairing on decomposable elements is the determinant of the evaluation matrix (Exterior-power duality pairing).

[L2]

The top exterior power is one-dimensional (The top exterior power is one-dimensional).

Verification

technique · direct
1.1given

The matrix with entries ei(vj) is exactly the coordinate matrix [v1 ⋯ vn] of the ordered n-tuple (v1,…,vn).

2.1L1step 1.1algebra

Applying [L1] to αi=ei gives ⟨e1∧⋯∧en, v1∧⋯∧vn⟩=det⁡(ei(vj))=det⁡[v1 ⋯ vn].

3.1L2step 2.1

By [L2], this scalar determines the decomposable top wedge relative to the standard volume form.

4.1step 2.1step 3.1∎

Thus the determinant is the top-degree pairing against e1∧⋯∧en.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The Euclidean metric as a symmetric two-tensor

Example

On Rn, the Euclidean metric

g=∑i=1ndxi⊗dxi

is a smooth section of the symmetric subbundle of T20Rn.

Facts & Assumptions

Given: The Euclidean metric g on Rn.

[F1]

The symmetric two-tensors form a fibrewise subbundle of the covariant tensor bundle (Symmetric and alternating covariant tensor subbundles).

[L1]

That fibrewise symmetric part is a smooth vector subbundle (Symmetric and alternating images are smooth subbundles).

Verification

technique · direct
1.1given

The coefficients of g in the standard coordinates are constant, so g is smooth.

2.1F1L1step 1.1

For vectors u,v, one has g(u,v)=g(v,u), so each fibre value gp is symmetric. Hence [F1] places g in the symmetric fibrewise part, and [L1] identifies that part as a smooth subbundle.

3.1step 2.1∎

Therefore the Euclidean metric is a symmetric smooth two-tensor.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The area form in polar coordinates

Example

On the polar chart domain {(r,θ):r>0}, the Euclidean area form pulls back as

F∗(dx∧dy)=r dr∧dθ,

where F(r,θ)=(rcos⁡θ,rsin⁡θ).

Facts & Assumptions

Given: The polar-coordinate map F(r,θ)=(rcos⁡θ,rsin⁡θ).

[F1]

Pullback of a differential form is defined by composing with the differential (The pullback of a differential form).

[L1]

Verification

technique · direct
1.1F1givenalgebra

By [F1], F∗dx=cos⁡θ dr−rsin⁡θ dθ,F∗dy=sin⁡θ dr+rcos⁡θ dθ.

2.1L1step 1.1algebra

Using [L1] and bilinearity of the wedge product, F∗(dx∧dy)=F∗dx∧F∗dy=(cos⁡θ dr−rsin⁡θ dθ)∧(sin⁡θ dr+rcos⁡θ dθ)=r dr∧dθ.

3.1step 2.1∎

Thus the area form becomes r dr∧dθ in polar coordinates.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

Pullback of the circle angular form along a parametrized curve

Example

Let c:R→S1⊆R2 be the parametrized unit circle c(t)=(cos⁡t,sin⁡t), and let

η=−y dx+x dy.

Then

c∗η=dt.

Facts & Assumptions

Given: The curve c(t)=(cos⁡t,sin⁡t) and the 1-form η=−y dx+x dy.

[F1]

Pullback of a differential form is defined by composing with the differential (The pullback of a differential form).

Verification

technique · direct
1.1F1givenalgebra

Along the curve, x∘c=cos⁡t, y∘c=sin⁡t, so c∗x=cos⁡t,c∗y=sin⁡t,c∗dx=−sin⁡t dt,c∗dy=cos⁡t dt.

2.1step 1.1algebra

Therefore c∗η=−(sin⁡t)(−sin⁡t dt)+(cos⁡t)(cos⁡t dt)=(sin⁡2t+cos⁡2t) dt=dt.

3.1step 2.1∎

Thus the angular form pulls back to the standard parameter form on the circle.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

A vector field with no pullback under a noninjective map

Statement refuted

False claim: for every smooth map F:M→N and vector field Y on N, there is a vector field X on M satisfying dFp(Xp)=YF(p) for every p∈M.

Facts & Assumptions

Given: The constant map F:R→R2, F(t)=(0,0), and the constant vector field Y=∂/∂x on R2.

[L1]

A general mixed tensor field does not have a pullback by every smooth map (A general mixed tensor field does not have a pullback by every smooth map).

Counterexample

technique · direct
1.1given

The map F is noninjective and has differential dFt=0 for every t∈R.

2.1givenstep 1.1algebra

A vector field X as in the false claim would satisfy dFt(Xt)=YF(t) at each point. Step 1.1 makes that impossible, because dFt(Xt)=0 for every Xt∈TtR, whereas YF(t)≠0.

3.1L1step 2.1∎

Hence Y has no pullback along F, giving the announced counterexample and agreeing with [L1].

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The volume coordinate expression changes sign under a reflection

Statement refuted

False claim: the coordinate expression of a top-degree form is unchanged by a reflection.

Facts & Assumptions

Given: The reflection R:R2→R2, R(x,y)=(x,−y), and the form ω=dx∧dy.

[L1]

Counterexample

technique · direct
1.1givenalgebra

The reflection satisfies R∗dx=dx and R∗dy=d(−y)=−dy.

2.1L1step 1.1algebra

By [L1], R∗ω=R∗(dx∧dy)=R∗dx∧R∗dy=dx∧(−dy)=−dx∧dy.

3.1step 2.1∎

Therefore the top-degree form changes sign under the reflection, so the claimed invariance is false.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-01Open item page →

The canonical one-form on a cotangent bundle as a covariant tensor

Example

On T∗R2 with coordinates (x,y,ξ1,ξ2), the canonical 1-form is

λ=ξ1 dx+ξ2 dy.

At a point (p,ξ) and a tangent vector v to T∗R2, it satisfies

λ(p,ξ)(v)=ξ(dπ(v)),

where π:T∗R2→R2 is the bundle projection.

Facts & Assumptions

Given: The cotangent bundle projection π:T∗R2→R2 and a point (x,y,ξ1,ξ2).

[F1]

A differential 1-form is a smooth section of the cotangent bundle (A smooth differential k-form).

[F2]

The cotangent bundle fibre at (x,y) consists of covectors on T(x,y)R2 (Cotangent space and cotangent bundle as a disjoint union).

Verification

technique · direct
1.1F2givenalgebra

Write v=a ∂x+b ∂y+c ∂ξ1+d ∂ξ2 at (x,y,ξ1,ξ2). Then dπ(v)=a ∂x+b ∂y, so the covector ξ=ξ1 dx+ξ2 dy gives ξ(dπ(v))=ξ1a+ξ2b.

2.1F1step 1.1algebra

The form λ=ξ1 dx+ξ2 dy takes the same value on v, namely λ(v)=ξ1a+ξ2b. Thus λ(p,ξ)(v)=ξ(dπ(v)). Its coefficients are smooth coordinate functions, so [F1] makes it a smooth 1-form.

3.1step 2.1∎

Therefore the canonical one-form is a concrete covariant tensor on the cotangent bundle.

Sources