Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 Euclidean right triangle has minsize proportional to its scale

Example

In (R2,d2) consider the triangle with vertices (0,0),(s,0),(0,s), where s>0. Its perimeter is (2+2)s and its minsize μ(s) satisfies s/2μ(s)s,μ(s)=sμ(1). In particular its minsize is a positive linear function of its scale; no optimal coefficient is asserted.

Facts & Assumptions

Given: Fix s>0 and the three indicated straight sides in the Euclidean metric.

[F1]

Minsize is the infimum of the diameters of triples, with one point on each chosen side. (Real trees, tripod triangles, slimness and minsize).

[F2]

On R2, d2((x,y),(x,y))=(xx)2+(yy)2 is a metric. (Rn as the set of functions nR, and d1, d2, d are metrics on it).

[F3]

The nonnegative square root exists and is unique; in particular (2)2=2 and 2>0. (Square roots exist: a unique a0 with (a)2=a; the positives are {x2:x0}).

Verification

technique · direct
1.1

Parameterize the two axis sides by γ1(u)=(u,0) and γ2(u)=(0,u) for 0us. Their pairwise parameter distances are (uv)2=uv. Parameterize the third side by γ3(u)=(u/2,su/2) for 0us2. Its squared distance between parameters u,v is 2((uv)/2)2=(uv)2, so it too has distance uv. These are isometric segments with exactly the displayed endpoints. Their lengths sum to (2+2)s.

F2F3
2.1

Write an arbitrary side triple as p=(u,0), q=(0,v), r=(t,st) with u,v,t[0,s]. Then d2(p,r)st and d2(q,r)t, since their squared distances include respectively (st)2 and t2 and all other summands are nonnegative. Therefore its diameter is at least max(t,st)s/2. This holds for every triple, so μ(s)s/2.

F1F2F3step 1.1
2.2

Take p=q=(0,0) and r=(s,0), which belong respectively to the two axis sides and the third side. Their three pair distances are 0,s,s, so the diameter is s and μ(s)s. In particular at s=1 the computed bounds are 1/2μ(1)1.

F1F2step 1.1
3.1

Multiplication of both coordinates by s bijects all triples for scale one with all triples for scale s, with inverse division by s. The distance formula gives d2(sx,sy)=sd2(x,y) because s>0. Hence the set of admissible diameters is exactly s times the scale-one set. Multiplication by a positive scalar commutes with its infimum: all scaled values are at least sμ(1), and a value less than μ(1)+ε/s scales to less than sμ(1)+ε. Thus μ(s)=sμ(1), with a positive coefficient by step 2.2.

F1F2F3step 2.2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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