Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

Unisolvent degrees of freedom define a unique reference interpolant

Statement

Let (K^,P^,Σ^) be a reference finite element with N=dim⁡P^, dual shape functions ϕ^i, and bounded extensions of its degrees of freedom to a normed function space X containing P^. Then the operator I^v:=∑i=1Nσ^i(v)ϕ^i is the unique linear map X→P^ satisfying σ^i(I^v)=σ^i(v) for every i, and I^p=p for every p∈P^.

Facts & Assumptions

Given: The reference finite-element convention of Reference finite elements and unisolvent degrees of freedom and an input v∈X on which every degree of freedom is defined.

[F1]

The degree-of-freedom map JΣ^:P^→KN is bijective, and the shape functions satisfy σ^i(ϕ^j)=δij. (Reference finite elements and unisolvent degrees of freedom)

Proof

1.1F1given

If N=0, then P^={0} and the empty sum defines the unique linear map X→P^; all degree-of-freedom identities are vacuous and reproduction holds for the sole element p=0. For N≥1, define I^v=∑i=1Nσ^i(v)ϕ^i. The sum is finite and each coefficient is linear in v, so I^ is a well-defined linear map into P^. Applying the jth degree of freedom gives σ^j(I^v)=∑iσ^i(v)σ^j(ϕ^i)=σ^j(v) by [F1].

2.1F1step 1.1∎

If p∈P^, then both p and I^p have the same degree-of-freedom vector, by step 1.1; injectivity of JΣ^ therefore gives I^p=p. If another J:X→P^ has the same degree-of-freedom values, then JΣ^(Jv−I^v)=0, and injectivity again gives Jv=I^v. This proves uniqueness.

Depends on

Used by

Dependency tree · one level

1 result within one dependency step 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