add diagram sharing design and tla verification specs

[fabracht]

Summary

• design doc for diagram sharing: named view/edit grants + public/link sharing + transitive cascade, holding across CRUD, child entities, and the live event stream under a mutually-untrusting-tenant model
• corrects stale frontend-ownership.md claims (read is enforced; events are broadcast) verified against code
• TLA+ specs verifying the authorization core; a current-behavior spec proves the event-leak and unprotected-children holes are real

Test plan

• DiagramSharing.tla — 12/12 invariants hold (26,244 states)
• DiagramSharingCurrent.tla — same invariants violated on today's behavior (teeth check)
• CascadeClosure.tla — cascade = exact reference closure, cycle-safe (1,792 states)
• GrantLifecycle.tla — direct=set, cascade=max never downgrades, revoke clears (6/6)