Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 lower bound for the transpose forces a dense image of a ball

Statement

Let K=R or C. Let T:XY be bounded linear between normed spaces, and let C>0 satisfy gCTg for every gY. With open balls, BY(0,1/C)T(BX(0,1)).

Facts & Assumptions

Given: The spaces, maps, scalar field, and hypotheses in the statement above. All duals consist of linear functionals over the ambient field; evaluation has no conjugation.

[F1]

From The transpose of a bounded operator, with its stated hypotheses: Let K=R or C. Let T:XY be bounded and linear between normed spaces. Its transpose, or Banach adjoint, is T:YX,(Tg)(x)=g(Tx). The duals are def-dual-space-of-a-normed-space. Composition is bounded by lem-composition-operator-norm-inequality, so this has the displayed codomain. It is linear in g over K. No complex conjugation is inserted; a Hilbert adjoint uses a separate inner-product identification.

[F2]

From The transpose is bounded with the same norm, with its stated hypotheses: Let K=R or C. For a bounded linear T:XY between normed spaces, T:YX is bounded linear and T=T.

[F3]

From Strong separation of a closed and a compact convex set, with its stated hypotheses: Let C,KX be disjoint nonempty convex sets, where C is closed and K is compact. Then they are strongly separated by a nonzero functional in X.

Proof

1.1

Put D=T(BX(0,1)). It contains zero and is closed, convex and balanced: the image ball has these last two algebraic properties, and continuity of linear combinations preserves them on taking closure. For gY, continuity and phase rotation in the unit ball give supyDReg(y)=supx<1g(Tx)=Tg. The open-ball supremum equals the closed-ball supremum by scaling vectors by real numbers tending to one.

F1F2
2.1

If yD, strong separation of the nonempty closed convex set D and compact singleton {y} gives a nonzero gY, oriented so that Reg(y)>supDReg. Thus gyReg(y)>Tgg/C, hence y>1/C.

F3step 1.1given
3.1

Consequently every point of norm less than 1/C lies in D. Zero was already in D. If T=0, the hypothesis forces Y=0; separation in step 2.1 rules out any point outside D={0}, so the argument remains valid even in that degenerate case.

step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

11 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