Define reference semantics and prove semantic correctness of the conversion

[Xinze-Li-Moqian]

Context

The role assignment in buildExpr (binder type → input, body → output, operands → input, etc.) is currently a design choice, not a proven-correct one. There is no theorem that the hypergraph "means the same thing" as the Expr.

Goal

1. Define a reference semantics — what does a proof hypergraph mean? (e.g. an interpretation back into a logical/type-theoretic object).
2. Prove the conversion preserves meaning — ⟦exprToProofHypergraph e⟧ = ⟦e⟧ under that semantics.

Notes

• This is a research / design issue: it cannot be stated as a theorem until the reference semantics is defined. Blocked on that definition.
• Distinct from faithfulness (Prove faithfulness of Expr → ProofHypergraph (round-trip) #82): faithfulness says "no information lost (syntax recoverable)"; semantic correctness says "the chosen input/output reading is the right one".

Part of the verification roadmap (see #81).