One Function for Every Prime

How random polynomials factor over the p-adic numbers: an algorithmic route to the wild case of the factorization-density conjecture, machine-checked in Lean — unconditionally for quadratics, as a certified architecture for every degree. Written by Claude Fable 5 (an AI system built by Anthropic) with Asvin G, July 2026; updated August 9, 2026, and August 10, 2026. Companion to the expandable map of the Lean development.

The question

Pick a prime $p$ and draw a monic polynomial $f = x^n + c_{n-1}x^{n-1} + \dots + c_0$ with each coefficient a uniformly random $p$-adic integer (each digit of $c_i = a_0 + a_1 p + a_2 p^2 + \cdots$ drawn independently and uniformly; this is Haar measure on $\mathbb{Z}_p$, and the coefficient tuple $(c_0, \dots, c_{n-1})$ is then uniform on the ambient probability space $\mathbb{Z}_p^n$). Over $\mathbb{Q}_p$ the polynomial factors into irreducible pieces, and each piece carries two invariants: its ramification index $e$ and residue degree $f$, with $e \cdot f$ its degree. The multiset

is the splitting type — a multiset: repeated pairs are kept, as in the split type below. (Polynomials with repeated roots form a null set, the zero locus of the discriminant, and are set aside by the counting convention of the statement section: no finite truncation ever decides them.) Each type is a measurable event, so it has a probability $\rho_\sigma(p)$ — its density. For quadratics there are three types: split $\{(1,1),(1,1)\}$, inert $\{(1,2)\}$, ramified $\{(2,1)\}$. How does $\rho_\sigma(p)$ vary with $p$?

When $p > n$ the prime is tame for degree $n$ (it cannot divide any ramification index that occurs), and two classical inputs make the computation uniform in the prime. For the unramified part: where the reduction mod $p$ is squarefree, Hensel's lemma lifts its factorization exactly, and the repeated-factor locus recurses one digit deeper — a geometric series. For the ramified part: every ramified piece is tamely ramified, and tame extensions are completely and explicitly classified — each is generated by a root of a binomial

with finitely many extensions per invariant pair $(e, f)$, counted by expressions in $q$ alone. Together these give each tame density as the value of a fixed rational function of $q = p$ (a uniformity going back to Del Corso and Dvornicich; see §5 of the paper cited next). The quadratic example below displays both inputs at once: the geometric series down the discriminant's valuation is the recursion, and “ramified $\iff v(d)$ odd” is the tame classification of $\mathbb{Q}_p(\sqrt d\,)$. At the finitely many wild primes $p \le n$ these formulas were conjectured to persist by Bhargava, Cremona, Fisher, and Gajović on the strength of low-degree computations. G, Wei, and Yin (arXiv:2212.00294) proved the tame case in general, with a functional equation reflecting Poincaré duality, and proposed a geometric route to the wild case through a Tate-type resolution of the resultant locus; that construction does not hold at wild primes as stated, and the wild case of the conjecture is open. This page presents an independent, algorithmic route toward it — computing the densities rather than comparing them — and reports exactly how much of that route is machine-checked in the Lean proof assistant.

The statement: a density is a limit of counts, caught in a squeeze

The theorem is about one number per prime — one for each prime $p$, degree $n$, and splitting type $\sigma$, of which a fixed degree admits only finitely many ($\sum_i e_i f_i = n$) — and the number is defined by counting, not by measure theory. Truncate the coefficients: mod $p^k$, a monic degree-$n$ polynomial is one of $p^{nk}$ residue classes — each class a cylinder, the set of all $f$ whose coefficients have the given first $k$ digits. Call a class decided to $\sigma$ if every polynomial in it has splitting type $\sigma$ — the $k$ known digits already force the factorization — and undecided if two polynomials in it factor differently, or if it contains a polynomial with repeated roots. That decided classes exist at all is Krasner-style continuity: the splitting type is locally constant away from the repeated-root locus, so around any squarefree $f$ a deep enough truncation forces the verdict. The second undecidedness clause adds nothing new — a repeated root can be resolved by deeper digits in more than one way, fully split among them, so a class containing one already contains two verdicts — it only makes that case explicit. Write $D_\sigma(k)$ for the decided-to-$\sigma$ count and $U(k)$ for the undecided count; a class that is not undecided consists of squarefree polynomials of a single type, so the finitely many types partition the level exactly:

A decided class stays decided at every deeper level: its $p^n$ children inherit the verdict, so $D_\sigma(k+1) \ge p^n D_\sigma(k)$, and the decided fractions $D_\sigma(k)/p^{nk}$ are nondecreasing in $k$ and bounded; their limit defines the density. The partition brackets it at every finite level — the upper bound because a class deciding to $\sigma$ at any deeper level sits inside a class currently decided to $\sigma$ or currently undecided:

This is the squeeze. The limit in $(0)$ exists regardless, by bounded monotonicity; what it still lacks is identity and computability. If the undecided fraction $U(k)/p^{nk}$ tends to $0$ — it does, exponentially fast up to a polynomial factor; this is one of the proof's named obligations (exhaustiveness, final section) — then the two sides of $(0)$ pinch. Any effective envelope $\varepsilon_k \ge U(k)/p^{nk}$ then computes $\rho_\sigma(p)$ to precision $\varepsilon_k$ from the level-$k$ counts alone (effective is a real demand: the definition of $U(k)$ quantifies over every polynomial in a class and is no algorithm — the classifier of the movements below is what supplies the bound). And the limit equals the Haar probability of the type event from the opening section: each class is a cylinder of measure exactly $p^{-nk}$, and the decided classes form an increasing union exhausting the event up to the repeated-root locus, a null set. Everything downstream manipulates the finite counts $D_\sigma(k)$; the measure theory is spent.

