add feature to deprecate spaces/properties (theorems?)

[StevenClontz]

No description provided.

[marswill]

As long as we are considering deprecation of theorems, spaces, etc, does it make sense to include redundant traits in this discussion?

Right now, whenever we spot redundant trait files, we delete them. While this is not a huge problem, it's dawned on me that this is a somewhat extreme way to deal with redundant content that could conceivably have a use down the road. Particularly since occasionally there's a nicely stated concise proof of something directly in the trait file. In theory when we delete it it's still in the commit history, but in practice it's probably impractical to dig it up if needed.

For example, consider a scenario where a space $X$ has traits $A,B,C,D,E$, and we observe that $A\wedge B \wedge C\wedge D\implies E$, so we delete $E$ as redundant. Then later we find out that $X$ has property $F$, and as everyone knows, $E\wedge F\implies A\wedge B \wedge C \wedge D$. We would probably rather assert traits $E$ and $F$, vs asserting $A$, $B$, $C$, $D$ and $F$. But this entails re-adding an additional trait that was previously deleted.

If we did want to preserve these redundant traits, it seems like for the moment, even before any kind of programmatic solution is implemented, we ought to be able to simply make a "redundant" folder in any space that has redundant traits, and move traits to that folder, instead of deleting. Would this be doable right now, with the current setup? In other words, if we make a new "redundant" folder in a space's directory, will its contents already be simply ignored? If so, I think it might make some sense to start doing that.