Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Successor-occurrence sets of a serial relation are open and dense

Statement

Work in ZF. Let A≠∅, let R⊆A×A be serial, and give Y=Aω the reciprocal first-difference metric of Discrete sequence spaces are complete in ZF. Then Un={f∈Y:(∃m∈ω) f(n) R f(m)}, for n∈ω, is a sequence of open dense sets. Witness indices m are unrestricted.

Facts & Assumptions

Given: The nonempty A, serial R, and metric space Y in the statement.

[F1]

Seriality means that every a∈A has at least one b∈A with a R b (The serial-relation Dependent Choice principle over ZF).

[F2]

Finite-prefix cylinders in Y are nonempty clopen sets forming a metric basis (Discrete sequence spaces are complete in ZF).

[F5]

A set is dense when its closure, defined by meeting every ball, is the whole space (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[F4]

Proof

1.1F3F4given

Each Un is a set by Separation in Y. The graph {(n,U)∈ω×P(Y):(∀f∈Y)(f∈U↔(∃m∈ω)f(n) R f(m))} is also a set by Separation. For each n there is exactly one such U, so this graph defines an indexed family with domain ω.

2.1F2step 1.1

If f∈Un, fix one witnessing m. Every g in the cylinder [f↾(max⁡(n,m)+1)] has g(n)=f(n) and g(m)=f(m), hence g(n) R g(m) and g∈Un. This is an open neighbourhood of f, so Un is open.

2.2F1F2step 1.1

Fix one a∗∈A, and let s:l→A be any finite prefix; l=0 is allowed. Set L=max⁡(l,n+1). Extend s to t:L→A by assigning a∗ at each new coordinate. Thus t(n) is defined and L>n. Seriality gives one b∈A with t(n) R b. Define g(i)=t(i) for i<L, g(L)=b, and g(i)=a∗ for i>L. Then g∈[s] and g(n) R g(L), so g∈Un. This is one explicit extension for a fixed cylinder and fixed n, not a choice of extensions for a family of cylinders.

3.1F1F2F5step 2.1step 2.2∎

Every nonempty open subset of Y contains a cylinder, and hence meets Un by the preceding construction. Equivalently every ball meets Un, which is exactly density by the metric closure definition. Thus every Un is open dense. For singleton A={a∗} seriality forces a∗ R a∗ and the same construction gives Un=Y. No infinite relation-path was assumed in proving nonemptiness of a cylinder.

Depends on

Used by

Dependency tree · two levels

21 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