Exact status, nothing more claimed anywhere on this page. Vocabulary first, once: the development is the Lean 4 formalization this page reports, presented statement by statement in the companion map linked at the top; machine-checked and certified mean accepted by Lean's proof kernel; the classifier is the development's implementation of the polygon-reading algorithm of the second movement; the capstone is its top-level theorem. For $n \le 2$ the theorem is proved, machine-checked with no hypotheses — one statement universally quantified over the prime, a single parametric proof rather than a list of per-prime evaluations. At $n = 3$ the functions are constructed and match all recorded values, wild primes included. At general $n$ what is machine-checked is an implication: at any prime whose counting data satisfies a two-clause regularity condition, $\rho_\sigma(p) = R_\sigma(p)$ for every $\sigma$, with the density existing and agreeing in three certified readings — keyed to the classifier's verdicts, to the true type, and to $\mathbb{Z}_p$-coefficient classes. (The first two of those are a priori different notions of decided: the $U(k)$ above quantifies over polynomials, while the classifier keeps its own undecided count; their agreement is part of what the condition demands.) The final section states the four open pieces; the table closing this section is the exact ledger, and nothing on this page claims more than it.

The values themselves are classical; what the theorem box reports is that the statement is machine-checked end to end, at every prime, along the route below. The point is the phrase every prime. At odd $p$ these formulas fall out of a short discriminant computation. At $p = 2$ that computation is wrong in two separate ways — and the corrected count lands on the same functions anyway. The whole subject is in this example, so here it is in full.

Note what the example needed at $p=2$: digits of the discriminant three levels deep (the mod-$8$ square law), where odd $p$ needed one. That is wild ramification in miniature — decisions depend on digits at depths the tame theory never inspects — and it is the difficulty the general proof must manage at every degree.

The proof in four movements

The proof computes both brackets of $(0)$ at every level at once, and its plan fits in four lines. (a) Enumerate mod $p$: the $q^n$ possible reductions decide everything Hensel can decide and leave clusters of repeated roots. (b) The tree: lifting mod $p^2, p^3, \dots$ drives a tree of Newton-polygon reads on the clusters, and the tree's skeleton — which reads exist, what each can see, which read follows which — is the same for every prime; $p$ enters only through the edge weights, each a power of $q^{-1}$ times a count. (c) The recursion: the type $\sigma$ selects the accepting leaves; summing all root-to-leaf weights is a finite linear solve, and each self-loop of the skeleton — a read that reproduces its own situation one level deeper — sums to a geometric series $1/(1 - q^{-E})$. (d) Visible uniformity: counts, powers of $q^{-1}$, geometric series, and solves against them can only ever produce denominators built from $q^c - 1$ — nonzero at every prime power — so the solved function evaluates at every $p$, and the squeeze $(0)$ pins $\rho_\sigma(p)$ to its value. The four movements below are these four lines with their machinery; the two degree-5 walks afterward run the whole pipeline end to end.

Movement 1: enumerate mod p

Level zero reads the reduction $\bar f \in \mathbb{F}_q[x]$ — $q^n$ equally likely possibilities, each a cylinder of mass $q^{-n}$. Split $\bar f$ into its squarefree part and its repeated factors. The squarefree part is decided on the spot: Hensel lifts each simple irreducible factor of degree $d$ to an unramified piece $(1, d)$, and the count of reductions with a given squarefree shape is a polynomial in $q$ (the product formula of the tame expandable above, built from the irreducible counts $N_d(q)$). Each repeated factor $\bar\varphi^{\,m}$ ($m \ge 2$) names a cluster: $m \deg \bar\varphi$ roots agreeing mod $p$, not yet separated, about which level zero says nothing more. For a repeated linear factor $(x - \bar c)^m$ the algorithm recenters, $x \mapsto x + c$: the cluster's coefficient window becomes $m$ coefficients all divisible by $p$, with all deeper digits still uniform and independent — a fresh, smaller copy of the original problem, one digit down. Two lemmas stand behind that sentence, not one: the Hensel measure isomorphism of part (c) of the tame expandable splits $f$ into (cluster factor) $\times$ (co-factor) measure-exactly, and recentering the cluster factor is a triangular, measure-preserving change of coordinates on its coefficients; the development proves them as the node-equals-cylinders identification of the next movement. (For a repeated factor $\bar\varphi^{\,m}$ of degree $d > 1$ the base is never extended: the algorithm refines by a key polynomial — a monic degree-$d$ lift of $\bar\varphi$ — and the subsequent residual reads happen in the residue extension $\mathbb{F}_{q^d} = \mathbb{F}_q[y]/(\bar\varphi)$, whose counts are the linear case's with $q \mapsto q^{d}$.) So level zero outputs: decided mass, polynomial-in-$q$ weights, and a list of clusters that carry all the remaining uncertainty.

Movement 2: the tree — one skeleton for every prime

Each cluster is read one digit deeper by the Newton polygon. Plot, for each coefficient $c_i$ of the recentered factor, the point $(i, v(c_i))$, writing $v = v_p$; take the lower convex hull. The negatives of the hull slopes are the valuations of the roots (slope $-\tfrac23$ in the figure means roots of valuation $\tfrac23$), and each segment carries a residual polynomial over the residue field — defined next — whose factorization refines the information one level. Iterating decides every squarefree polynomial in finitely many levels: this is the Ore–Okutsu–Montes classification.

Here is the residual polynomial, at the first level. Let $S$ be a hull segment of slope $-h/e$ in lowest terms, starting at the vertex $(i_0, v_0)$ and spanning $e\,d$ columns. Its lattice points sit at $(i_0 + je,\ v_0 - jh)$ for $j = 0, \dots, d$, and the residual polynomial reads the coefficients along them:

