ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Endpoint-duplicating functions on $[0, 1]$ become all continuous functions on the endpoint quotient

Example

Let $A : = {f \in C ([0, 1], R) : f (0) = f (1)} .$ Then $A$ is a uniformly closed unital real function algebra. Its indistinguishability relation identifies exactly the two endpoints $0$ and $1$ , and the descent map identifies $A$ isometrically with all continuous real-valued functions on the endpoint quotient $[0, 1] / {0, 1}$ .

Facts & Assumptions

Given: The closed interval $[0, 1]$ , the endpoint-equality algebra $A$ , and its indistinguishability quotient.

[L1]

For a uniformly closed unital real function algebra on a compact Hausdorff space, descent is a unital algebra isomorphism onto the full continuous real function algebra of its indistinguishability quotient, and it is isometric when the space is nonempty (A closed unital real function algebra is $C (Y, R)$ on its indistinguishability quotient).

[L2]

The indistinguishability relation is $x \sim_{A} y$ exactly when $f (x) = f (y)$ for every $f \in A$ (The quotient that identifies points indistinguishable by a real function algebra).

[L3]

For $a \leq b$ , every family of open subsets of $R$ whose union contains $[a, b]$ has a finite subfamily whose union already contains $[a, b]$ (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact).

[L4]

A subset $A$ of a topological space $X$ is a compact subset — that is, the subspace $(A, T_{A})$ is a compact space — if and only if every family of open subsets of $X$ whose union contains $A$ has a finite subfamily whose union contains $A$ , or else $A = \emptyset$ (A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, clause 1).

[L5]

The function $d_{R} (s, t) = ∣ s - t ∣$ is a metric on $R$ , and its metric topology is the usual topology (The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded).

[L6]

Every metric space is Hausdorff: distinct points are separated by disjoint open balls (Distinct points of a metric space have disjoint balls around them).

[L7]

Hausdorffness is hereditary: every subspace of a Hausdorff space is Hausdorff ( $T_{0}$ , $T_{1}$ , and Hausdorffness are hereditary, Hereditary, open-hereditary and closed-hereditary properties of topological spaces).

[L8]

The inclusion of a subspace into its ambient space is continuous (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[L9]

For continuous $f, g : X \to R$ on a topological space, $f + g$ , $f g$ , $∣ f ∣$ , $\max (f, g)$ and $\min (f, g)$ are continuous (Sums, products, absolute values, finite maxima and minima, and quotients of continuous real-valued maps on a topological space are continuous where defined).

[L10]

A map is continuous when the preimage of every open set containing an image point contains an open set around that point (Continuity of a map of topological spaces at a point and globally).

Verification

technique · direct

1.1L3L4L5L6L7

By [L3] and the equivalence in [L4], the subspace $[0, 1]$ of $R$ is a compact topological space. By [L5] and [L6] the line $R$ is Hausdorff, so [L7] makes the subspace $[0, 1]$ Hausdorff.

1.2givenalgebra

Endpoint equality is preserved by pointwise sums, real scalar multiples, and products, and every constant has equal endpoint values, so $A$ is a unital real function algebra.

1.3givenalgebra

If $g$ is uniformly approximable by members of $A$ , then for every $ε > 0$ some $f \in A$ satisfies $∣ g (0) - f (0) ∣ < ε / 2$ and $∣ g (1) - f (1) ∣ < ε / 2$ ; since $f (0) = f (1)$ , this forces $g (0) = g (1)$ . Hence $A$ is uniformly closed.

1.4L8L9L10constructalgebra

For $c \in (0, 1)$ let $ι : [0, 1] \to R$ be the inclusion and put $t_{c} : = \min {c^{- 1} ι, (1 - c)^{- 1} (1 - ι)}$ . A constant map is continuous because the preimage of every open set is $\emptyset$ or all of $[0, 1]$ , which is the condition in [L10]; $ι$ is continuous by [L8]; so [L9] makes the two affine maps and their pointwise minimum continuous. For $0 \leq x \leq c$ one has $x / c \leq 1 \leq (1 - x) / (1 - c)$ , and for $c \leq x \leq 1$ the two inequalities reverse, so $t_{c} (x) = x / c$ on $[0, c]$ and $t_{c} (x) = (1 - x) / (1 - c)$ on $[c, 1]$ . Hence $t_{c} (0) = t_{c} (1) = 0$ , so $t_{c} \in A$ ; also $t_{c} (c) = 1$ , and $t_{c} (x) > 0$ for $0 < x < 1$ , so $t_{c}$ vanishes only at the two endpoints.

2.1step 1.4L2

Every member of $A$ identifies $0$ and $1$ . Conversely, if $x \neq y$ and ${x, y} \neq {0, 1}$ , at least one of the two points is interior; choosing that point as $c$ in step 1.4 gives a tent function taking value $1$ there and a value strictly below $1$ at the other point. Thus [L2] says that the only nonsingleton equivalence class is ${0, 1}$ .

3.1step 1.1step 1.2step 1.3step 2.1L1∎

Steps 1.1, 1.2, and 1.3 meet the hypotheses of [L1], and step 2.1 identifies its quotient; since $[0, 1]$ is nonempty, [L1] gives the isometric conclusion, so descent is an isometric unital algebra isomorphism $A ≅ C ([0, 1] / {0, 1}, R)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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

J. M. Erdman, A Companion to Real Analysis, Theorem 21.2.15 (standard reference, not scraped)

Endpoint-duplicating functions on [0,1][0,1] become all continuous functions on the endpoint quotient