Exhaustive tame hypermap archive
OpenKeplerMission.tame_archive_classificationEvery fixed archive row decodes to a good face list. Every tame finite hypermap is represented by one of those rows, allowing reversal of orientation. Representation requires exact node labels, unique directed darts, edge reversal and complete face cycles. This is a coverage theorem, not merely a claim that archived rows are tame. The reported 18,762 matches the AFP 2013-12-11 archive: 9 triangular, 1,105 quadrilateral, 15,991 pentagonal and 1,657 hexagonal cases. The AFP entry records a change of tameness constants and archive on 3 July 2014. The final archive has 19,715 rows: 9 + 1,253 + 16,080 + 2,373; the pinned make_archive.hl explicitly records this July-2014 count. Exact permutation comparison shows all 18,762 older classes retained and 953 added, with no duplicate or mirror-equivalent rows within either archive. The mission uses the final accompanying archive, whose source SHA-256 is 703ea865a124aa69f0ee12d94df7065bbbf5701a3085776e24632d14493474db. These are candidate graphs: the classification is coverage, not a claim that every stored row is tame or geometrically realizable (primary §7.2).
Here G is the fixed decoded archive, Rep is the complete face-list representation relation, and H^op reverses orientation.
Source. Hales et al., A Formal Proof of the Kepler Conjecture (2017), https://doi.org/10.1017/fmp.2017.1, §§7–8 pp.17–21; Blueprint Theorem8.38 WTEMDTA (extended PDF p.312); AFP Flyspeck-Tame Computation/Completeness.thy:completeness; formal_graph/archive/archive_all.ml.
Formalization note. Source-derived interface or explicitly identified analytic corollary; no proof of the target is supplied by defining its proposition.
import Definitions.Def_Kepler_MissionContracts set_option autoImplicit false
namespace KeplerMission theorem tame_archive_classification : TameArchiveClassification := by sorry end KeplerMission
Read-back
What the Lean code literally says, in plain math · gpt-6
This names, without proving, the conjunction that every slot of the fixed 19,715-entry archive decodes to a Good face list and that every finite hypermap satisfying the full tame predicate has some successfully decoded archived face list representing either that hypermap or its opposite. Good means nonempty faces, no repeated directed cyclic edge pair, and presence of the reversed pair. Representation uses node labels, an injective directed-pair map, reversal by the edge permutation, and two-way coverage of face cycles up to rotation. The tame hypothesis includes the permutation coherence, involution and incidence conditions, numerical Euler condition, connectedness, face sizes 3 through 6, node count 13 through 15, degree restrictions, and the specified admissible real weights of total strictly less than 1.541. The quantified hypermaps need not first be geometrically realized. This proposition does not assert that every archived entry is tame or realizable, nor uniqueness of an archive representative.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.