the reduction returning $0$ exactly at the lattice points whose coefficient lies strictly above $S$, and a nonzero digit at both endpoints (they are hull vertices); the variable $y$ stands for the class of $x^e/p^h$ on the roots the segment governs. Factor $R_S = \prod_i \varphi_i^{m_i}$ over $\mathbb{F}_q$. Each simple factor ($m_i = 1$) certifies an irreducible piece with ramification index $e$ read from the slope's denominator and residue degree $\deg \varphi_i$ — degree $e \deg \varphi_i$ in all (Ore's theorem; simple is its regularity hypothesis, and repeated residual factors are exactly where it withholds judgment). Each repeated factor names a cluster of $e\, m_i \deg \varphi_i$ roots not yet separated, into which the algorithm refines — when $e = 1$ and $\deg \varphi_i = 1$, by the recentering $x \mapsto x + c$ with $\bar c$ the repeated root; in general, by a key polynomial of degree $e \deg \varphi_i$ built from the segment data — after which a finer polygon is read over a larger residue field. So every read out of a cluster has one of three outcomes, and this trichotomy is the entire branching logic of the tree: decide a piece (a slope denominator forces $e$, a simple residual factor forces $f$), split the cluster (an interior vertex, or a residual with two coprime factors, partitions the roots into smaller clusters read independently), or survive (the residual is again a single repeated factor: the cluster persists whole, one level deeper — and when the polygon says all roots are divisible by $p$, the rescale $x \mapsto px$ hands back a fresh copy of a smaller-or-equal problem: a self-loop).

Run on all polynomials at once, the algorithm organizes them into a tree: a node is the data read so far, and the polynomials passing through a node form an explicit finite union of digit cylinders, so the node has an exact measure, a sum of powers of $q^{-1}$. For instance, a monic cubic over $\mathbb{Z}_2$ has the polygon of the figure exactly when $v(c_0) = 2$, $v(c_1) \ge 2$, $v(c_2) \ge 1$, a cylinder of measure

This identification of nodes with cylinders is proved in the development, and it converts the random polynomial into a random descent of the tree: the brackets of $(0)$ are sums of node measures.

Descending means refining, and a refinement must transport the data already read. The transport law: if the residual at the current node factors as $R(y) = (y - \tilde c)^{\mu}\, h(y)$ with $h(\tilde c) \neq 0$ — a root of multiplicity $\mu$ against a co-factor regular there — then after the refinement centered at $\tilde c$, the child's residual is

Unpacked: the child's slots $y^0, \dots, y^{\mu-1}$ vanish, so its polygon rises exactly as deep as the multiplicity forces and no further; the $y^{\mu}$-digit is $h(\tilde c) \neq 0$, pinning the child's vertex; and every coefficient of $h(y + \tilde c)$ is a fixed polynomial in the parent's digits — the transported leading row is fully determined, no fresh randomness entering it (the digit rows beneath keep their still-unread uniform digits) — and since $y \mapsto y + \tilde c$ is invertible on digit data, the child is again an exact union of cylinders with the same count of pinned digits. The tree-equals-cylinders picture persists to every depth. (At deeper levels the development states $(\dagger)$ with an explicit anchor-monomial factor $(y + \tilde c)^a$ multiplying the co-factor and with the level's height normalization threaded through the digit rows — position data none of this page's examples excite: $a = 0$ in every one.)

The wild difficulty: $(\dagger)$ is an identity of leading digits, over the residue field. A descent must also transport the digit rows beneath, and there the size of $p$ enters. The transported row-$k$ digit is a fixed polynomial in the parent digits with two kinds of terms: row-local tame terms, and products of lower digits that overflow upward — carries, exactly as in decimal addition. At a tame prime the two stay in separate rows and clearing a slot is a linear equation with unit coefficient in the center's next digit — a Newton step; “is $u$ a square” closes at the first digit. At a wild prime the Taylor coefficients themselves carry extra powers of $p$ (at $p = 2$, $f'(c) = 2c$), pushing the tame term up into the rows where the carries land — and the sum can cancel identically:

That computation ran where every slope denominator seen so far is $1$, so a digit is a plain element of $\mathbb{F}_q$ and the only carries are vertical, between rows. Past a segment of slope $-h/e$, a digit also acquires a fractional height: it lives at a height in $\tfrac1e \mathbb{Z}$, hence carries a coset $\rho \in \mathbb{Z}/e$, and when transported digits multiply, cosets add — overflowing past $e$ costs one full unit of height and deposits the segment's pinned vertex unit $\bar z$ (the residual root the branch selected). The development runs the whole calculus inside the one ring where this bookkeeping is native,

where $\kappa$ is the residue field at the current level — the extension of $\mathbb{F}_q$ built by the residual factors selected so far, which contains $\bar z$ (for the $x^4+9$ branch above, $\kappa = \mathbb{F}_9 \ni \bar z = i$; at the first level $\kappa = \mathbb{F}_q$). A digit of coset $\rho$ is a $\kappa$-multiple of $u^{\rho}$; the relation $u^e = \bar z$ is the carry rule, the exact analogue of a tens-column deposit. (On either piece of the $x^4 + 18$ example: a root $x$ is the coset-$1$ digit, and $x^2 = 3 \cdot (\text{unit with residue } \bar z)$ is $u \cdot u = \bar z\, u^0$ — squaring the half-height digit overflows to integer height and reads off $\bar z$.) $D$ is bookkeeping, nothing more: it need not be a field — when $p \mid e$, on the wild segments, it is not even reduced — and only its multiplication rule is ever used. Every transport polynomial — the $h(y + \tilde c)$ of $(\dagger)$, the $t + t^2$ of $(\ddagger)$, and their analogues at every level and multiplicity — is computed once, symbolically: an identity in $D[y]$ with integer coefficients, $\bar z$ a formal generator, $\kappa$ an abstract extension of the bounded degree the pattern records, and $q$ a free variable in the weights. The prime enters exactly once, as the characteristic of $\kappa$ when the fixed identity is evaluated — the collapse $t + t^2 \equiv 0$ in $(\ddagger)$ is characteristic-$2$ arithmetic acting on one such identity — so no per-prime case analysis remains beyond that evaluation, and wildness is reduced to which of these identities a branch can reach. What is not proved is faithfulness at every level: the base combinatorial lemmas asserting that the $D$-calculus matches true factorization — multiplicativity of the digit map, the landing laws behind $(\dagger)$ — are the conjecture row of the status table, verified exhaustively on their full stated finite ranges (up to $40{,}378$ configurations per lemma) and cross-checked against an independent factorization routine, open in general. At degree $2$ nothing rests on them — which is why the quadratic theorem carries no hypotheses.

