Design: what should the proof hypergraph definition look like?

[Xinze-Li-Moqian]

Question

The current Hypergraph definition (on development) uses a bare type parameter V for vertices — vertices have no identity, no structure, no data. This needs to be redesigned from scratch.

Design questions to resolve

1. Vertex identity. What is a vertex's id? Content hash (like Merkle tree / Lean.Expr hash) vs natural number vs something else? Hash means same content = same id across different hypergraphs.

2. Vertex as container. What data does a vertex carry? Kind (Prop, Term, Tactic, ...)? Label? Children? Should vertices have recursive structure (like Lean.Expr is a tree)?

3. Construction. How is a hypergraph built? Recursively from sub-expressions? By explicit enumeration? Should there be a builder pattern?

4. Relationship to Lean.Expr. How does a vertex relate to the Lean expression it came from? Is the hypergraph a quotient/projection of the Expr tree, or a separate structure linked by a mapping?

5. Edge semantics. Is the current Hyperedge (ordered inputs → ordered outputs + colour) the right abstraction, or does it need to change too?

6. Acyclicity and connectivity. Are these still axioms of the structure, or derived properties?

Where to think this through

Write the definition in the white paper first (§2 or a new section), in natural language + mathematical notation. Only translate to Lean after the paper definition is stable.

Acceptance criteria

• White paper has a precise mathematical definition of proof hypergraph
• Design addresses all 6 questions above
• ADR documenting the chosen design
• Then: implement in Lean on development branch