Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

The polynomial algebra is dense but not closed on a nondegenerate compact interval

Example

Let a<b be real numbers, and let P[a,b] be the real algebra of restrictions to [a,b] of real polynomials. Then P[a,b] is uniformly dense in C([a,b],R) but is not uniformly closed.

Facts & Assumptions

Given: Reals a<b and the algebra P[a,b] of restricted real polynomials.

[L1]

Every unital point-separating real function algebra on a compact Hausdorff space is uniformly dense in the full real continuous-function space (Real Stone–Weierstrass theorem for compact Hausdorff spaces).

[L2]

For ab, every continuous real function on [a,b] is a uniform limit of polynomials (Polynomials are uniformly dense in C([a,b],R) for every closed interval).

[L3]

A nonzero real polynomial of degree n has at most n distinct real roots (A nonzero real polynomial of degree n has no more than n distinct real roots).

[L4]

For ab, 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).

[L5]

The function dR(s,t)=st is a metric on R, and its metric topology is the usual topology (The absolute value makes R a metric space: d(x,y)=xy is a metric, its open balls are the intervals (xr,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]

A subset A of a topological space X is a compact subset — that is, the subspace (A,TA) 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= (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).

[L10]

For continuous f,g:XR on a topological space, f+g, fg and f 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).

[L11]

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.1

By [L4] and the equivalence in [L7], the subspace [a,b] of R is a compact topological space; by [L5] and [L6] the line R is Hausdorff, so [L8] makes the subspace [a,b] Hausdorff.

L4L5L6L7L8
1.2

Put c:=(a+b)/2, so a<c<b, let ι:[a,b]R be the inclusion, and put h:=ιc, so that h(x)=xc. A constant map is continuous because the preimage of every open set is or all of [a,b], which is the condition in [L11]; ι is continuous by [L9]; so [L10] makes ιc and then h continuous.

L9L10L11givenalgebra
2.1

The restricted polynomials form a unital real function algebra, and the coordinate polynomial xx separates distinct points; hence [L1] makes P[a,b] uniformly dense in C([a,b],R). In particular, [L2] also places the continuous function h from step 1.2 in its uniform closure.

step 1.1step 1.2L1L2algebra
2.2

Suppose a real polynomial p agreed with h on [a,b]. Then q(x):=p(x)(xc) vanishes at every x[c,b]; if q were nonzero, that nondegenerate interval would contain more distinct roots than the finite bound in [L3], so q is the zero polynomial and p(x)=xc identically.

step 1.2L3algebra
3.1

Evaluating the identity from step 2.2 at a gives p(a)=ac<0, whereas h(a)=ac=ca>0, a contradiction. Therefore hP[a,b].

step 1.2step 2.2algebra
4.1

Step 2.1 puts h in the uniform closure and step 3.1 keeps it outside P[a,b], so P[a,b] is not closed; together with the density in step 2.1 this proves the example.

step 2.1step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 111 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources