Naming note: this chapter is Ch Gal, not “Ch Γ”. Γ is already the series’ limit cycle — the closed orbit at r = 1 in the contact normal form, used across Vol I, the PolyLaminin chapter and the recurrence-ladder page. A second meaning would be a name collision of exactly the kind the repo ledger records elsewhere. The mnemonic-letter convention (Ch A · Autophagy, Ch W · Wigner, Ch T · Tubulin) is followed instead.
§ 1 · The Ladder Is One Polynomial
Seven chapters on this ladder name seven constants. φ = 1.618 is the root of
x² = x + 1. η ≈ 1.8393 is the root of x³ = x² + x + 1. Δ ≈ 1.9276
answers the four-term recurrence, Σ ≈ 1.9659 the five-term, and the sequence climbs toward
τ = 2 without ever arriving.
Those are not seven separate facts. They are one polynomial evaluated at seven values of a parameter:
The dominant real root of p_n is the n-bonacci constant. That the roots increase
with n and converge to 2 is the ladder's shape; it is why τ = 2 is a limit and not a rung.
Multiplying by (X − 1) telescopes the sum and gives a trinomial,
X^(n+1) − 2X^n + 1, which is what lets the trinomial literature speak to the
ladder at all — with a caveat that turns out to be load-bearing, and is the subject of § 3.
§ 2 · From a Constant to a Symmetry
A number is a weak object. The interesting question is not what is η but what
else is η — which other numbers are indistinguishable from it by any polynomial identity
with rational coefficients. That set is η's conjugates, and the group permuting them is the
Galois group of p_n.
The group is the ladder's real invariant. Two rungs with the same group are structurally the
same rung wearing a different number. When the group is the full symmetric group
S_n — every permutation of the roots is legitimate — the rung has no hidden
structure: no subfield, no partial symmetry, nothing that survives to constrain the recurrence.
When the group is smaller, something does.
For the ladder the expected answer is S_n, and the machinery to prove it is
standard in outline: irreducibility gives transitivity, complex conjugation supplies a
transposition, and a transitive group with a transposition is S_n — provided it
is also primitive. That proviso is where the chapter stops being a summary and starts being
an open problem.
§ 3 · The Obstruction, Named
For prime degree the proviso is free: a transitive subgroup of S_p
containing a transposition is all of S_p, and surjectivity closes immediately.
Odd composite n defeats that route. The chain becomes irreducible ⇒ transitive, then
transitive + primitive + a transposition ⇒ S_n by Jordan. Primitivity is
the load-bearing step, and it is not free.
| Result | Status | Evidence |
|---|---|---|
nBonacci_action_injective | VERIFIED | Mathlib galActionHom_injective, applied directly. No sorry. |
nBonacci_action_bijective | OPEN | sorry. Surjectivity. |
Theorem_Galois | OPEN | Compiles, derives from the line above, inherits its sorry. |
Irreducibility of p_n | ASSUMED | Carried as hypothesis hirr, not discharged. |
The primitivity results for trinomials are Movahhedi–Salinier (1996) and
Cohen–Movahhedi–Salinier (1997, 1999), and they are not in Mathlib. Formalizing them is
a prerequisite; no tactic search closes this sorry without them.
A second gap sits in front of that one. Those theorems concern irreducible
trinomials, and their permutation action is on the full root set of the trinomial. Here
X^(n+1) − 2X^n + 1 factors as (X − 1) · p_n(X), so it is reducible
by construction: the action on its n+1 roots fixes 1 and is not transitive. The hypotheses do
not apply as stated, and the transfer from the trinomial back to p_n is a
reduction argument that has not been written. Citing the literature does not discharge it.
No theorem number from any of those papers is cited on this page. The PDFs have not been read against this repository, and a numbered result quoted from working knowledge is a claim rather than a citation. This is not fastidiousness: a replacement reference proposed for this very paragraph — complete with title, journal, volume, pages and DOI — turned out on checking to describe no such article. Only the authors and the year were right.
§ 4 · Building Fields to Order
The ladder poses the group question in one direction: here is a polynomial, what is its group?
The inverse Galois problem poses it in the other: here is a group, produce a polynomial.
In 2026 the SAIR foundation ran that problem as an open competition at degree 24 — 25,000
transitive groups 24T1–24T25000, each with several possible
signatures, most of the map blank. This chapter's computational half is what that produced.
Composita — building imprimitively on purpose
Since 24 = 2·12 = 3·8 = 4·6 = 2·2·6 = 2·3·4, a field can be assembled from smaller ones. The
compositum of two linearly disjoint subfields contains both, so its group is
imprimitive by construction — the opposite of the ladder's expected S_n,
and precisely the region a random search never reaches, because random polynomials land in
S24 or A24. The minimal polynomial of a sum of generators comes from
Newton power sums, exactly:
Towers — reaching what composita cannot
A tower is not a compositum, and the difference is not cosmetic. Let K12 be
totally real of degree 12 and let α ∈ K12 be negative at exactly j of its
twelve real places. In K24 = K12(√α) the 12−j positive places each split into two
real places and the j negative ones each contribute a complex conjugate pair:
Choosing α is exact rather than a search. If θ generates K12 with real conjugates
θ₁ < ⋯ < θ₁₂, then mθ − k is negative precisely where θᵢ < k/m, so placing
k/m in the gap (θⱼ, θⱼ₊₁) gives exactly j negative places. The minimal polynomial is
g_α(x²) where g_α = m¹²·g((x+k)/m) — integer arithmetic, no
resultants, no power sums. And irreducibility is free: K12 totally real means
every square in it is non-negative at every real place, α is negative somewhere, so α is not a
square, so [K12(√α):K12] = 2 and g_α(x²) is irreducible. No
factorization is performed or needed.
§ 5 · The Signature Ladder, and a Parity Law
The tower is a one-parameter machine for the signature axis: fix K12, slide k/m up
the conjugate ladder, and j = 0…12 delivers r = 24, 22, 20, …, 0 from a single field. Three of
those signatures are unreachable by any compositum.
Across a generic compositum the signature multiplies: r = ∏ rᵢ with rᵢ ≤ dᵢ and rᵢ ≡ dᵢ (mod 2). Enumerating the shapes 2·12, 3·8, 4·6, 2·2·6, 2·3·4, 2·2·2·3 over all parity-admissible constituent signatures gives reachable r ∈ {0, 2, 4, 6, 8, 12, 16, 18, 20, 24}. The complement is exactly r ∈ {10, 14, 22}: 22 would need 2·11 or 1·22, and 11 and 22 each overshoot or mis-parity every available dᵢ; likewise 10 and 14.
Stated for the generic primitive element. This is unreachability by the generic compositum, not a theorem about every degree-24 field possessing a proper subfield.
The second axis is subtler, and it is not free. Write N(α) = ∏σ(α) over the twelve
real embeddings. Since √N(α) = ∏√σ(α) always lies in the Galois closure, whether
N(α) is a rational square decides whether that element is rational — confining the
twist module to the index-2 kernel of the sum map — or generates a quadratic subfield not
inherited from K12, letting the module reach the full 2¹². Two
different groups at the same signature.
Exactly j of the factors of N(α) are negative, so
sign N(α) = (−1)ʲ. For odd j this is negative, and a negative rational is never a
square. Hence at r ≡ 2 (mod 4) — that is r = 22, 18, 14, 10, 6, 2 — only the
non-confined module class occurs, for every α, and the group axis is not a free
parameter. At r ≡ 0 (mod 4) both classes are available.
Verified on 2,443 (K12, m, k) triples: 2,443 confirm, 0 violate. The argument
uses only α's sign pattern, so it holds for every α in K12, not only the linear
family used here.
There is a free corollary. The constant term of the submitted degree-24 polynomial is exactly
a₀ = g_α(0) = N(α), because g_α is monic of even degree. So a single
integer square-root test on the first coefficient reads the module class off the page — no
factorization, no prime sampling, no threshold.
An earlier draft of this section asserted that unit twists (|a₀| = 1, which give the smallest discriminants) are necessarily in the confined class, so that small discriminant and full module were mutually exclusive. Wrong. A unit has N(α) = ±1, not necessarily +1. Combined with the parity law: at odd j, N(α) = −1 for every α including units, and −1 is not a square — so at r ≡ 2 (mod 4) a unit is small-discriminant and non-confined at once.
The correct and narrower statement: at even j a unit forces N(α) = +1 and the coupling
is real; at odd j there is nothing to give up. The actionable form is the opposite of the
original advice — at r = 22, 18, 14, 10, search the required interval for
m¹²·g(k/m) = ±1 and take the small discriminant for free, since parity has
already fixed the module class.
§ 6 · Reading the Group Without a Licence
Identifying a degree-24 Galois group normally requires Magma. The cheap substitute is Chebotarev: the degrees of the irreducible factors of f mod p are the cycle type of a Frobenius element, so climbing primes samples the group's cycle types. Two fields with different cycle types must have different groups.
The temptation is to run that backwards, and it is a trap. This is where the project's largest quantitative error lived.
An earlier version of this work reported 195 distinct cycle-type spectra across 587 fields and concluded, since different spectra force different groups, that 195 was a lower bound on distinct groups. The competition's Magma verifier returned 31 distinct labels from those same polynomials. The estimate overcounted by 6.3×.
The premise is true of limiting spectra and false of sampled ones. A
spectrum read at 25 primes is a small multinomial sample; two fields with the same group
routinely show different observed spectra, so counting observed spectra counts sampling noise
as structure. For two samples of size n from one distribution,
E[L1] ≈ 1.1284 · S / √n with S = Σ√(pᵢ(1−pᵢ)), so any fixed cutoff
splits high-entropy groups apart while merging low-entropy ones.
Replacing the fixed cut with a threshold scaling as S/√n, sampling at 1000
primes, and calibrating the constant against the returned labels recovers 38 of the 39
true pairs with every cluster pure. That the qualitative caveat is classical — Dedekind
gives containment only — is exactly why the number, not the caveat, is the thing worth
reporting.
§ 7 · What the Oracle Returned
Seven submissions, 1,468 polynomials, all accepted by the official Magma pipeline. Every figure below is the verifier's output, not this project's interpretation of it.
| Submitted | Lines | Labels | Pairs | Construction |
|---|---|---|---|---|
| 15 Aug | 588 | 31 | 39 | composita, r ∈ {0,2,4,8} |
| 16 Aug | 450 | 121 | 213 | composita, signature sweep |
| 16 Aug | 86 | 10 | 10 | r = 20 composita |
| 16 Aug | 43 | 7 | 7 | r = 20 tower |
| 16 Aug | 57 | 16 | 16 | r = 16 tower |
| 16 Aug | 6 | 3 | 3 | opposite square class |
| 16 Aug | 238 | 5 | 20 | towers, r = 22/18/14/10 |
| union | 1468 | 159 | 304 | — |
The last row of the table is the parity law made visible. The 238-line tower submission returned exactly the 20 pairs predicted — but from only five distinct labels, the identical set at every one of r = 22, 18, 14, 10. All four are odd j, so all four were forced into the same module class. Sliding k/m moves the signature and leaves the group where it was.
Of the 588 rows in the first submission, 201 fell on pairs already in the frozen LMFDB
baseline. Of those, 112 rows were no-scored as lmfdb_baseline_not_improved; the
other 89 rows unlocked 16 distinct pairs by exhibiting a strictly smaller exact
nfdisc than the baseline's, with margins up to 10¹⁴. That is 112 + 89 = 201, in
rows. Sixteen cells of the degree-24 record now have a smaller discriminant than they did,
verified by someone else's pipeline. No sampling assumption, no predicted label, nothing that
can later turn out to have been an estimate wearing the grammar of a measurement.
Why the discriminants are small is structural, not lucky: composita built from small-conductor
pieces, and unit twists over totally real K12 where α being a unit makes the
relative different divide (2). The smallest lines sit at log₁₀|poldisc| = 36 — a root
discriminant near 31.6 at degree 24.
§ 8 · AXLE Cross-Reference, Pedagogy, and Verification Status
Where this sits on the ladder
| Chapter | Supplies | Direction |
|---|---|---|
| Ch φ · Fibonacci | n = 2, the one rung whose group is settled by prime degree | base case |
| Ch η · Tribonacci | n = 3, η ≈ 1.8393, the DNLS spine — prime degree, group closes | base case |
| Ch Gal · Galois | the group question for all n at once; odd composite n open | this chapter |
| Ch Δ · Tetranacci | n = 4 — composite, the obstruction bites | consumes Γ |
| Ch Σ · Pentanacci | n = 5 — prime again, closes again | consumes Γ |
| Ch Ω · Hexabonacci → τ | n = 6 — composite, open; the limit τ = 2 | consumes Γ |
| Ch A · Autophagy | the model for a Lean-verified chapter at 0 sorries | method |
The pattern the ladder exposes: the group closes at prime n and stalls at composite n. φ, η and Σ are settled by the prime-degree argument. Δ and Ω are not, and the τ = 2 limit is approached along a subsequence half of which is out of reach. That is a statement about the ladder, not about the difficulty of any one rung.
Pedagogy — what this chapter teaches that a solved one cannot
The teachable content here is not the Galois correspondence, which every algebra course covers. It is the discipline of the oracle. Three distinct failure modes appeared in this work, and a student can recognise all three:
| Failure | Looked like | Caught by |
|---|---|---|
| Fabricated citation | Complete bibliographic fields — title, journal, volume, pages, DOI | Checking the publisher record before commit |
| Inapplicable hypothesis | A correctly cited theorem about irreducible trinomials | Noticing our trinomial is reducible by construction |
| Statistic read as measurement | 195 distinct spectra, correctly computed | An external verifier returning 31 |
All three share a shape: something that looks like evidence and is not. The defence is the same in each case — an oracle outside the work. For a Lean file that oracle is the kernel; for a degree-24 polynomial it is Magma. Neither can be argued with, which is the point.
Formal-verification status
A result counts as proved here only when #print axioms returns
[propext, Classical.choice, Quot.sound] and nothing else. If sorryAx
appears, the theorem is open regardless of what any README, badge, description or chapter says
about it — including this one. The IGP24 half obeys the same rule with a different kernel: the
verifier's returned status and scoringStatus columns are the claim,
and a locally verified polynomial is a candidate, not a result.
Reproducibility mapping, per house rule: each claim in §§ 5–7 traces to a producing script and
its verifier output. The parity law → tower.py + the 2,443-triple check; the
clustering correction → recluster.py, calibrated against the returned label CSVs;
the 16 discriminant records → the competition's own results CSVs, which are the primary
record and not reproduced from this end.
What is not claimed
No new theorem. The tower construction is standard — adjoining a square root with a prescribed
sign vector is the ordinary way to build a field of given signature, and g_α(x²)
is the definition of the minimal polynomial of a square root, not a discovery. The
contribution there is engineering: no traces, no factorization, and it belongs in a
reproducibility note rather than an abstract. The parity law, the a₀ = N(α)
invariant and the compositum-unreachability of r ∈ {10, 14, 22} are elementary, two-line
arguments, and are stated above as lemmas because that is what they are.
The quantified clustering correction in § 6 is the one item with genuine novelty risk, and it is UNRESOLVED pending a literature search — zbMATH Open or MathSciNet, plus the Klüners–Malle database papers and the LMFDB Galois-group methodology notes, since anyone building those tables at scale met this and may have written the correction down without publishing it as a result. Until that search is run, no novelty claim attaches to it. The sixteen discriminant records do not depend on the outcome.