Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)
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.

Influence-curve representers form an affine orthogonal-complement class

Statement

Let H be a real Hilbert space, let T⊆H be a closed linear subspace, and let ψ˙:T→Rk be continuous linear with an ambient representer ϕ0∈Hk, meaning ψ˙(s)=⟨ϕ0,s⟩H coordinatewise for all s∈T. Assume Countable Choice. Then all ambient representers are exactly

ϕ0+(T⊥)k.

The unique representer in Tk is ϕcan=ΠTϕ0; when ψ˙ is a statistical path derivative, this is its canonical gradient. Projection is applied coordinatewise.

Facts & Assumptions

Given: The hypotheses above. Here T⊥={h∈H:⟨h,s⟩H=0 for every s∈T}.

[F1]

Hilbert space: a real Hilbert space is a real inner-product space complete in its induced norm.

[F2]

Orthogonal decomposition by a closed subspace: under Countable Choice, a closed subspace M of a real Hilbert space has the decomposition H=M⊕M⊥.

[F3]

Orthogonality and the orthogonal complement: M⊥ consists of the vectors whose inner product with every element of M is zero.

[A1]

The Axiom of Countable Choice (ACω): Countable Choice selects a point from each member of a countable family of nonempty sets; it is the axiom assumed by [F2].

Proof

Given: A real Hilbert space H, a closed linear subspace T, a continuous linear map ψ˙, an ambient representer ϕ0, and Countable Choice.

1.1givenF1F3

If ϕ∈Hk is any other representer, then for every s∈T and coordinate j, ⟨ϕj−ϕ0,j,s⟩H=0, so ϕj−ϕ0,j∈T⊥ by [F3]. Thus every representer lies in ϕ0+(T⊥)k.

1.2givenF1F2F3A1choose

Apply [F2] coordinatewise to write ϕ0=ΠTϕ0+h with ΠTϕ0∈Tk and h∈(T⊥)k. Countable Choice is used only in this projection step through [F2] and [A1].

2.1givenF1F3step 1.1algebra

Conversely, if h∈(T⊥)k, then ⟨ϕ0+h,s⟩H=⟨ϕ0,s⟩H+⟨h,s⟩H=ψ˙(s) for every s∈T, so ϕ0+h is a representer. Hence the full representer set is exactly the stated affine class.

3.1step 1.1step 1.2step 2.1F1F3algebra∎

By step 1.2, ΠTϕ0 is a representer. If two representers lie in Tk, step 1.1 places their difference in (T⊥)k as well; each coordinate then lies in T∩T⊥ and has squared norm zero by positive definiteness in [F1], so the difference is zero. This proves existence and uniqueness of the canonical representer.

Remarks

The theorem is a Hilbert-space statement; its only choice use is Countable Choice for the projection decomposition.

Depends on

Used by

Dependency tree · two levels

16 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