Skip to content

docs(spec): update Basic.lean with two-layer architecture #61

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Xinze-Li-Moqian merged 1 commit into from
May 27, 2026
Merged

docs(spec): update Basic.lean with two-layer architecture #61

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 19 additions & 26 deletions lean/ProofAtlas/Hypergraph/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,38 +7,31 @@ Authors: MathNetwork
/-!
# Proof hypergraph — design specification

This file specifies the proof hypergraph: the combinatorial
structure that ProofAtlas extracts from formal proofs.
Two-layer architecture (see `docs/milestones/phase-1.md`):

## Design intent
## Layer 1: AstroNet (arXiv:2604.10435)

A proof hypergraph is a directed, ordered, coloured, acyclic
hypergraph where:
Generic content-addressable hypergraph. Reusable foundation.

- **Vertices** are explicit objects with identity and kind
(proposition, term, inference step, etc.), not a bare type
parameter.
- **Hyperedges** represent inference steps: ordered inputs
(premises) → ordered outputs (conclusions), labelled with a
colour (inference rule type).
- **Acyclicity** ensures the graph represents a valid derivation.
- **Connectivity** ensures the graph is one connected component.
- **AstroNerve** = (identity, references, record)
- identity: SHA-256 hash of record (not of references)
- references: ordered list of nerve identities
- record: opaque content string
- **AstroNet** = collection of nerves with 5 axioms:
content-addressing, self-reference, injectivity, closure,
no duplicate/self-references for width > 0
- Depth filtration: inductive stratification by nesting

## What needs to be defined
## Layer 2: Proof hypergraph (ProofAtlas-specific)

1. `Vertex` — a structure with id, kind, and optional metadata.
2. `Hyperedge` — ordered inputs/outputs referencing vertices,
with colour label. Inputs/outputs disjoint and injective.
3. `Hypergraph` — a collection of vertices and edges satisfying
acyclicity and connectivity.
4. Incidence predicates, reachability, automorphisms.
Built on AstroNet by adding:

## Current status
- References split into **input** / **output**
- **Colour** label (inference rule type)
- **Acyclicity** (no self-descendant)
- **Connectivity** (one component)

This definition is being redesigned on the `development` branch.
The previous implementation used a bare type parameter `V` for
vertices, which prevented vertices from carrying any structural
information. The new design will make vertices first-class objects.
## Status

See the `development` branch for work in progress.
Definition being designed. See issue #58.
-/
Loading