Alphabeta Math
ExampleConstruction: AI-adaptedVerification: 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.

An explicit norming functional for the finite-dimensional maximum norm

Example

Let K∈{R,C} and n≥1. Equip Kn with ∥y∥∞=max⁡1≤k≤n∣yk∣. For x≠0 let j be the least index attaining ∥x∥∞, and put fx(y)=xj‾∣xj∣yj. Conjugation is trivial over R. Then fx(x)=∥x∥∞ and ∥fx∥=1. At x=0 the zero functional attains the unit-dual-ball norm formula. For n=0, use the unique zero norm on the zero vector space, which has no norm-one functional.

For a displayed nonuniqueness instance, at x=(1,1)∈K2 the distinct functionals f1(y)=y1 and f2(y)=y2 both have norm one and value 1=∥x∥∞. This entire finite-coordinate construction works in ZF without assuming HB.

Facts & Assumptions

[F1]

A finite nonempty list of real numbers has a maximum and minimum (Every nonempty finite set of reals has a maximum and a minimum).

[F2]

Every nonempty subset of the natural numbers has a least element (The well-ordering principle).

[F3]

The dual is the bounded scalar-linear functionals, with norm the supremum of absolute values on the closed unit ball (The dual space X^* of a normed space and its dual norm).

[F4]

The norm axioms use absolute homogeneity with the modulus over R by A norm on a real vector space, the induced metric, and the dictionary with the metric axioms and over C by Complex norm and complex normed space.

Verification

Given: K=R or C, n≥1, and the displayed coordinate formulas, with the zero-dimensional case treated separately.

1.1givenF1F4algebra

For n≥1, the finite list ∣y1∣,…,∣yn∣ has a maximum. It is nonnegative and is zero exactly when each coordinate is zero. For any scalar a, max⁡k∣ayk∣=∣a∣max⁡k∣yk∣, including a=0. Also each ∣yk+zk∣≤∣yk∣+∣zk∣≤∥y∥∞+∥z∥∞, and taking the maximum gives the triangle inequality. These verify that ∥⋅∥∞ is a norm over either field.

2.1step 1.1F2F3algebra

For x≠0, the set of maximizing indices in {1,…,n} is nonempty. Its least element j exists by natural-number well-ordering. Then ∣xj∣=∥x∥∞>0, so c=xj‾/∣xj∣ is defined and ∣c∣=1. The formula fx(y)=cyj satisfies fx(ay+bz)=acyj+bczj=afx(y)+bfx(z), and ∣fx(y)∣=∣yj∣≤∥y∥∞. Thus fx is scalar-linear and bounded, with ∥fx∥≤1.

3.1step 2.1F3algebra

Let ej have coordinate one in position j and zero elsewhere, and put y=(xj/∣xj∣)ej. Then ∥y∥∞=1 and fx(y)=xj‾xj/∣xj∣2=1. Thus ∥fx∥≥1, proving ∥fx∥=1. Also fx(x)=xj‾xj/∣xj∣=∣xj∣=∥x∥∞.

4.1step 3.1F3algebra

For any bounded linear f of norm at most one and nonzero x, ∣f(x)∣=∥x∥∞∣f(x/∥x∥∞)∣≤∥x∥∞; step 3.1 attains equality. At x=0, every linear f gives value zero and the zero functional attains the same maximum. For n=0 the vector space has just zero and every linear functional sends it to zero, so the dual has only the zero functional of norm zero; its unit ball is nonempty but it has no norm-one element.

5.1step 2.1step 3.1F3algebra∎

At x=(1,1), ∥x∥∞=1. Each coordinate functional satisfies ∣fk(y)∣=∣yk∣≤∥y∥∞ and fk(ek)=1, so ∥fk∥=1 for k=1,2. Both give fk(x)=1, while f1(1,0)=1 and f2(1,0)=0, so they are distinct. In dimension one the same displayed construction is fx(y)=x‾y/∣x∣, with its norm and value computed in steps 2.1 and 3.1. No extension or infinite selection was used.

Source notes

Brezis Corollary 1.3 and Remark 2, pp.3–4 (finite explicit specialization); Teschl Theorem 4.20 proof, p.116 (norming criterion).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

33 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