Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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.

A linear functional annihilating the kernel of a surjection is a unique transpose multiple

Statement

Let A:Rm→Rn be a surjective linear map, with m,n≥1, and let ℓ:Rm→R be linear. If ℓ vanishes on ker⁡A, then there is a unique λ∈Rn such that ℓ(v)=⟨λ,Av⟩for every v∈Rm. Equivalently, the row vector of ℓ is ATλ.

Facts & Assumptions

Given: The surjective linear map A and the linear functional ℓ vanishing on ker⁡A.

Proof

technique · direct
1.1givenL1choose

For each standard basis vector ej, choose wj∈Rm with Awj=ej, and define λj=ℓ(wj). These are finitely many choices.

2.1step 1.1L1L2algebra

For v∈Rm, put w=∑j<n(Av)jwj. Then Aw=Av by [L1] and linearity, so v−w∈ker⁡A and ℓ(v)=ℓ(w)=∑j<n(Av)jλj=⟨λ,Av⟩.

3.1step 2.1L1L2∎

If both λ and μ work, surjectivity gives v with Av=λ−μ; then 0=⟨λ−μ,Av⟩=∥λ−μ∥22, so λ=μ. This proves existence and uniqueness.

Depends on

Used by

Dependency tree · two levels

35 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources