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.
Minimal Walks, Oscillation, and L- and S-Spaces: Examples and Counterexamples
1 · Prerequisites
- Arithmetization, Incompleteness, and Relative Consistency
- Binary Operations, Monoids, Groups and Subgroups
- Boolean Algebras, Stone Duality, and the Prime Ideal Theorem
- Borel and Analytic Sets, Perfect Sets, and Determinacy
- Cardinal Arithmetic, Cofinality and the Alephs
- Club, Stationary Sets, and Pressing Down
- Compactness
- Compactness in Metric Spaces
- Complete Metrizability, Čech-Completeness, and Baire Category
- Completeness, Completion, and Uniform Continuity
- Condensation, GCH, and Diamond in L
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Deduction, Soundness, Completeness, and Compactness
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-Support Iterations and Martin's Axiom
- Forcing Orders, Names, and Generic Extensions
- Formal Set-Theoretic Syntax, Structures, and Satisfaction
- Foundations of the Real Numbers for Analysis
- Hereditary and Productive Behaviour of the Separation Axioms
- Large Cardinals, Measures, and Elementary Embeddings
- Metric Spaces
- Metrization: Urysohn, Nagata–Smirnov, Bing, Smirnov
- Minimal Walks, Oscillation, and L- and S-Spaces
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Preservation, Cohen Forcing, and the Continuum
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Proper Forcing, Countable-Support Iterations, and PFA
- Reflection, Absoluteness, and Elementary Submodels
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Set-Theoretic Trees, Delta Systems, and Diamond
- Subspaces, Products, and Quotients
- Suprema and Infima
- The Arithmetical Hierarchy and Post's Theorem
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Constructible Hierarchy and Inner Models
- The Forcing Theorem and Formal Consistency Transfer
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Urysohn's Lemma and the Tietze Extension Theorem
- Well-Founded Relations, Rank, and the Cumulative Hierarchy
2 · Summary
The first example computes every node and running maximum in a finite fragment of a minimal walk through , then verifies both upper- and lower-trace concatenation at the intermediate point. Repeated running maxima are retained until the final lower-trace set is formed, so no multiplicity or empty-maximum case is hidden.
The second example feeds two prescribed bits into the exact functional form of Moore's colouring theorem. The resulting point lies in one clopen subbasic set and outside another, explicitly producing a nonempty finite Boolean neighbourhood. It does not enlarge the theorem to an arbitrary binary matrix.
The false statement separates the three relevant theories: ZFC constructs an L-space, CH constructs a strong S-space, and PFA rules S-spaces out. Under the stated supercompact consistency assumption, S-space existence is not a ZFC theorem, so neither the provability status nor the constructions arise by a formal interchange of separability and Lindelöfness.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
A finite minimal walk and its lower trace
Example
Use the normalized successor values and put
For , , and , the three relevant minimal walks are
Their upper traces satisfy
The lower-trace running-max lists are respectively , , and . Thus
and the strict separation hypothesis is visibly .
Facts & Assumptions
Given: Extend the displayed fragment to the normalized locally finite -sequence fixed on the companion page.
C-sequences and the upper and lower traces of minimal walks on omega-one chooses at each stage the least member of at or above the target, excludes the final target from the upper trace, and records lower traces by running maxima of .
Concatenation and limit control for minimal-walk traces gives trace concatenation when .
Verification
The displayed is cofinal in , contains , and has finite intersection with every . Together with , it meets every local requirement of [F1] used in this calculation.
Aiming at , the least points at or above the target are in , in , in , and in . Aiming at , the first two choices are and ; aiming at from , the choices are and . This proves the three displayed walks and, after deleting their terminal points, the three asserted upper traces.
For target , the successive intersections along the long walk are , , , and . Their cumulative maxima are . For target , the two intersections are both , giving ; for target from , the intersections are and , giving .
Passing from the running-max lists to their trace sets gives and . Hence [F2] applies and its upper- and lower-trace unions agree exactly with the direct computations. No maximum of an empty set occurs, all three targets are strict lower endpoints, and multiplicities were retained until the final set calculation.
An oscillation pattern controls clopen membership
Example
For , form the disjoint blocks
and let and . Apply Moore's pattern theorem with , , the constant map , and , . It returns and with and
Consequently the single point has the prescribed simultaneous membership pattern
In Moore's topology on , the finite Boolean combination
is therefore a nonempty clopen basic neighborhood of . This realizes two bits on the graph of one function; it does not claim control of an arbitrary relation beyond those two graph entries (which in this case are all its entries), nor of an arbitrary matrix when .
Facts & Assumptions
Given: The colouring and topology fixed on the companion page; ordinal multiplication and addition have their usual meanings.
The Moore colouring realizes finite binary patterns realizes and hence for positive finite and uncountable pairwise-disjoint block families.
Moore's clopen-generated topology defines and makes every finite Boolean combination of the clopen.
Verification
The maps , , and divide into successive three-point blocks: each displayed ordinal is countable, , and different blocks are disjoint. Thus and are uncountable pairwise-disjoint families of two- and one-element subsets, respectively.
Use [F1] with and . For the resulting , its parity conclusion gives and .
Because , both and are strictly below . The defining endpoint clause in [F2] therefore turns the two equalities of step 2.1 into and .
By [F2], is clopen and basic, and step 3.1 puts in it. Hence is nonempty and is a neighborhood of the stated point. Both bits, the shared column, the strict order, and the complement bit are explicit; the invocation uses positive and makes no assertion beyond the functional graph allowed by [F1].
False: L-space and S-space existence are dual ZFC theorems
Statement
ZFC settles L-space and S-space existence in parallel by dual arguments: ZFC proves that an L-space exists and also proves that an S-space exists, with one proof obtained from the other by interchanging separability and Lindelöfness.
Facts & Assumptions
Given: The theories in the cited result are interpreted as separate branches. For the metamathematical nonprovability clause, assume .
L-space and S-space existence is asymmetric proves that ZFC constructs an L-space, ZFC+CH constructs a strong S-space, ZFC+PFA proves that no S-space exists, and under the displayed source-consistency assumption S-space existence is not a theorem of ZFC.
Refutation
The first half of the proposed parallel is correct: [F1] constructs an L-space in ZFC. But [F1] obtains an S-space only in the separate CH branch and obtains the incompatible conclusion that no S-space exists in the PFA branch.
Under the source-consistency assumption in Given, [F1] proves that ZFC does not prove the existence of an S-space. Hence the assertion that both existence statements are ZFC theorems is false relative to that same standard large-cardinal consistency assumption.
Nor do the actual arguments arise by a formal interchange of two words: the L-space branch uses Moore's minimal-walk colouring in ZFC, the positive S-space branch uses CH, and the negative S-space branch uses PFA. These hypotheses and conclusions cannot be conjoined, and empty or singleton spaces supply neither kind of witness. Thus both the claimed parallel ZFC status and the claimed dual proof are refuted, with no converse consistency implication asserted.