Skip to content

Supernatural numbers

Prime-exponent supernatural arithmetic, finite-quotient profinite orders and indices of closed subgroups, a closed-subgroup tower law, and the torsion-order comparison with profinite rational-circle character groups.

Quoted from the project description in formalization.yaml of FormalFrontier/supernatural-numbers at commit cb444a40, Apache-2.0.

No articles: its formalization.yaml lists no highlights, and none of its 3 headline results links a declaration that the scan finds in the linked file at this commit, so they are quoted below.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/supernatural-numbers, read at commit cb444a40 (2026-11-04).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “self-assessed”.
  • Review notes: “Compilation checks, including warning-fatal builds, are distinct from complete transitive standard-axiom verification, including private and generated declarations. Neither schema validation nor this self-assessment constitutes independent mathematical review, rights assessment or certification of a particular revision or its publication status.”
  • Automation: agent; framework “Codex CLI (Formal Frontier Hive), Lean 4 and mathlib”; tool setup “AI agents using Codex CLI, Lean 4 and mathlib developed the mathematical library, checked clients, metadata, bottom/simplification work and the doc-gen4 Markdown adapter. Beacon assembled the original modules, notices and corrections; Folio contributed headline exposition. Exact model versions and total costs were not recorded here.”
  • Automation notes: “Formal Frontier Agents is the collective formalization credit. Beacon is an AI-agent contributor, not a separately identified human author. Beacon's original modules, other AI-agent client/metadata/bottom and documentation contributions, Folio's headline exposition and the adapter's Root Stability/Anchor Ideal recipe lineage are credited in README.md and docs/README.md. Apache notices, collective credit and genuine third-party attribution are preserved; the collective author credit does not identify a copyright holder. The generated API includes displayed Lean signatures and project docstrings, not external book text.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Cohomology of Number Fields, Jürgen Neukirch, Alexander Schmidt, Kay Wingberg, Corrected second edition, version 2.3 (May 2020), Definitions (1.1.5)--(1.1.6) and the following consequences (book; adapts).

Builds on

Headline results

Quoted from the headline results in README.md of FormalFrontier/supernatural-numbers at commit cb444a40, Apache-2.0.

Arithmetic with arbitrary prime exponents. A supernatural number has an ℕ∞ exponent at every prime, without a finite-support restriction. Multiplication adds exponents and divisibility is pointwise order; the complete-lattice bottom is one. Infinite iProd uses suprema of exponent sums over finite subfamilies of a Type-indexed family, whereas iSup and iInf accept arbitrary Sort indices. The positive-natural ofPNat and explicit all-natural ofNat preserve multiplication and reflect divisibility; ofNat 0 = ⊤ and neither map installs a numeral coercion. iSup_ofNat_dvd_iff characterizes the supernatural least common multiple of a Sort-indexed natural-number family, including empty-family and zero cases. See Basic and NatEmbedding.

The closed-subgroup index tower law. The supernatural profiniteOrder and profiniteIndex use finite quotients of a profinite group. For closed subgroups N ≤ H of the same ambient profinite group, profiniteIndex_tower proves [G : N] = [G : H] * [H : N], taking the relative index in H via closedSubgroupWithin H N hNH. Normality is not required, but closedness and the common profinite ambient group are.

Torsion and character orders. For an additive abelian group A with IsAddTorsion A, characterEquivProfiniteCharacter identifies its rational-circle-valued characters with the additive group underlying its profinite character group; the torsionOrder_eq_profiniteOrder_character theorem equates their supernatural orders. The topology-free wrapper gives A the discrete topology; the lower-level Pontryagin interface requires explicit topological assumptions. These noncomputable constructions make no nontorsion or general Pontryagin-duality claim.

Mathlib supplies prime-factorization, finite/profinite-group and Pontryagin infrastructure; this library supplies the supernatural arithmetic and bridges. The released groupTheory library supplies the canonical rational-circle inclusions and finite-order preimages through GroupTheory.Topology.RationalCircle, following their original formalization in this library. Publicly importing SupernaturalNumbers also exposes these declarations. Use AddCircle.rationalToReal, AddCircle.rationalToCircle, AddCircle.exists_rational_preimage_of_isOfFinAddOrder and Circle.exists_rational_preimage_of_isOfFinOrder in new code. The seven former Supernatural names in Characters remain deprecated aliases from October 7, 2026, retained for at least three months. Group Theory's open-kernel comparison for compact groups is distinct from this library's discrete torsion-group character equivalence. See the API reference and checked finite and infinite examples, as well as rational-circle clients.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.