The skeleton is prime-free. The tree itself is infinite — polygons steepen, recenterings stack, digits accumulate without bound — but almost none of that history matters below a node. Everything the subtree and the transition weights out of a node depend on is one bounded packet of the node's data, its pattern — a letter, in the alphabet language the rest of this page uses: which move opened the current window (initial read, increment, or recentering — the landing moves transport by different carry laws); the degree bookkeeping (window width, accumulated residue degree); the geometry of the side being read (stride $e$, length, position); the residual's factorization shape and which factor the branch descends into; and the spans of the sibling sides. Deliberately not in the packet: the sides' heights, the run-lengths of repeated reads, every digit value, every lift — the unbounded quantities. Forgetting them is safe: $x^2 - 2$ and $x^2 - 8$ (sides $(0,1)$–$(2,0)$ and $(0,3)$–$(2,0)$) are the same letter — different node measures, identical futures. And the prime is not a field of the packet at all. What licenses the forgetting is the stability lemma, the load-bearing statement of this movement:

for nodes $v, v'$ of any two trees — the same prime or different primes: there is a bijection of children preserving patterns, and corresponding transitions carry the same weight, one rational expression in $q$ evaluated at each node's own prime. Subtrees are isomorphic as weighted trees, conditional on their roots; the descent is a Markov walk on the finite pattern set, and the transfer matrix of the third movement is well-defined. Note how much $(\star)$ carries: the packet retains no digit values, while the one-step reads plainly consume them — so this is a genuine averaging theorem, the assertion that forgotten digits influence a transition's weight only through how many digit choices realize each child, never through which; the equivalence relation it certifies is literal equality of packets, field by field. One honesty clause: for transitions that route digit overflow through a recentering — the carry-facing cases — $(\star)$ rests on the base carry lemmas above (the conjecture row of the status table). The finiteness statements are proved outright:

the first by encoding each pattern injectively as a bounded vector of bounded slots, the second because outside self-repetition every read strictly increases a rank: an integer progress measure built from the packet (accumulated residue degree, lost window width, side position), bounded in terms of $n$. Run-collapsed counts a consecutive run of one letter once. The second bound is what tames the infinite branches: a branch can repeat one read unboundedly — the quadratic march down $u$'s digits is exactly such a run — but an unbounded run never changes its letter, so it collapses to a single node with a self-loop, its depth becoming a parameter ($1, 2, 3, \dots$ or $\infty$) rather than new tree shapes. Collapsed, every branch spells at most $6n^2$ distinct letters, and the whole catalogue is machine-enumerated:

