Step 4 · End-to-end pipeline

TODO. Will cover:

• The geometricProfile : Lean.Environment → IO HypergraphReport entry point.
• Const-sharing as the glue: every .const Name reference (across all declarations) maps to a single shared vertex.
• The four computed quantities — incidence data, conductance, resistance matrix, δ-hyperbolicity — and what each tells you.
• The #atlas.* command suite for invocation at the Lean command prompt (see Command reference).

For a runnable demo today, see the live demo on the front page or ProofAtlas/Demos/Pipeline.lean in the repo.