Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29
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.

The comparison constants between ∥⋅∥1, ∥⋅∥2 and ∥⋅∥∞ on R2, and vectors attaining each

Example

On R2 with the norms of The p-norms ∥x∥p for rational p≥1, and ∥x∥∞, the comparison chain of The finite and reverse triangle inequalities for a norm; and for n≥1 every norm N on Rn satisfies N(x)≤C∥x∥1 and is Lipschitz, hence continuous, for d2 clause 3 reads

∥x∥∞  ≤  ∥x∥2  ≤  ∥x∥1  ≤  ι(2) ∥x∥∞,∥x∥1  ≤  ι(2)  ∥x∥2.

Each of these four constants is attained, so none can be improved:

  • e0=(1,0) has ∥e0∥∞=∥e0∥2=∥e0∥1=1, so the first and second inequalities are equalities there;
  • (1,1) has ∥(1,1)∥∞=1, ∥(1,1)∥2=ι(2) and ∥(1,1)∥1=ι(2), so the third and fourth inequalities are equalities there.

The general theorem For n≥1 all norms on Rn are equivalent supplies constants but no attaining vectors; that is what this computation adds.

Unit balls. Writing Bp:={ x∈R2:∥x∥p≤1 } for p∈{1,2,∞}, the chain gives B1⊆B2⊆B∞, and both inclusions are strict: (1,1) lies in B∞ and not in B2, and (3/ι(5))(1,1) lies in B2 and not in B1. The scalar has to be chosen strictly between 1/ι(2) and 1/ι(2): at the endpoint 1/ι(2) the vector (1,1)/ι(2) has ∥⋅∥1=1 and so still lies in B1.

Facts & Assumptions

[L1]

The comparison chain on Rn for n≥1, at n=2: ∥x∥∞≤∥x∥2≤∥x∥1≤ι(2)∥x∥∞ and ∥x∥1≤ι(2)∥x∥2 (The finite and reverse triangle inequalities for a norm; and for n≥1 every norm N on Rn satisfies N(x)≤C∥x∥1 and is Lipschitz, hence continuous, for d2 clause 3, The Cauchy-Schwarz inequality for finite sums).

[L3]

Square roots: c is the unique nonnegative s with s2=c, so 1=1, and squaring is strictly monotone on the nonnegatives (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}, Squaring is monotone on the nonnegatives).

[L4]

Canonical naturals: ι(1)=1, ι(2)=1+1>1, ι(2)>0, and ι is strictly increasing (The canonical natural ι(n)=n⋅1F of a field, Canonical naturals are positive and strictly increasing).

[L5]

Absolute value: ∣1∣=1, ∣0∣=0, ∣t∣≥0 (Absolute value in an ordered field, Basic properties of the absolute value).

Verification

technique · direct
1.1

∥e0∥1=∣1∣+∣0∣=1, ∥e0∥2=12+02=1=1, and ∥e0∥∞=max⁡{1,0}=1.

L3L5
1.2

∥u∥1=∣1∣+∣1∣=ι(2), ∥u∥2=12+12=ι(2), and ∥u∥∞=max⁡{1,1}=1.

L3L4L5
1.3

The inclusions B1⊆B2⊆B∞ follow from the chain: ∥x∥1≤1 gives ∥x∥2≤1, and that gives ∥x∥∞≤1.

L1L2
2.1

At x=e0 the first inequality of [L1] reads 1≤1 and the second reads 1≤1: both are equalities, so neither ∥⋅∥∞≤∥⋅∥2 nor ∥⋅∥2≤∥⋅∥1 can be improved by a constant smaller than 1.

step 1.1L1
2.2

At x=u the third inequality of [L1] reads ι(2)≤ι(2)⋅1 and the fourth reads ι(2)≤ι(2)⋅ι(2)=ι(2): both are equalities, so the constants ι(2) and ι(2) are best possible.

step 1.2L1L3
2.3

The inclusions are strict: u has ∥u∥∞=1 and ∥u∥2=ι(2)>1 since ι(2)>1, so u∈B∞∖B2; and w:=(3/ι(5))u has ∥w∥1=ι(2)⋅3/ι(5)=ι(6)/ι(5)>1 while ∥w∥2=ι(2)⋅3/ι(5) satisfies ∥w∥22=ι(2)⋅ι(9)/ι(25)=ι(18)/ι(25)<1, so w∈B2∖B1.

step 1.2L2L3L4
3.1

Steps 2.1 and 2.2 exhibit an attaining vector for each of the four inequalities, and steps 1.3 and 2.3 give the strict inclusions of the unit balls.

step 2.1step 2.2step 1.3step 2.3∎

Remarks

  • Sharpness is not the same as equivalence. For n≥1 all norms on Rn are equivalent asserts that constants exist and produces some; nothing in it says which are smallest. The computation above supplies attaining vectors, and those are what make the constants of the chain best possible on R2.

  • Both attaining vectors are extreme in the expected way. A vector with a single nonzero coordinate makes all three norms agree; a vector whose two coordinates have equal absolute value spreads the mass as evenly as possible and is where ∥⋅∥1 is largest relative to the other two. On Rn the same two vectors give equality with ι(n) and ι(n) in place of ι(2) and ι(2); only the case n=2 is verified here.

  • The strictness computation in step 2.3 is arithmetic, not geometry. The scalar 3/ι(5) was chosen to lie strictly between 1/ι(2) and 1/ι(2); any scalar in that open interval would serve, and the interval is nonempty exactly because ι(2)<ι(2).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

85 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