CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-02

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.

Even polynomials on $[- 1, 1]$ form a unital algebra but are not dense because they do not separate $- 1$ and $1$

Statement refuted

Refuted: a unital real function algebra on a compact space is dense without the point-separation hypothesis.

Facts & Assumptions

Given: $A$ is the algebra of even polynomials restricted to $[- 1, 1]$ .

[L1]

A unital separating real function algebra has the properties in A unital point-separating real subalgebra of $C (K, R)$ .

Proof

technique · direct

1.1

The constants belong to $A$ , and sums and products of even polynomials are even, so $A$ is a unital algebra.

givenL1algebra

1.2

Every $p \in A$ has $p (- 1) = p (1)$ ; therefore $A$ does not separate these two points.

givenL1algebra

2.1

If $p \in A$ , then $\max {∣ p (- 1) + 1 ∣, ∣ p (1) - 1 ∣} \geq 1$ , so $∥ p - id ∥_{\infty} \geq 1$ .

step 1.2algebra

3.1

Hence the identity function is not in the closure of $A$ , and $A$ is not dense.

step 2.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Stone-Weierstrass Theorem (University of Chicago) (standard reference, not scraped)

Even polynomials on [−1,1][−1,1] form a unital algebra but are not dense because they do not separate −1−1 and 11