Import optimized MetricCodes bounds

[Vilin97]

Summary

• import OpenAI's MetricCodes formalization from openai/ten-proofs@94bc0fe, ported to Lean 4.34
• preserve the four canonical headline theorem signatures:
  • MetricCodes.Johnson.main_binary_theorem
  • MetricCodes.Spherical.HigherHierarchy.main_general
  • MetricCodes.Spherical.HigherHierarchy.strict_hierarchy
  • MetricCodes.Spherical.HigherHierarchy.NumericalMaximum.eventually_kissingNumber_lt_published
• incorporate and explicitly credit Dean Cureton's substantial optimization work from 30c21d7; the project is therefore registered with mix provenance
• stack on Import sharp sphere-packing asymptotics #391 and reuse LeanPool.SpherePacking, avoiding a duplicate ~55k-line SpherePacking development

Optimization and cleanup

• split the original 114,406-line monolith into 14 implementation modules; every file is below 10,000 code lines (largest: 8,864)
• reduce non-comment implementation code from 105,323 to 101,903 lines: 3,420 lines / 3.2% below the canonical source, and 445 code lines below the human-optimized fork
• compute source- and kernel-dependency closures from the headline endpoints, remove 13 declarations dead in both closures, and privatize 583 additional internal declarations
• narrow direct Mathlib imports and remove accidental umbrella namespace conflicts
• remove all 765 source set_option directives and all warning-producing/deprecated constructs
• document the public API (709 declaration doc comments total)
• refactor all oversized proofs below the 200-code-line gate (maximum: 188)

Validation

• lake build LeanPool.MetricCodes — green, warning-free; 3,845 jobs
• representative default-option full rebuild — 249.89 s wall, 4,694,780 KB peak RSS
• lake exe runLinter LeanPool.MetricCodes — passed
• lake exe lint-style LeanPool.MetricCodes — passed
• lake exe lint-style LeanPool — passed
• lake exe mk_all --check — passed
• focused kernel axiom audit — all 4,699 parsed public declarations resolved, 0 findings
• canonical-vs-import normalized signature comparison — all four headline signatures match
• exact-head hosted full Lean CI (run 33920801163) — passed (all 10 shards, aggregate build, linters, style, and quality)
• full repository quality checker — passed (7:38.62 wall, 9,612,292 KB peak RSS)
• source scan — no sorry, admit, unsafe, partial, or set_option
• git diff --check — passed

This is intentionally based on codex/import-openai-sphere-packing-2026-09-04, so the PR diff contains MetricCodes only.

[greptile-apps]

Greptile Summary

The change imports the optimized MetricCodes formalization, registers its headline results and mixed provenance, and updates the repository’s aggregate imports and project metadata.

• Splits MetricCodes across an entry module and fourteen implementation modules.
• Registers four canonical headline theorem signatures.
• Credits the canonical OpenAI source and Dean Cureton’s optimization work.
• The supplied base-to-head range also contains the KasamiCyclicAdditive formalization.

Important Files Changed

Filename	Overview
LeanPool/MetricCodes.lean	Defines the MetricCodes project entrypoint, headline metadata, and mixed-provenance attribution.
LeanPool/MetricCodes/Conclusion.lean	Contains concluding portions of the imported MetricCodes proof development and feeds the project entrypoint.
LeanPool/MetricCodes/Binary.lean	Provides the binary-code portion of the imported formalization, including the Johnson-bound development.
LeanPool/MetricCodes/Hierarchy.lean	Implements hierarchy results underlying registered spherical-code headlines.
LeanPool/projects.yml	Registers project metadata, source revisions, provenance, entry modules, and headline declarations.
LeanPool.lean	Adds aggregate imports that make the new project modules reachable from the repository root.
NOTICE	Updates the generated repository attribution index.
README.md	Updates the displayed repository project count.

_{Reviews (3): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[Vilin97]

Fixed the hosted full-style findings in dc85fcb. The patch changes whitespace only across the eight reported MetricCodes files and removes every ; occurrence (41 lines total, including five occurrences masked from the current first-semicolon check).

Validation on the exact commit:

• lake exe lint-style LeanPool.MetricCodes — passed
• lake exe lint-style LeanPool — passed
• lake build LeanPool.MetricCodes — passed, 3,845 jobs, 6:24 wall, 4,678,312 KB peak RSS
• git diff --check — passed
• independent token-stream audit — non-whitespace content is unchanged in every edited file

A fresh hosted full Lean CI run is being dispatched against this exact head.

[Vilin97]

Fresh exact-head hosted Lean CI is fully green on dc85fcb1: all ten build shards, aggregate assembly/build, Lean lint, full text-style lint, and repository quality checks passed.

Run: https://github.com/Vilin97/lean-pool/actions/runs/33920801163

[Vilin97]

Changes requested by automated review

Reviewed exact head 88abb65ee75eff7ade27fb53363a1959f7b124c5. The MetricCodes content is not safely reviewable as this PR stands: the current separation gate fails because the PR file set also carries NOTICE and README.md, and the branch diff includes the stacked SpherePacking project from #391. The checked-in policy permits a content-only PR here. Rebase/retarget this branch onto current main, remove the unrelated SpherePacking/metadata changes, and rerun CI so the exact-head diff contains only MetricCodes plus its registry/root imports.