make properties direct metadata of spaces

[StevenClontz]

As I work on #130, I'm seeing a bunch of redundancy blocking efficient contributions. The decision for each property having a file was based on the assumption each property needed a proof. But if we're relying more on peer-reviewed external sources, maybe this can be more conveniently contained in the yaml frontmatter of the space (in the PR I'm about to make, I just directly cite MathOverflow for each property, and don't add any extra information).

[prabau]

Could be convenient in some cases. Just one thing though. Many properties of spaces can be deduced from other properties via theorems. We don't want to lose that ability, as it's one of the nice features of pi-base, allowing to eliminate duplication in that way. If space X is listed as having property A, and a theorem has A implying B, we still need B. One asserted trait per file may be what makes this work currently? (And not directly related, but I think there are quite a few traits files that could actually be removed and deduced instead.)

[StevenClontz]

This proposal would replace the files spaces/Sx/properties/Pm.md and spaces/Sx/properites/Pn.md with the following header metadata in spaces/Sx/README.md (which I'd further lobby to rename to spaces/Sx.md):

properties:
    - id: Pm
      value: [true|false]
    - id: Pn
      value: [true|false]

Then all the current reference metadata and supporting content written each property's markdown file would be incorporated into the main spaces/Sx/README.md (or spaces/Sx.md) file. This better mirrors the pattern of properties/Py.md and theorems/Tz.md files, and should make editing much more streamlined. Particularly in the case of #134 where I have a single reference that defends every asserted property.

This should not change the behavior of automatically deduced properties. We still need to provide tooling to find redundant properties.

[prabau]

Are you proposing this only for the cases of properties whose justification is entirely contained in the reference mentioned at this top level that defines the space itself, and we would keep the previous scheme for cases where more explanations are provided or different references are used specifically for different properties?

Also I assume the search capabilities by properties would not be affected?

[StevenClontz]

Ah, let me amend this.

properties:
    -   id: Pm
        value: [true|false]
        refs:
        -    mathse: 123456
    -   id: Pn
        value: [true|false]
        refs:
        -    jstor: 123456

So each assertion should have a reference or two. Then either any further elaboration goes in the main README for the space itself, or we could consider an extra note: "hello world \(x^2+y^2\)" attribute on each property item that contains the content currently stored in the space/property pair markdown file.

[StevenClontz]

N.B. I'm not proposing any difference in the front-end viewer; it would have essentially the same capabilities (search, automatic deduction, etc). But this would make most contributions significantly more streamlined.

[prabau]

I am starting to like this idea. For deploying/testing this, we could:

• do a first pass at a change in the infrastructure to support both old and new scheme
• pick a representative space X with multiple property files with a variety of things like proofs, comments we want to preserve, etc
• introduce a parallel space "TEST X" using the new scheme
• see the result and compare how spaces X and TEST X look like in the front end viewer
• tweak/iterate as necessary until we are satisfied with the result

[prabau]

Can this be closed without action?

[GeoffreySangston]

I think this suggestion is not the direction pi-base has gone in, and can be closed. Is that correct?