Mark redundant traits on Related view

[StevenClontz]

Closes #232

[cloudflare-workers-and-pages]

Deploying topology with    Cloudflare Pages

Latest commit:	fb6aa92
Status:	✅  Deploy successful!
Preview URL:	https://49df78b0.topology.pages.dev
Branch Preview URL:	https://stevenclontz-20260309-redund.topology.pages.dev

View logs

[StevenClontz]

Seems to work without a performance hit: https://8f1aefd6.topology.pages.dev/spaces/S000091

[StevenClontz]

@prabau @mathmaster13

[StevenClontz]

For fun: this also works if you want to know when a particular property is being asserted redundantly across the database: https://8f1aefd6.topology.pages.dev/properties/P000050/spaces

[prabau]

Regarding performance, I am curious at what point the computation of the redundancy of traits is done. Is it precomputed for all asserted traits up front, or when opening a specific space's page or a specific property's page?

[StevenClontz]

It's computed each time a page is opened that uses the function that checks it a trait is redundant. Having this precomputed along with all the deduced traits is obviously better but more difficult.

[prabau]

Precomputing everything up front would NOT be better in my opinion, as it could impact start up time for pi-base.

If there is no noticeable performance impact, your solution is perfect. One could also cache this information per property/space, but that adds unnecessary complexity if it's not needed.

[yhx-12243]

I think we can add a option in Advanced page and let user open it itself.

Normal user does not need this, and contributor only open it when he want to make new things. @StevenClontz

[mathmaster13]

I think we can add a option in Advanced page and let user open it itself.

Normal user does not need this, and contributor only open it when he want to make new things. @StevenClontz

yeah good idea
This is a dev feature, after all. The asterisk might annoy people. Or not.

[StevenClontz]

The meaning of the asterisk is pretty obvious when you click it vs others, and I actually think it's of mathematical interest. But let me try adding some global "advanced" state that doesn't require switching branches and see how it feels

If we go this way, should the redundancy proof also be tucked behind Advanced mode?

[mathmaster13]

The meaning of the asterisk is pretty obvious when you click it vs others, and I actually think it's of mathematical interest. But let me try adding some global "advanced" state that doesn't require switching branches and see how it feels

If we go this way, should the redundancy proof also be tucked behind Advanced mode?

No clue. I like the redundancy proofs as a matter of curiosity, and so I actually now agree with you that they should be not hidden. It is of mathematical interest.

As a side note, I know that there are some times where one space needs to be special-cased as part of proving a more general theorem which then implies the original result for that one space. I'm curious if it's easy (for Prolog) to detect and allow this sort of thing. This is unrelated to the current PR.

[StevenClontz]

Aside: while I'm digging around here, I'm finally implementing something I've wanted for a while: indication of which properties are relevant to the search/redundancy:

[StevenClontz]

I believe this is a strict improvement as-is, and I don't want to add complexity by adding an "advanced" mode global state that isn't already there. Arguably there is general interest in seeing in the related properties list when a property is redundant with others. Let's see how it plays out.

It's not clear to me why e2e tests are failing for some commits but not others. Going ahead and merging anyway for now.