Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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 normal sequence of entourages yields a uniformly continuous pseudometric with controlled dyadic balls

Statement

Given a decreasing symmetric sequence (En) with E0=X×X and En+1∘3⊆En, there is a pseudometric p on X such that En⊆{p≤2−n}⊆En−1 for every n≥1. In particular, each set {p<ε} is an entourage, so p is uniformly continuous for the original uniformity in the sense of A gauge of pseudometrics and, on a nonempty set, the uniformity it generates.

Facts & Assumptions

Given: A normal sequence (En) of symmetric entourages on X.

[A1]

The given sequence satisfies E0=X×X, is decreasing, and has En+1∘3⊆En.

[A2]

Every entourage contains the diagonal, and every superset of an entourage is again an entourage because a uniformity is an upward-closed filter (Uniform space in the entourage formulation, Filter on a set).

[L1]

A pseudometric satisfies symmetry, the triangle inequality, and p(x,x)=0 (Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

Every nonempty set of reals bounded below has an infimum, which is a lower bound and is approached from above within every positive epsilon (Every nonempty set bounded below has an infimum, Epsilon characterisation of the infimum, Greatest lower bound (infimum)).

[L3]

Finite sums split under concatenation and are nonnegative when their terms are nonnegative; a nonempty finite sum of positive terms is positive (Finite sums and finite products, by recursion, Laws of finite sums and finite products, claims 3 and 4).

[L4]

The dyadic weights 2−n=(1/2)n are positive, satisfy the rational power laws, strictly decrease with n, and tend to 0 (Laws of rational exponents, claims 1 and 2, Monotonicity of r↦ar and of a↦ar, claim 1, and For ∣r∣<1 the sequence rk is null, and for ∣r∣>1 the sequence ∣r∣k diverges to +∞, claim 1).

[L5]

Strong induction may assume a claim for every smaller natural number (Strong (complete) induction).

Proof

technique · constructive
1.1

For x,y∈X, let W(x,y) be the set of sums ∑i<k2−ni over all finite chains x=x0,…,xk=y with (xi−1,xi)∈Eni. This set is nonempty because the one-edge E0=X×X chain has weight 1. Every dyadic term is positive by [L4], so every such finite sum is nonnegative by [L3]; hence 0 is a lower bound. By [L2], the infimum exists; define p(x,y):=inf⁡W(x,y).

A1L2L3L4construct
1.2

We prove by strong induction on the number k of edges, simultaneously for every n, that a k-edge chain of total weight less than 2−n has En-related endpoints. For k=0 the endpoints coincide and hence are En-related by [A2]. Now let k≥1 and assume the claim for every shorter chain. Its total weight w is positive by [L3] and [L4]. Take the first edge for which the cumulative weight through that edge exceeds w/2. The subchain before it has weight at most w/2, and the subchain after it has weight less than w/2; because w<2−n, both are less than 2−(n+1). They have fewer than k edges, so the induction hypothesis makes both endpoint pairs En+1-related. The middle edge has weight 2−m≤w<2−n; strict decrease of the dyadic weights gives m≥n+1, and decreasingness of (Ej) puts that edge in En+1. Thus the endpoints lie in En+1∘3⊆En. Strong induction proves the claim for every finite chain.

A1A2L3L4L5
2.1

The empty chain has weight 0, while all weights are nonnegative, so p(x,x)=0. Reversing a chain preserves its weight because each En is symmetric, so p(x,y)=p(y,x). For the triangle inequality, suppose instead that p(x,z)>p(x,y)+p(y,z) and put δ=(p(x,z)−p(x,y)−p(y,z))/3>0. By [L2], choose an x-to-y chain of weight a<p(x,y)+δ and a y-to-z chain of weight b<p(y,z)+δ. Their concatenation has weight a+b<p(x,y)+p(y,z)+2δ<p(x,z) by [L3], contradicting that p(x,z) is a lower bound of W(x,z). Thus the triangle inequality holds, and p is a pseudometric by [L1].

step 1.1L1L2L3
2.2

A one-edge En-chain has weight 2−n, so En⊆{p≤2−n}.

step 1.1
2.3

If p(x,y)≤2−n with n≥1, then [L4] gives p(x,y)≤2−n<2−(n−1). Apply the epsilon property in [L2] with ε=2−(n−1)−p(x,y)>0 to obtain a chain of weight less than 2−(n−1). Step 1.2 gives (x,y)∈En−1. Thus {p≤2−n}⊆En−1.

step 1.1step 1.2L2L4
3.1

Given ε>0, choose n with 2−n<ε by [L4]. Then En⊆{p≤2−n}⊆{p<ε}, so the latter set is an entourage by upward closure. By A gauge of pseudometrics and, on a nonempty set, the uniformity it generates, p is uniformly continuous for the original uniformity.

A2step 2.2L4discharge-construct∎

Depends on

Used by

Dependency tree · two levels

72 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