Tracking subspaces and gaining traits

[felixpernegger]

Many of our manually added traits are of the following form: "X contains {S} as a subspace and {S|P}" where P is some hereditary property. (+)
So I started assembling a list of all hereditary properties (see #1674) and a list of all subspaces. This list now has about 2000 pairs (SA, SB) where SB is a subspace of SA (i transitively closed it and it has (all) redundants) and 41k pairs of spaces which are not subspaces (this are almost entirely deduced from hereditary traits marked in #1674). About 5000 pairs of spaces (SA, SB) are still unknown if SA contains SB or not.

Now, using those pairs of subspaces and hereditary properties in the form of (+), one can deduce (as of now) 87 new traits for spaces; after deduction engine, apparently 109 traits, about 4% of all traits still unknown.

I'll continue adding new pairs, which hopefully will give rise to more new traits etc.. For this, I set up a tool (with Claude code), with which one can add pairs of subspaces and non subspaces and it works very nicely (you can also check gained traits etc).

So, if anyone is interested in using that and working on this, please say so. This is really a good way to get traits efficiently. :)

On another note, 87+ traits may be a bit much for one PR, even though each trait is simple (usually its trivial to see if something is a subspace). Preferable to split up?

[felixpernegger]

List of traits found:

  Deduction engine: 220 spaces, 47847 trait values.
  Hereditary propagation found 87 new trait values (109 total with theorem re-deduction):
    P000118 does NOT hold for Altered long ray (S000040)  [via Long ray (S000038)]
    P000117 does NOT hold for Altered long ray (S000040)  [via Long ray (S000038)]
    P000147 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000167 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000093 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000136 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000051 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000168 does NOT hold for Michael's product topology (S000077)  [via Irrational numbers $\mathbb R\setminus\mathbb Q$ (S000028)]
    P000197 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Long ray (S000038)]
    P000180 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Long ray (S000038)]
    P000215 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Long ray (S000038)]
    P000103 does NOT hold for Tychonoff plank (S000078)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000215 does NOT hold for Tychonoff plank (S000078)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000177 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000093 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000117 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000110 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000113 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000102 does NOT hold for Sorgenfrey plane (S000076)  [via Sorgenfrey line (S000043)]
    P000172 does NOT hold for Product of the first-uncountable ordinal with the continuum-power of unit intervals (S000104)  [via Continuum power of $[0,1]$ (S000103)]
    P000174 does NOT hold for Product of the first-uncountable ordinal with the continuum-power of unit intervals (S000104)  [via Continuum power of $[0,1]$ (S000103)]
    P000103 does NOT hold for Product of the first-uncountable ordinal with the continuum-power of unit intervals (S000104)  [via Continuum power of $[0,1]$ (S000103)]
    P000167 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega+\omega+1$ (S000034)]
    P000178 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000118 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000216 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000197 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000177 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000180 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000179 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000182 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000183 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000074 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000117 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000215 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000132 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000131 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000015 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000106 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000067 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000112 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1$ (S000035)]
    P000167 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega+\omega+1$ (S000034)]
    P000136 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega+\omega+1$ (S000034)]
    P000168 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega+\omega+1$ (S000034)]
    P000178 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000118 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000177 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000117 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000132 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000106 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000112 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1$ (S000035)]
    P000191 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000186 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000080 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000187 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000081 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000103 does NOT hold for Countable $\sigma$-product $\sigma(\omega_1+1)^\omega$ (S000181)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000172 holds for Deleted Tychonoff corkscrew (S000089)  [via Tychonoff corkscrew (S000088)]
    P000174 holds for Deleted Tychonoff corkscrew (S000089)  [via Tychonoff corkscrew (S000088)]
    P000186 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000080 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000172 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000187 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000174 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000081 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000103 does NOT hold for Product of long ray and continuum power of a closed interval (S000173)  [via Continuum power of $[0,1]$ (S000103)]
    P000191 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000080 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000093 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000187 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000081 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000103 does NOT hold for Deleted Tychonoff corkscrew (S000089)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000178 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000118 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000177 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000117 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000082 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000110 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000132 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000144 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000113 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000102 does NOT hold for Michael's product topology (S000077)  [via Michael line (S000063)]
    P000215 does NOT hold for Stone-Čech compactification $\beta\omega$ of the integers (S000108)  [via Novak space (S000109)]
    P000103 does NOT hold for Product $\omega_1\times(\omega_1+1)$ (S000218)  [via Ordinal space $\omega_1+1$ (S000036)]
    P000147 does NOT hold for Bing's Example G (S000136)  [via Michael's subspace of Bing's Example G (S000137)]
    P000008 holds for Michael's subspace of Bing's Example G (S000137)  [via Bing's Example G (S000136)]
    P000014 holds for Michael's subspace of Bing's Example G (S000137)  [via Bing's Example G (S000136)]

[prabau]

Definitely split this up. If it's all generated by Claude code, it shouldn't be a problem, right?

To make sure I understand, this is an external tool run independently of pi-base to help generating a PR?

Or will the idea eventually be integrated into pi-base by enhancing the deduction system and tracking the subspace relationship in (top of file) metadata, and then this will be automatic without even having to specify all those derivable traits?

[prabau]

If you do just one PR for one the spaces above having a good number of added traits, as a proof of concept, that would be great to look at first.

I assume Claude code is also used to generate the PR itself?

[mathmaster13]

This is awesome.

I've strongly thought about adding a subspace relation to the deduction system; I think the biggest improvement we can make to deduction is some way to add theorems with two quantified space variables (i.e. metaproperty theorems and relations between spaces).

This issue is a pretty nice argument for such an improvement.

[prabau]

Yeah, it's another thing that should be discussed in the "community meeting" #1664.

[felixpernegger]

@prabau @mathmaster13 short demo of the tool:

Screencast.from.2026-03-14.15-41-37.webm

If you wanna use it or have suggestions, please say

[yhx-12243]

Former discussion : #1071 (in case anyone hasn't seen it before) @felixpernegger

[yhx-12243]

Wow it's indeed a great idea I've waiting for a long time (after all, product, subspace, quotient, sum with finite, countably infinite, arbitrary ...), and it'll be a better database for it 👏
But maybe it is a vast project and maybe need many steps (My thought is that, in the later stage, for example, we may have:

• if A + B => C, A hereditary, B hereditary, and automatically C hereditary,
• We can also mark relationship between spaces. Take product as an example, we can mark S31 = S29^2, and auto deduce some property, e.g., KC, is not product-closed,
• e.g. We can mark T5 as hereditary version of T4 and deduce T663 from T661,

Anyway, this is only a very long-term planning and maybe hard to implement, that's totally OK 😀)

One will update the deduction magnificently, including but not limited to auto meta-properties about spaces, to automate deduce things.

[prabau]

@StevenClontz FYI