No entry mentions $p$: the enumeration closure runs from the pattern clauses alone, the same list serving every prime, wild included ($53$ at $n = 3$ is the development's sealed catalogue; the observed longest path $2n$ sits far below the proved bound $6n^2$). The tree the proof sums over is therefore a finite weighted graph: the letters are its states, the self-loops carry the collapsed runs, and $p$ lives only in the edge weights — counts over $\mathbb{F}_q$ times powers of $q^{-1}$, one rational expression per edge.

Movement 3: the recursion — the type selects, linear algebra sums the tree

Now fix the type $\sigma$. Each letter's one-step reads either absorb — the decided pieces so far plus the forced future add up to $\sigma$ (an accepting leaf) or to some other type (a rejecting leaf) — or continue to another letter. Because transitions depend only on patterns $(\star)$, the depth-$N$ vector of type-masses obeys a linear recursion with a fixed transfer matrix over $\mathbb{Q}(q)$, and summing over all depths is a Neumann series:

where $K_{\alpha\beta}(q)$ is the weight of continuing from letter $\alpha$ to letter $\beta$ in one level and, for each type $\sigma$, $(b_\sigma)_\alpha(q)$ is the weight of absorbing from $\alpha$ into $\sigma$. One structure hides inside $b_\sigma$: a read that splits a cluster hands back several independent smaller clusters (independent by the Hensel measure isomorphism), and the branch's verdict is assembled from their joint types — a product of solved values, not a single matrix entry. The solve is therefore inductive on window degree: smaller windows are solved first, and a splitting read's absorption weight multiplies the already-solved subcluster entries (exactly how the degree-5 tame walk below multiplies its $3$-cluster value against the solved degree-2 entry); the states of the linear system at each degree are its undivided windows alone. The solution's entries, read at the root, are the candidate functions $R_\sigma$, and $\sum_\sigma R_\sigma = 1$ holds identically. On a self-loop the resolvent is scalar and the series is literally geometric: a loop of one-circuit weight $q^{-E}$ (each circuit pins $E$ fresh digits) contributes

which is where every $q^c - 1$ in the final denominators is born. Here is the complete expansion at degree $2$ — the smallest instance of the whole pipeline, and exactly the computation the machine-checked quadratic theorem certifies.

The full mechanism at degree $n$ is this computation with the catalogue's states instead of $2$ ($53$ at degree $3$), the transition weights supplied by the polygon-and-carry analysis instead of by inspection, and one $b_\sigma$ per type. Whether these symbolic weights model genuine factorization at every prime is exactly the carry-lemma dependency flagged in the second movement.

Movement 4: the formula, visibly uniform in every prime

Trace what the solved entries can be made of. Every weight in $K$ and $b_\sigma$ was generated by five operations: polynomial counts over $\mathbb{F}_q$ (the $N_d(q)$, residual-shape counts); pinned digits $q^{-b}$; geometric depth closures $\sum_{w \ge 0} A\, q^{-cw} = A\,q^c/(q^c-1)$ with $c \ge 1$ (the heights the pattern forgot, resummed); base change $q \mapsto q^{\delta}$ (clusters over extension residue fields); and finite sums and products. By induction over these five operations, every entry of $K$ and $b_\sigma$ — every stratum mass, every intermediate — lies in the ring of the target theorem, and the same membership for the solved entries is the conclusion:

so the assembled function has no pole at any prime or prime power: this is where uniformity becomes visible, as a closure property of the arithmetic rather than a case analysis over primes. The solve is the one step the five-operation induction does not cover: inverting $I - K$ divides by $\det(I - K)$, and membership of the inverse in $\mathcal{R}$ is a theorem with content, not an observation — where a block's determinant factors into self-loop terms $1 - q^{-E}$ it is visible, and nonvanishing at every prime power comes free; whether the assembled determinant always so factors is exactly what stays open at general degree. In the development the proved part is the master denominator theorem, which establishes the membership for its kernel family at every degree; its falsifier — the development's numerical counterexample-search harness — additionally checked the fully assembled pipeline through degree $5$ (every reduced denominator, at $18{,}120$ prime powers) and found zero vanishing. Where the factorization is not yet proved, clause one of the regularity gate below stands in for it, one prime at a time. Two more facts make the solve legitimate at each evaluation $q = p$, rather than merely formal. First, evaluated at $p$, the entries of $K$ and $b_\sigma$ are conditional masses: the one-step reads out of a letter are disjoint events partitioning the fresh digit block, so every row obeys

making $K(p)$ substochastic; by Perron–Frobenius its spectral radius is at most $1$, and $\det(I - K(p)) \neq 0$ is then a complete certificate that it is strictly below $1$ and the Neumann series converges geometrically. For quadratics the estimate is strict row by row ($\det(I-K) = 1 - q^{-2} \ge \tfrac34$ at every prime); at general degree it is the determinant that aggregates the leaks, and the wild threat has a precise shape: a closed class of letters trading mass only among themselves — a carry-locked loop with no decision reachable — would put an eigenvalue at $1$ and void the solve at that prime. The nonvanishing of $\det(I - K(p))$ is clause one of the regularity gate in the ledger: a finite computation per prime, verified in every constructed instance, conjectural in general. (Every self-loop met so far leaks at every prime: the quadratic loop sheds mass $1 - \tfrac1q$ per circuit even at $q = 2$.)

Second, the solved values must be the counted ones — and here two clocks need reconciling: one transition of the walk can pin several digits, so depth in the graph is not coefficient level. The gate's second clause is exactly this reconciliation. At level $N$ the $p^{nN}$ classes split exactly as in $(0)$, and the clause demands that the decided count equal the Neumann series truncated by digit cost — the series regrouped so each term sits at the coefficient level its pinned digits reach, a bounded regrading since every transition pins at least one digit (the $p = 2$ envelope below shows the lag it absorbs) — one count computed twice, through the recorded pattern solutions and directly from the cylinder measures. Writing the regrouped truncation as $\sum_{d=0}^{N-1} K^d b_\sigma$, it telescopes against the full solve (matrices evaluated at $q = p$, entries read at the root):

The right-hand side is the tail: under the gate's identification, the mass that decides to $\sigma$ only after level $N$. Its entries are masses, hence nonnegative — that alone is the upper bracket of $(0)$ with $R_\sigma(p)$ in place of the limit. And a polynomial deciding after level $N$ is undecided at level $N$, so the tails sum to at most the undecided mass. With $\varepsilon_N$ any envelope for $U(N)/p^{nN}$:

which is the capstone's two-sided bracket:

The asymmetry is the content: the upper bound is free (a partial sum of a nonnegative series never exceeds its value), and the lower bound costs exactly one envelope. If $\varepsilon_N \to 0$, the squeeze $(0)$ closes on $R_\sigma(p)$: the density exists and equals the solved value, by counting alone.

For quadratics the envelope is proved at every prime — closing the unconditional theorem. At general degree the bracket, the convergence, and the three readings are proved as one implication from the per-prime instance data — the two-clause gate together with the envelope — whose construction is the open row of the status table.

The expansion at degree five: two walks through the whole pipeline

Degree two is special — a quadratic is solved by its discriminant. Degree five is not: there are seventeen splitting types ($\sum e_i f_i = 5$), the wild primes are $2, 3, 5$, and no single discriminant-like invariant separates the types. Here the pipeline runs end to end for one representative tame type and one representative wild type, displaying the actual recursive sum each time: the entry branches mod $p$, the cluster strata with their weights, the type's selection among the verdicts, the self-loop series, and the one function at the end. (One sub-solve is quoted rather than expanded — the tame walk's $5$-cluster subtree, flagged where it occurs.) Provenance, per the ledger: these two functions are computed by the development's symbolic engine (the same expansion as below, run for all seventeen types; $\sum_\sigma R_\sigma = 1$ symbolically, and every value cross-checked against an independent PARI $p$-adic factorization oracle at $p \in \{2,3,5,7\}$) — certified theorems only at $n \le 2$; at degree $5$ they are the conjecture's exact predicted values.

What remains: four pieces

These are the open items of the algorithmic route, in the proof's own order. Since the wild case of the conjecture is open in the literature, they are what stands between the current certificates and a proof of it — machine-checked from the outset. The ledger above remains the exact accounting: its Proved rows are machine-checked, its other rows are not — the degree-5 functions stay computations, the carry-facing half of $(\star)$ stays conditional, the thirteen slots stay unformulated — and the four items below are where every conditionality on this page bottoms out.

