Hamilton–Perelman Poincaré reconstruction archive

Status

The Poincaré conjecture is a solved classical theorem. This archive reconstructs the Hamilton–Perelman finite-extinction route; it does not reopen the problem or claim a new proof.

The theorem

Every closed, connected, simply connected topological 3-manifold is homeomorphic to S³.

The analytic proof is conducted in the smooth category after the classical dimension-three Top/PL/Diff bridge and begins from an arbitrary smooth Riemannian metric.

Proof route represented by the archive

Ricci flow
  -> control of singularity models and noncollapsing
  -> Ricci flow with controlled surgery
  -> finite extinction for the Poincare profile
  -> finite topology-change history
  -> backward connected-sum reconstruction
  -> fundamental-group elimination of nontrivial factors
  -> S3.

Sources

Primary attribution belongs to Grigory Perelman’s three preprints:

1. The entropy formula for the Ricci flow and its geometric applications.
2. Ricci flow with surgery on three-manifolds.
3. Finite extinction time for the solutions to the Ricci flow on certain three-manifolds.

The archive uses John Morgan and Gang Tian’s Ricci Flow and the Poincaré Conjecture as the governing complete detailed reconstruction. Bruce Kleiner and John Lott’s Notes on Perelman’s Papers supplies the detailed cross-check for Perelman’s first two preprints and the finite-extinction handoff.

Repository contributions

The programme contributes:

• a normalized theorem and dependency ledger;
• an atlas of fifteen recurrent false-proof patterns;
• a versioned analytic theorem-interface ledger;
• an exact finite surgery-history schema;
• two valid and twelve malformed executable histories;
• source-preserving component ancestry and backward reconstruction;
• a Lean-checked finite evaluator conditional on explicit imported event equations;
• final source-concordance, category and non-circularity audits;
• a claim-level trust matrix and retained proof-debt register.

Trust boundary

The repository does not formalize Ricci flow, canonical-neighbourhood analysis, neck detection, surgery existence, noncollapsing or finite extinction. A valid JSON record does not prove that a geometric event occurred. The Lean theorem assumes ImportedEventRelation, which connects a real source-certified event to its finite reconstruction equation.

The Lean layer is expression-level. It does not formalize manifolds, connected sums or van Kampen’s theorem.

Source-concordance boundary

The campaign-critical roles of Perelman I/II/III, Morgan–Tian and Kleiner–Lott have been cross-checked. The archive retains open debt for sentence-by-sentence proof correspondence, exact parameter translation and independent analytic verification.

Perelman’s second preprint explicitly identifies a graph-manifold assertion as deferred and an eventual-smoothness/maximal-horn assertion as unjustified and irrelevant to the remaining conclusions. Neither assertion is used by this archive’s finite-extinction Poincaré route.

Permitted description

A source-normalized and adversarially audited reconstruction of the Hamilton–Perelman finite-extinction proof route, with executable topology-history fixtures and a Lean-checked finite backward evaluator. The analytic Ricci-flow and manifold-level topology theorems remain explicitly imported from the classical literature.

Claims not made

• new or alternative proof of the Poincaré theorem;
• proof of an open Millennium problem;
• independent verification of every Hamilton–Perelman estimate;
• formalization of Perelman’s analytic proof;
• machine-checked proof of the Poincaré theorem;
• event existence from schema validity;
• equivalence of Poincaré, elliptization and geometrization;
• novelty or priority.