Draw derived proofs

[jamesdabbs]

Updates the derived trait display to visually present the overall proof

Hovering a node or edge highlights the corresponding property or theorem

Several examples of varying complexity:

• Discrete => T0 – a simple line
• Zero dimensional + scattered => urysohn – a tree
• Discrete => urysohn – a single loop
• Finite + discrete => urysohn – a non-trivial web (but see Reduce derived proofs #82)
• A slightly different example involving more negations

We can iterate and tweak this indefinitely. I have a few TODOs I'd like to at least look at before moving this out of draft as a v1:

• improve layout, handle resizing
• ensure nodes don't escape bounding box
• align graph towards top of panel
• pick an apply a stable color scheme
• add tests to cover the new .ts code

Questions

• Hows the general layout and interactivity? Any suggestions?
• We talked about trying to improve the existing theorems list, through a mix of "collapsing" chains of implications that are straight lines, and sorting them in a more natural order. Looking at this one – I'm struggling to put together a reasonable algorithm for how those theorems should be sorted and grouped. Any suggestions? (Forget for a second that Discrete => T1, and that the proof is overcomplicated Reduce derived proofs #82)

[cloudflare-workers-and-pages]

Deploying with    Cloudflare Pages

Latest commit:	fb2ae8c
Status:	✅  Deploy successful!
Preview URL:	https://8920baa8.topology.pages.dev
Branch Preview URL:	https://graph.topology.pages.dev

View logs

[StevenClontz]

Looking at this one – I'm struggling to put together a reasonable algorithm for how those theorems should be sorted and grouped. Any suggestions?

I think the more important thing is that users can manually manipulate the graph and get the picture they need to grok what's going on, not to mention to take a screenshot of (or export to a vector file?) for inclusion in their paper or MathOverflow post.

[StevenClontz]

Other hot takes:

• I don't think the distinction of blue nodes is very helpful: I'm spending a lot of time carefully hovering over the tiny circle to see the pop-up text.
• Could we add Txyz to each edge in addition to hover support?
• It'd be very helpful if true properties were colored differently than false properties.
• I don't think fixing the consequent in place is helpful.
• See also my comments at Reduce derived proofs #82