Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

An inner-product space need not be complete

Statement refuted

Every inner-product space is complete for its induced norm.

Facts & Assumptions

[A1]

The p-series m11/m2 converges, and a convergent sequence of reals is Cauchy (For rational p>0, 1/kp converges iff p>1, Every convergent sequence is Cauchy, Limits and Cauchy sequences of reals).

[A2]

On counting measure the integral of f2 is the series of the f(k)2, and almost-everywhere equality is equality everywhere, so the norm of a finitely supported sequence is (kxk2)1/2 (p is the Lp space of counting measure, Counting measure on an arbitrary set).

[A3]

The pairing is linear in the first argument, conjugate-linear in the second and positive definite, and Cauchy–Schwarz gives x,yxy (Real and complex inner-product spaces and their induced length, Cauchy–Schwarz: x,yxy, with equality exactly for dependent pairs).

[A4]

A metric space is complete when every Cauchy sequence converges in it, and a Hilbert space is complete for its induced norm (Complete metric space: every Cauchy sequence converges in the space, Hilbert space).

Counterexample

technique · direct

Given: The space c00 of finitely supported real or complex sequences with the pairing x,y=kxkyk, a finite sum for x,yc00.

1.1

The pairing is an inner product on c00: linearity in the first argument and conjugate symmetry are finite-sum algebra, and x,x=kxk2=0 forces every coordinate xk to vanish; the induced length is the 2 norm of the finitely supported sequence.

A2A3
1.2

Let u(N) be the sequence with uk(N)=1/(k+1) for k<N and uk(N)=0 for kN; each u(N) lies in c00, and for M>N one has u(M)u(N)2=Nk<M1/(k+1)2=N<mM1/m2, a difference of partial sums of the convergent p-series, which tends to 0 as N,M by [A1]; hence (u(N)) is Cauchy in the 2 norm.

A1A2
2.1

Suppose vc00 were a limit of (u(N)) in the induced norm; then for each fixed k, Cauchy–Schwarz applied to vu(N) and the k-th coordinate vector gives vkuk(N)vu(N), so vk=limNuk(N)=1/(k+1) for every k, and v has infinitely many nonzero coordinates, contrary to finite support.

step 1.2A3
3.1

Hence the Cauchy sequence (u(N)) in the inner-product space c00 has no limit there, so c00 is not complete for its induced norm, and the statement that every inner-product space is complete is false.

step 1.1step 2.1A4

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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