The object
For n ≥ 2 the n-bonacci polynomial is
p_n(X) = X^n − (X^(n-1) + … + X + 1). Its dominant real root is the
n-bonacci constant: the golden ratio at n=2, the tribonacci constant
η ≈ 1.8393 at n=3, increasing to τ = 2. That ladder
is the algebraic spine of the series.
Multiplying by (X−1) gives a trinomial,
X^(n+1) − 2X^n + 1. That is what puts the trinomial literature in range —
but the trinomial so obtained is reducible by construction, which is a hypothesis failure
and not a detail. See the obstruction.
Lean status
| Result | Status | Evidence |
|---|---|---|
| nBonacci_action_injective | VERIFIED | Mathlib galActionHom_injective, applied directly. No sorry. |
| nBonacci_action_bijective | OPEN | sorry. Surjectivity. See the obstruction. |
| Theorem_Galois | OPEN | Compiles, but derives from the line above and inherits its sorry. |
Irreducibility of p_n | ASSUMED | Carried as hypothesis hirr, not discharged here. |
For prime degree p, a transitive subgroup of S_p containing a
transposition is all of S_p, and surjectivity closes at once. Odd composite
n defeats that route. The chain becomes irreducible ⇒ transitive, then
transitive + primitive + a transposition ⇒ S_n by Jordan — so
primitivity is the load-bearing step. The relevant 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 are statements about
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) over ℚ, so it is reducible and the
action on its n+1 roots fixes 1 and is not transitive. The hypotheses
therefore do not apply as stated, and the transfer from the trinomial to p_n is
itself OPEN — a reduction argument to be written, not a
lookup. Citing the literature does not discharge it.
No theorem number inside 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. Bibliographic fields are recorded under Sources with how each was checked.
IGP24 entry
IGP24 asks for
explicit degree-24 integer polynomials realizing as many of the 25,000 transitive groups
24T1–24T25000, and their signatures, as possible. The frozen
LMFDB-derived baseline covers 286 labels and 622 of the 165,836 possible
(24Tt, r) pairs. Credit is per (24Tt, r) pair, once per team, so the
binding constraint is distinct pairs — not polynomials.
Construction A — composita
24 = 2·12 = 3·8 = 4·6 = 2·2·6 =
2·3·4. A compositum of linearly-disjoint subfields is imprimitive by
construction, which is where most of the 25,000 groups live and where random sparse search
does not go. Random polynomials land in S24 or A24.
min poly of α + cβ from Newton power sums:
s_k = Σ_m C(k,m) p_m(f) p_(k−m)(g) deg f = a, deg g = b, ab = 24Construction B — quadratic towers over totally real fields
A tower is not a compositum, and it reaches signatures no compositum can. 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 give a complex conjugate pair:
signature (2(12−j), j), r = 24 − 2j, j = 0 … 12Choosing α 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 then g_α(x²) where
g_α = m¹²·g((x+k)/m) — integer arithmetic, no resultants
and no power sums.
Irreducibility is free. K12 is totally real, so every square in it is
non-negative at every real place; α is negative somewhere, hence not a square, hence
[K12(√α):K12] = 2 and g_α(x²) is irreducible. No
factorization is performed or needed.
Interval placement of k/m sets the signature: r = 24 − 2j.
Three values — r = 22, 14, 10 — are unreachable by any
compositum, since r = d mod 2 forces an even-degree constituent to have even
signature and each of those requires an odd one.
Square class of N(α) within that interval gives one exact bit of the
group. Since ∏σ(α) = N(α) is rational,
√N(α) always lies in the Galois closure: when N(α) is
a rational square that element is rational and the all-flips element of
C₂¹² acts trivially, confining the twist module to the index-2
kernel of the sum map; when it is not, ℚ(√N(α)) is a quadratic
subfield not inherited from K12 and the module can reach the full
2¹².
The bit is readable off the submitted line. g_α is monic of even
degree, so the constant term of the degree-24 polynomial is exactly
a₀ = g_α(0) = N(α). One integer square-root test classifies a line
— no Frobenius profiling, no threshold, no calibration.
Necessary, not complete: it splits the twist module by one bit, not into all
its submodules. But that bit is exact where a sampled profile is statistical. Checked against the
twelve r=16 classes below — six have square a₀, six
non-square, and no class contains both.
Verifier results
Everything in this section is returned by the official Magma pipeline, not asserted here.
| Submitted | Lines | Accepted | Labels | Pairs | Scoring |
|---|---|---|---|---|---|
| 15 Aug 17:37 | 588 | 588 | 31 | 39 | SCORED 34 scoreable, 16 unlocked |
| 16 Aug 06:03 | 450 | 450 | 121 | 213 | PENDING composita, r = 0…24 |
| 16 Aug 06:44 | 86 | 86 | 10 | 10 | PENDING r=20 composita |
| 16 Aug 11:27 | 43 | 43 | 7 | 7 | PENDING r=20 tower |
| 16 Aug 11:36 | 57 | 57 | 16 | 16 | PENDING r=16 tower |
| 16 Aug 11:46 | 6 | 6 | 3 | 3 | PENDING redundant, see below |
| 16 Aug 11:52 | 238 | 238 | 5 | 20 | PENDING towers r=22,18,14,10 |
| union | 1468 | 1468 | 159 | 304 | — |
Of submission 1's 588 accepted rows, 201 fell on pairs already in the frozen baseline. 112 of
those were no-scored as lmfdb_baseline_not_improved. The other 16 baseline pairs
were unlocked on a strictly smaller exact nfdisc, with margins up to
10¹⁴ — the composita are built from small-conductor pieces, so their
discriminants are structurally small.
This page previously reported that the mod-p ladder found
195 distinct cycle-type spectra across the 587 fields of submission 1, and that since
different spectra force different Galois groups, 195 was a lower bound on distinct groups. The
verifier returned 31 distinct labels and 39 distinct
(24Tt, r) pairs 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 the expected
L1 distance is ~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, at 1000 primes, and calibrating the constant
against the returned Magma labels recovers 38 of the 39 true pairs with every cluster
pure. The old figure was an estimate presented in the grammar of a measurement.
What the tower reaches
Predicted class counts are from the local Frobenius clustering; pair counts are what the verifier returned.
| submission | signatures | predicted | returned pairs | returned labels |
|---|---|---|---|---|
| r=20 tower | 20 | 7 | 7 | 7 |
| towers | 22, 18, 14, 10 | 20 | 20 | 5 |
| r=16 tower | 16 | 12 | 16 | 16 |
| r=20 composita | 20 | 9 | 10 | 10 |
The 238-line submission returned exactly the 20 pairs predicted — but from only
five distinct labels: 24T14744, 24T14745, 24T16693,
24T16694, 24T19635, the identical set at every one of
r = 22, 18, 14, 10. Sliding k/m along the conjugate
ladder moves the signature and leaves the group where it was. Since credit is per
(24Tt, r), five groups still bought twenty pairs — but the group axis
contributed nothing, and the per-signature clustering could not have detected this, because it
never compared across signatures.
All five labels have non-square a₀ — and that turns out to be
forced, not accidental. See the parity coupling below.
A six-line submission was wasted here. It added α from the opposite square class
as companions to the r=16 tower lines; the verifier returned 3 pairs, all three
already present in that earlier submission. The earlier file already spanned both square classes
— six classes with square a₀ and six without, a fact measured before the
companion file was built and not consulted while building it.
Write N(α) = ∏σ(α) over the twelve real embeddings of the
totally real K12. Exactly j of the factors are negative, so
sign N(α) = (−1)^jFor odd j this is negative, and a negative rational is never a square.
Since √N(α) = ∏√σ(α) always lies in the Galois
closure, the square class of N(α) 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¹². Therefore:
| signature | j | r | N(α) | module class |
|---|---|---|---|---|
| r ≡ 0 (mod 4) | even | 24,20,16,12,8,4,0 | positive | both classes available — a free bit |
| r ≡ 2 (mod 4) | odd | 22,18,14,10,6,2 | negative | non-confined only, always |
The argument uses nothing about the shape of α — only how many real places it is
negative at — so it holds for every α in K12, not just the linear family
mθ − k used here. Checked on 2,443
(K12, m, k) triples: 2,443 confirm, 0 violate.
This explains the collapse above exactly. The 238-line submission targeted
j = 1, 3, 5, 7, all odd, so every line was forced into one module class and the four
signatures could only ever return the same groups. It is also the practical rule: at
r ≡ 2 (mod 4) the tower has no group axis at all, and more classes there require a
different block structure, not a wider search. The square classes observed in the returned labels
agree — 24T7819, 7829, 7831, 7834, 10257–10259, 12727, 12729, 14761
occur only at r = 16, 20, never at r = 22, 18, 14, 10.
None of the 20 tower pairs appears in the competition's published uncovered-signature list, so
the construction landed entirely on ground already held by someone. The list has 2,722 open cells
across 1,253 groups, and r=22 appears nowhere in it — equally consistent with
those cells being covered and with their never having been enumerated, and this page does not
choose between those readings.
The smallest lines sit at log₁₀|poldisc| = 36, a root discriminant of
about 31.6 at degree 24. Those all have |a₀| = 1: α is a unit, so the
relative different divides (2). A unit is a square class representative, which
couples the two axes — the small-discriminant lines are exactly the confined-module
ones, and reaching the full 2¹² means giving up the unit and with it the
small discriminant.
No 24Tt label was computed locally: this entry was prepared without Magma, and
the official verifier assigns the labels. Predicted labels are inferred from Frobenius density
profiles, appear in no column of any submission, and affect nothing. Clustering counts are
exhaustive for these constructions, not proofs that no further classes exist at a
signature. The tower class counts above rest on profiles computed over 400 primes at
r = 22,18,14,10 and 250 at r = 20,16; a wider
α sweep across both square classes would likely raise them.
Nothing here is described as a discovery until the verifier says so, and for the tower submissions it has not yet said so.
Reproducing
python3 gen_igp24_v2.py # composita: 754 constructions -> 587 distinct fields
python3 tower.py build j # towers: K12(sqrt a), j negative places, r = 24-2j
python3 tower.py profile j
lake exe cache get && lake build
#print axioms Theorem_GaloisA 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. The IGP24 analogue is the verifier's returned status and
scoringStatus columns; a locally verified polynomial is a candidate, not a result.
Sources
pub publisher or primary record · search bibliographic data from search; PDF not read · given full text supplied to this repository · pers personal communication, unverified · retracted recorded error
Mathematics.
- search A. Movahhedi and A. Salinier, The primitivity of the Galois group of a trinomial, J. London Math. Soc. (2) 53 (1996) 433–440. 10.1112/jlms/53.3.433
- search S. D. Cohen, A. Movahhedi and A. Salinier, Double transitivity of Galois groups of trinomials, Acta Arith. 82 (1997) 1–15.
- search S. D. Cohen, A. Movahhedi and A. Salinier, Galois groups of trinomials, J. Algebra 222 (1999) 561–573.
- pub C. Jordan, Théorèmes sur les groupes primitifs, J. Math. Pures Appl. (2) 16 (1871) 383–408.
- pub LMFDB Collaboration, Galois groups of degree 24, lmfdb.org/GaloisGroup/?n=24. Frozen baseline CSV downloaded from the competition site and used for all baseline comparisons on this page.
- retracted “On the Galois group of trinomials”,
J. Algebra 182 (1996) 322–333,
10.1006/jabr.1996.0172— no such article. Title, journal, volume, pages and DOI all incorrect. Proposed as a replacement for a[CITE NEEDED]marker, checked, and rejected before commit.
Standards of practice.
- given H. Cohn, Advice for amateur mathematicians on writing and publishing papers, cohn.mit.edu/advice. Full text supplied to this repository; the page itself was not fetched.
- pub T. Tao, Advice on writing papers, terrytao.wordpress.com
- pub M. Abouzaid, N. Srivastava, R. Ward and L. Williams, First Proof Second Batch, arXiv:2606.18119v1 [cs.AI], 16 June 2026. Its four grading categories — essentially flawless, minor revisions, major revisions, reject — are used on this page as an evaluation rubric. Tao appears there as a UCLA principal investigator on System B, not as an author or editor.
- pers Recommendation of the above as a benchmark for “flawless”. Personal communication; date and channel not recorded.
The three search entries rest on bibliographic
search results, not on a review database. MathSciNet or zbMATH Open resolves each in under a
minute and promotes them to pub; until that is run, they are recorded at
the tier they were actually checked at. The retracted line stays
because a source list with no errors in it is an assertion, while one that records a caught error
and how it was caught is evidence of a process — the same reason
#print axioms outranks a badge.
Standard of claim
Self-reported metadata does not count. A repository description, a README, a CI badge and a chapter's prose are assertions about an artifact; only the kernel is evidence. IGP24 works the same way — it discards claimed labels and discriminants in submissions and computes its own, and its integrity rules make presenting a baseline pair as new an explicit violation.
This repository previously described itself as having proved that the action map is a bijective
isomorphism for all odd composite n, while the file carried sorry. That
is corrected, and the correction is recorded rather than quietly applied.
Two later corrections are recorded the same way. The obstruction's Movahhedi–Salinier
reference was carried as [CITE NEEDED], named from working knowledge. A replacement
was proposed with complete bibliographic fields — title, journal, volume, pages, DOI —
and checking it against the publisher record before commit found that no such article
exists; only the authors and the year were right. This is the failure mode Table 5 of
arXiv:2606.18119 documents across most graded
submissions, and it is why nothing on this page cites a theorem number from a PDF that has not
been read. Checking the reference surfaced the second correction: the trinomial primitivity
results assume irreducibility, so they do not apply to X^(n+1) − 2X^n + 1
without a reduction argument that has not been written. A plausible-looking citation and a
plausible-looking applicability are the same failure mode as a green badge over a
sorry.
A fourth correction, of a different kind. The 195-spectra figure above was not a bad citation and not a bad proof — it was a statistic computed correctly and interpreted as something it was not. The count was right; calling it a lower bound on distinct groups was wrong, because the invariant it counted was sampled rather than exact. It survived until the verifier returned 31 labels against it. A number carrying an implicit modelling assumption is the same species of claim as a badge: it looks like evidence and is not, and the only cure is an independent oracle. That is why the results section reports only what the Magma pipeline returned, and why the tower rows in it are marked NOT YET RETURNED rather than counted.
Contact
Built in-page: no third-party script, no cookies, nothing that fails invisibly if a reader blocks trackers.