1. Faithfulness (movement 2's tree is the true tree). The polygon reads, transports $(\dagger)$, and carry-algebra identities are computed symbolically; that every node's read matches the genuine factorization of every polynomial in its cylinders — the base carry lemmas, plus the bijection between the tree's leaves and the actual irreducible factors — is proved at degree $\le 2$ (which is why the quadratic theorem has no hypotheses) and open in general. The base lemmas are verified exhaustively on their full stated finite ranges (up to $40{,}378$ configurations per lemma) and cross-checked against an independent factorization routine.

2. Exhaustiveness (the squeeze closes). The undecided-mass envelope $\varepsilon_N$ of $(0)$ must tend to $0$ at every prime and degree. Proved for $n = 2$; threshold forms proved at general $n$; the unconditional statement is a conjecture, verified computationally beyond the constructed cases.

3. Regularity (the solve is legitimate at each prime). Two clauses per prime: $\det(I - K(q)) \neq 0$ at $q = p$ (no carry-locked closed class — the fourth movement's spectral certificate), and the two independently defined readings of the decided count — through the recorded pattern solutions and directly from the cylinder measures — agree. Both hold in every constructed instance; that they hold always is a conjecture.

4. The functional equation. The $R_\sigma$ are palindromic: for each type there is an integer $w_\sigma$ with $R_\sigma(1/q) = q^{w_\sigma}\, R_\sigma(q)$. For instance $R_{\mathrm{ram}}\!\left(\tfrac1q\right) = \frac{1}{\tfrac1q + 1} = q \cdot \frac{1}{q+1} = q\,R_{\mathrm{ram}}(q)$, so $w_{\mathrm{ram}} = 1$. At tame primes this is proved in the Chebotarev paper as a direct reflection of Poincaré duality in étale cohomology (with earlier tame-prime results of Del Corso and Dvornicich as input, per its §5); at wild primes it is open, like the uniformity itself. Within this development it stands as a recorded, uncertified statement that no certified result consumes; deriving it along the algorithmic route — from the palindromic structure of the transfer matrix $K(q)$ — is open.

Beyond these: the per-prime instance data at each degree, and the eventual content of the thirteen reserved hypothesis slots. Every open item except those thirteen slots exists in the development as a typed statement, so a proof supplied for any of them is checked by the same kernel that checked the rest. The slots deserve one honest gloss: each is today filled by a trivially satisfiable placeholder, so they neither narrow the certified implication nor add content to it — but the finished proof may need substantive conditions in exactly those positions, and until they are written the capstone's statement is presumptively weaker than the final theorem.

Milestone log (dated updates since this paper was written)

2026-08-07 — the weld: the carry model is the classifier's own calculus (six adversarially accepted proof notes; not machine-checked). Since this paper was written, the development has run a second certification track alongside Lean: mathematical prose proof notes accepted under an adversarial-verification bar — a note is accepted only after two consecutive clean hostile passes by verifiers reading in fresh contexts, with sealed, preregistered exact-numerics batteries riding each arc and every failed pass, repair, and erratum dated in the repository. Accepted is a strictly weaker certificate than the Proved rows of the ledger above: nothing in that ledger changes status because of anything in this section. On that track, early August produced an accepted carry calculus for the wild tower — one integer recursion giving, at every depth of the tower, the exact correction by which leading values fail to multiply (the "carry cocycle"), proved on a pinned model class of harness towers — and, on 2026-08-06/07, the weld: six notes, each accepted at that bar, identifying the model class with the genuine Okutsu–Montes objects of the second movement's tree. Four junction notes do the matching piece by piece: the lift junction (which polynomial the model tower stands for; six passes, four repairs; a 566-junction resultant cross-check, 560 outside the sealed roster), the dictionary junction (type data to tower data; eight passes, five repairs; independent generating-function and Galois-descent re-derivations, 385,057 and 5,519 exact checks, zero violations), the tree junction (Newton polygons and gradings transport level-to-level by an explicit affine shear; ten passes, eight repairs; re-derivation legs of 326,206 and 106,562 checks, zero violations), and the carry-algebra junction (anchor multiplication lands in a twisted group algebra; eight passes, six repairs; the isomorphism machine-confirmed exhaustively, 669 of 669). A fifth note discharges the lift-normalization corner — its first hostile pass found the original descent argument false at an explicit counter-instance, and the accepted proof is the rebuilt induction, counter-instance displayed (nine passes, seven repairs; sealed runner 25,409 checks, zero violations). The sixth, THEOREM WELD-M (ten passes, seven repairs; an 18,707-check battery with six planted falsifiers all caught), consolidates the package: one transport whose five faces — substrate, gradings, reads, multiplication, covariance — are the four accepted junctions, proved by citation with each junction's conditionality carried verbatim.

Two results in the package deserve statement here. First, the carry cocycle is proved to be a coboundary up to a single honest top carry, and the normalization achieving this is canonical: the gauge can be constructed from the cocycle alone, and an $H^1 = 0$ computation forces uniqueness — so "the whole correction is a gauge artifact" is now an accepted theorem, not a reading of numerics. Second, the reason a cocycle appears at all is elementary and, we think, pretty. A wild tower grows the value group in stages, $\mathbb{Z} \subset \tfrac{1}{e_0}\mathbb{Z} \subset \cdots \subset \tfrac{1}{E}\mathbb{Z}$, so every exponent splits into digits of a mixed-radix positional notation, and adding exponents produces carries; the carry table of positional notation is precisely the classical factor set presenting the extension $0 \to \mathbb{Z} \to \tfrac{1}{E}\mathbb{Z} \to \mathbb{Z}/E \to 0$ — measured on committed towers, its class is the fundamental class, the generator of $H^2(\mathbb{Z}/E, \mathbb{Z}) \cong \mathbb{Z}/E$ (a scratch-grade measurement, disclosed as such; the identification is not consumed by any proof). The tower's carries price these integer carries by residue-field elements, landing the class in $H^2(\mathbb{Z}/E, k^\times)$ for the finite residue field $k$ — and there a classical computation says $H^2(\mathbb{Z}/E, k^\times) \cong \mathbb{Z}/\gcd(E,\, |k|-1)$, which is prime to $p$ when $E$ is a power of $p$. At a wild tower, then, the class of the wild part of the carry cocycle provably dies. This is the cleanest high-level explanation we have of the method this whole development uses: at wild primes there is nothing at cohomology-class level to compute — all wild information lives at cochain level — so a proof must do explicit cochain bookkeeping with displayed fences (the ledger discipline of the notes) rather than invoke class-level machinery, and the standard uniformity toolkits stop exactly where the class dies.

The honest boundary, restated after the milestone. The weld carries exactly one open lemma (W2-OPEN-2: canonical-lift covariance above twist junctions, accepted as a fenced box, not as a theorem) plus fenced evidence cells named inside the notes; the counting block connecting the welded algebra to the density bookkeeping is in progress — its opening lemma (counts are blind to the entire carry/value layer: the mechanism of uniformity in $q$ as a lemma) is proved at attempt grade with a sealed 68,523-check zero-violation battery, its hostile arc not yet begun. And none of this is machine-checked: the four pieces of the previous section stand exactly as written — exhaustiveness and the wild functional equation remain open, the machine-checked results remain the degree-2 theorem unconditionally and the capstone conditionally, and the uniformity theorem at general degree is still not a Lean theorem. The companion map carries the weld as its own stage, with each note's acceptance record, check counts, and open cells beside it.

2026-08-08/09 — Stage one: the chain composed, the first acceptances, and what the machinery says about root counts. On August 8, 2026, the informal mathematics of the uniformity theorem became composed-complete: the proof chain has a named box at every joint — a reduction (W-12.D) feeds an induction (GENIND.B), whose stage laws (GENHN.A/B) consume a fractional-height test-family theorem (HE6.A) and the two-level slot-and-lift theorem with its terminating ladder (HE7.A) — and the last reconciliation, checking that a verifier-widened configuration is a literal instance of the general theorem, closed with 682 exact PARI jobs and zero mis-decisions. Composed through the chain: one rational function of $q$ per splitting type, at every fixed degree and every prime including the wild ones, summing to 1 identically and equal to the Haar density. The grade is the honest headline: COMPOSITION GRADE means every box is closed, written, and machine-instanced — it does not mean accepted, and this page keeps it strictly below the accepted bar of the previous entry; at composition day the boxes stood at grades from 0/2 upward, queued through the hostile-arc program.

That program recorded its first acceptances — and, more useful to a reader gauging the bar, its first complete challenge-to-discharge cycle. HE7 (the note carrying the chain's slot-and-lift theorem) passed two consecutive clean fresh-context passes; then a decorrelated-model ratification sweep, reading surfaces no earlier pass had audited, returned a CHALLENGE: one critical finding, scoped exactly to the note's level-3 proof displays (first live at degree 16, a region with zero machine coverage at the time). The acceptance was annotated, not revoked; the repair became a dated annex re-basing the offending recursion with an explicit cocycle; the repaired region received the first machine verification at a fired level-3 node anywhere in the program (79 of 79 degree-16 members against PARI, then 48 of 48 at degree 24, plus a triple-oracle leg retiring the shared-oracle blind spot); and the annex stack itself then passed two clean passes — the note is now fully frozen, corrections as dated appends only. GENH4, the quartic-degree discharge, has its body accepted at the same 2/2 bar, with the symmetric honesty: its own ratification sweep returned a challenge, and its annex stack's first pass was not clean; the repair has since landed and the stack stands at one clean pass (mid-arc as of this update; since closed — see the 2026-08-09/10 entry). Acceptance here is a property of a named text at a named date, and challenges after acceptance are part of the record, not exceptions to it.

Two companion notes turned the density machinery on the simplest random variable it governs: the number of $p$-adic roots of a random degree-$n$ polynomial. The expected count is $q/(q+1)$ for every degree $n \ge 2$ in the monic model — degree-independent — and exactly 1 in the projective model (the root count taken on the projective line); the probability generating function obeys a cluster recursion; every fixed moment stabilizes in degree (the $k$-th moment is constant once $n \ge 2k$); and as the degree grows the law converges to an explicit limit with an independent-discs reading. Where rows exist to compare, the suite ties the repository's committed transcription of the Bhargava–Cremona–Fisher–Gajović tables exactly (compared rows through degree 7). Two honesty flags, stated as loudly as the results: the notes are at ATTEMPT GRADE (proofs composed, sealed preregistered batteries green — on the expectation note, 93 exact checks passing and all four planted falsifiers, deliberately false variants the battery must flag, duly caught — no hostile pass yet), and NO NOVELTY IS CLAIMED — the literature search has not been done, and the faithful-citation check against the published paper is still owed, so every comparison is a statement about the repository's committed transcription, not about the paper.

A reader-posed question opened a new statistic: fix a tame extension $K$ of $\mathbb{Q}_p$ and count the roots landing in $K$. The embedding count is elementary — tame fields coordinatize as (ramification, residue degree, twist letter), and containment is a divisibility plus one congruence between letters — and the finding is that this statistic SEES the twist letter, already at the mean: two tame quartic fields of the same shape over $\mathbb{Q}_3$, differing only in letter, have different expected root counts — an exact computation in the note, not a statistical impression — where plain root counts are provably letter-blind. The Cohen–Lenstra-style guess for the mean was refuted by the note's own preregistered falsifier (the sealed battery returned 202 of 207, the five failures being exactly the preregistered falsifier firing: the battery refuting the guess as designed) and replaced by a corrected exact law. For unramified $K$ the letter machinery is provably invisible — unramified extensions are unique per degree, so there is no letter to see and the count is determined, polynomial by polynomial, by the splitting type alone — and there the corrected law's evidence was upgraded on August 9 from numerics to exact rational identities in $q$: moments up to the fourth, for unramified $K$ of degree two and three at every menu-certified degree $n \le 5$, computed by two routes sharing no computation (the committed splitting-type menus versus a divisor-lattice recursion), agree symbolically in all 32 of 32 cells; the mean is re-derived a third way by an independent $p$-adic Kac–Rice-style configuration count; and the original seventeen Monte-Carlo ties were retired to consistency-grade evidence — archimedean numerical coincidences are weak evidence in this game, their errors often of size one over a large power of $q$; exact rational identity is the currency. Attempt grade on both fixed-field notes (the original and its exact-identity companion); no hostile pass yet; no novelty claim (unsearched).

The honest boundary, restated after this milestone. Composition grade is below accepted, and accepted is below machine-checked; this section added nothing to the machine-checked set. The chain's boxes are queued through the hostile-arc program; HE7 (including its annexes) and GENH4's body are the two acceptances so far, GENH4's annex stack is mid-arc (repair landed; one clean pass as of this update) (since closed — see the next entry), and the distribution and fixed-field results stand at attempt grade with sealed batteries green and no hostile pass yet. No novelty is claimed for the distribution or fixed-field results — the literature comparison is unsearched and the faithful-citation check against the published tables is owed; every comparison against the Bhargava–Cremona–Fisher–Gajović tables in this section is against the repository's committed transcription.

2026-08-09/10 — the corpus at the bar: the chain's dependency closure and the tower campaign. On August 9, 2026, the hostile-arc program finished what the first acceptances started: each of the nine notes in the theorem chain's dependency closure — the reduction (W-12.D), the induction (GENIND.B), the general stage laws (GENHN), the fractional-height test family (HE6), the slot-and-lift theorem (HE7), the reconciliation (HE6R1), the degree-3 exhaustion law (HEX3), the composite-stage decision note at the base (HE3), and the quartic discharge (GENH4, now including its annex stack, fully frozen) — passed two consecutive clean fresh-context hostile passes. The arcs are part of the record: three of the nine survived decorrelated-model challenge-and-discharge cycles; GENHN had its own tower lemma refuted, repaired, and re-verified inside its arc; and HE3, the note at the base of the chain, had two critical findings caught on its first pass after its descendants were already frozen — the bar working exactly where a reader should worry it wouldn't. With the closure done, the theorem's $n \le 7$ leg rests entirely on accepted texts; accepted at this bar is not machine-checked, and nothing in this entry is a Lean event.

The chain's induction hands degrees eight and up to a tower analysis, and on August 10, 2026 that campaign closed: each of its seven notes — the tower-stage reconciliation (HETOW, reading the tower's $\sigma$ through the already-accepted slot-and-lift theorem), the composed budgets and window ledger (GENTOW1), the intermediate one-sidedness discharged by a page-verified citation to Fernández–Guàrdia–Montes–Nart (GENTOW2; the citation is in the sources below), the faithfulness geography (GENTOW3, accepted on a zero-finding pass (the program's first such pass)), partial inner sides (GENTOW4), the general-multiplicity graded frame with tower witnesses verified by exact computation to ladder depth six (GENTOW5), and the mixed-side tie (GENTOW6) — was accepted at the same 2/2 bar. The record: 19 hostile passes and 8 repair rounds; one decorrelated-model challenge batch whose five real findings were each repaired, two of the repairs becoming new proved lemmas — one showing the wrap-correction twist is a genuine cocycle rather than a character, so it cannot cancel height by height, yet the assembled residuals telescope it into a single global factor of an already-covered species (verified at three committed frames: 203 checks, 37 dual-route computer-algebra jobs, zero violations); the other a cap lemma proved outright when one corollary was found consuming a window-stability lemma beyond its proved scope — the gap repaired by proving more, not claiming less. Two campaign-wide stories: the seven notes predated a wrap-correction erratum, and on each of the seven first passes the verifier independently caught that seam — the repairs moved residue-letter bookkeeping only, and the termination arithmetic was proved invariant under the correction; and the program measured, for the first time, a cross-frame unit it had been assuming trivial — nontrivial values at each of six primes across four frames, the affected certificate re-scoped to its twisted form, and at a seventh measured prime the re-scoped certificate held exactly. That close puts the theorem's $n \ge 8$ leg on accepted texts; combined with the closure paragraph above, the full uniformity theorem's proof corpus now rests on accepted texts at the 2-clean bar, modulo the four named sub-boxes of the next paragraph — and accepted, again, is not machine-checked.

The honest boundary, restated after this milestone. Accepted at the 2-clean hostile bar is not machine-checked, and nothing in this entry adds to the Lean-certified set: the machine-checked results remain the degree-2 theorem unconditionally and the order-0 capstone conditionally — the latter's stated hypotheses being the tame functional-equation input and, for the full-density tie, exhaustiveness — and the general-degree uniformity theorem is still not a Lean theorem. The corpus residue is enumerated, not waved at: four named sub-boxes (three count refinements — an attainment case, a ledger half, a regime classification — and one battery-grade machine ask), none of them correctness conditions. The distribution and fixed-field notes stand where the previous entry left them: attempt grade, sealed batteries green, no hostile pass yet, no novelty claimed — the faithful-citation check against the published Bhargava–Cremona–Fisher–Gajović tables is still owed, and every comparison remains against the repository's committed transcription.

Sources

• Asvin G, Yifan Wei, John Yin, A Chebotarev density theorem over local fields, arXiv:2212.00294.
• Jordi Guàrdia, Jesús Montes, Enric Nart, Newton polygons of higher order in algebraic number theory, Trans. Amer. Math. Soc. 364 (2012), 361–416; arXiv:0807.2620. The imported “theorem of the index” is Theorem 4.18.
• Julio Fernández, Jordi Guàrdia, Jesús Montes, Enric Nart, Residual ideals of MacLane valuations, arXiv:1305.0775 — cited in the tower campaign for the intermediate one-sidedness discharge (GENTOW2); the cite is page-verified against the fetched PDF, a copy of which is md5-pinned in the repository.
• Øystein Ore, Newtonsche Polygone in der Theorie der algebraischen Körper, Math. Ann. 99 (1928), 84–117. Kôsaku Okutsu, Construction of integral basis I–II, Proc. Japan Acad. Ser. A 58 (1982).
• Jan Denef, The rationality of the Poincaré series associated to the p-adic points on a variety, Invent. Math. 77 (1984), 1–23; Jun-ichi Igusa, An Introduction to the Theory of Local Zeta Functions, AMS/IP (2000).
• Manjul Bhargava, John Cremona, Tom Fisher, Stevan Gajović, arXiv:2101.09590 — cited as the source of the density conjecture and of the root-count reference tables; the development's numeric comparisons are against a transcription committed in the repository, and the faithful-citation check against the published tables is still owed.
• Ilaria Del Corso, Roberto Dvornicich, Uniformity over primes of tamely ramified splittings, Manuscripta Math. 101 (2000), 239–266 — tame-prime uniformity and the duality behind the tame functional equation, consumed here in the form used in §5 of the first reference.

Provenance

Written by Claude Fable 5, an AI system built by Anthropic, which also carried out the Lean formalization, directed by and in collaboration with Asvin G. The companion map presents every major formal statement beside its mathematical translation and certification status; the Lean development is being prepared for public release.