Design: induced structures from Layer 0 (Induced/)

[Xinze-Li-Moqian]

Context

Layer 0 (Astrolabe: Nerve + Net) is on main. The next step is to build downstream structures induced from AstroNet, living under ProofAtlas/Induced/.

Known targets

• Hypergraph — the proof hypergraph (formerly "BDF hypergraph"). Adds colour, acyclicity, connectivity constraints on top of AstroNet. This is the core ProofAtlas structure.
• Graph — ordinary graph extracted from AstroNet's reference relations.

Open questions

• Layer 1 (directed net): what is it exactly? Does it need to exist as a standalone structure, or does direction fold into Hypergraph directly?
• Module-level API design for each induced structure
• Which structure to build first

Structure

ProofAtlas/
  Astrolabe/
    Nerve.lean
    Net.lean
  Induced/
    Hypergraph.lean
    Graph.lean
    ...

Each induced module imports from Astrolabe/ but is otherwise independent.

[Xinze-Li-Moqian]

Status update — architecture as built (branch feat/hypergraph)

The design evolved past the original note. Current structure:

ProofAtlas/
  Astrolabe/{Nerve,Net}      -- Layer 0: generic content-addressable hypergraph
  HyperRole.lean             -- shared input/output role
  Induced/
    ProofHypergraph.lean     -- proof hypergraph induced from AstroNet (lossy, content-addressed)
  ExprHypergraph/            -- faithful Lean.Expr hypergraph (NOT induced from AstroNet)
    Basic.lean               -- ExprShape, ExprHypergraph type, encode/decode, faithfulness/equivalence
    Ops.lean                 -- substF / lift / inst / beta + commuting diagrams
    ToProofHypergraph.lean   -- the lossy compression ExprHypergraph → ProofHypergraph

Key realisation: a faithful hypergraph cannot be an AstroNet
(content-addressing needs DecidableEq on ids; faithful ids carry
Level/MData which lack it). So the faithful ExprHypergraph is its
own standalone structure, and the AstroNet lineage (ProofHypergraph)
is the lossy downstream.

The intended tower of increasingly lossy representations:

ExprHypergraph (faithful)  →  ProofHypergraph (lossy, content-addressed)  →  Graph (ordinary, future)

each connected by an explicit compression map, with operations
descending via commuting squares (where compatible).

Done: ExprHypergraph + encode/decode faithfulness (#82), injectivity
(#83), substF/beta as graph ops with commuting diagrams, and the
ExprHypergraph → ProofHypergraph compression.

Resolved open question: "Layer 1 directed net" folded into
ProofHypergraph's input/output roles — no separate layer.

Remaining: direct (non-decode) ExprHypergraph → ProofHypergraph
traversal; the Graph level + compression; operation descent to the
lossy layers; semantics (#84).