WP65 · The Oracle Outside the Work

§1 · Three Things That Looked Like Evidence

In August 2026 this project ran a two-day campaign against the degree-24 inverse Galois problem: 1,468 polynomials in seven submissions, every one accepted by an official Magma verifier that nobody here controls. The mathematics is in Chapter Gal. This paper is about something the campaign produced incidentally and which travels further than the mathematics did.

Three separate claims made during the work looked like evidence and were not. They failed in three different ways, and each was caught by a different kind of oracle. Setting them side by side is more useful than any of them individually, because the shape they share is the thing worth teaching.

Failure	What it looked like	Oracle that caught it
Fabricated citation	A reference with complete bibliographic fields — title, journal, volume, pages, DOI	The publisher record, checked before commit
Inapplicable hypothesis	A correctly cited theorem, about irreducible trinomials	Noticing our trinomial is reducible by construction
Statistic read as measurement	195 distinct cycle-type spectra, correctly computed	An external verifier returning 31

The first is the familiar one and the easiest to guard against: check the record. The second is harder, because the citation was real — the failure was in the fit between hypothesis and object, and no bibliographic check detects that. The third is hardest, because nothing about it is false. The 195 was computed correctly from real data. What was wrong was the word attached to it.

A number that carries an unstated modelling assumption is the same species of claim as a green badge over a sorry. It looks like evidence. It is a summary of a belief.

§2 · Method — Two Ways to Build a Field to Order

The inverse problem asks for a polynomial realising a prescribed group. Degree 24 admits two usable constructions, and the difference between them turned out to matter more than either individually.

Composita

Since \(24 = 2\cdot 12 = 3\cdot 8 = 4\cdot 6 = 2\cdot 2\cdot 6 = 2\cdot 3\cdot 4\), a field can be assembled from smaller ones. A compositum of linearly disjoint subfields contains both, so its group is imprimitive by construction — exactly the region a random search never visits, since random polynomials land in \(S_{24}\) or \(A_{24}\). The minimal polynomial of a sum of generators comes from Newton power sums, exactly, with no resultants:

s_k = Σ_m C(k,m) · p_m(f) · p_(k−m)(g)

Towers

A tower is not a compositum. Take \(K_{12}\) totally real of degree 12 and \(\alpha \in K_{12}\) negative at exactly \(j\) of its twelve real places. In \(K_{24} = K_{12}(\sqrt{\alpha})\) 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 … 12

One parameter sweeps the whole signature axis from a single base field. Choosing \(\alpha\) is exact rather than a search: \(m\theta - k\) is negative precisely where \(\theta_i < k/m\), so placing \(k/m\) in the gap \((\theta_j, \theta_{j+1})\) gives exactly \(j\) negative places. The minimal polynomial is \(g_\alpha(x^2)\) with \(g_\alpha = m^{12}g((x+k)/m)\) — integer arithmetic throughout. Irreducibility is free: \(K_{12}\) totally real makes every square non-negative at every real place, \(\alpha\) is negative somewhere, so \(\alpha\) is not a square and \(g_\alpha(x^2)\) is irreducible. No factorization is performed or needed.

Neither construction is novel. Adjoining a square root with a prescribed sign vector is the ordinary way to build a field of given signature, and \(g_\alpha(x^2)\) is the definition of the minimal polynomial of a square root. What is contributed here is engineering — no traces, no factorization — and it belongs in a reproducibility note, not an abstract.

§3 · Two Lemmas the Campaign Produced

Lemma 1 · signatures no compositum reaches

Across a generic compositum the signature multiplies: \(r = \prod r_i\) with \(r_i \le d_i\) and \(r_i \equiv d_i \pmod 2\). Enumerating 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 \in \{0,2,4,6,8,12,16,18,20,24\}\). The complement is exactly \(r \in \{10, 14, 22\}\): 22 needs \(2\cdot 11\) or \(1\cdot 22\), and 11 and 22 each overshoot or mis-parity every available \(d_i\); likewise 10 and 14.

Stated for the generic primitive element — unreachability by the generic compositum, not a theorem about every degree-24 field with a proper subfield.

Lemma 2 · parity couples signature to group

Write \(N(\alpha) = \prod \sigma(\alpha)\) over the twelve real embeddings. Exactly \(j\) factors are negative, so \(\operatorname{sign} N(\alpha) = (-1)^j\). Since \(\sqrt{N(\alpha)} = \prod \sqrt{\sigma(\alpha)}\) always lies in the Galois closure, the square class of \(N(\alpha)\) 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 \(K_{12}\). For odd \(j\), \(N(\alpha) < 0\) and is never a square. Hence at \(r \equiv 2 \pmod 4\) only one module class occurs, for every \(\alpha\), and the group is not a free parameter.

Verified on 2,443 \((K_{12}, m, k)\) triples: 2,443 confirm, 0 violate. The argument uses only \(\alpha\)'s sign pattern, so it holds for every \(\alpha\), not only the linear family.

A free corollary: the constant term of the submitted degree-24 polynomial is exactly \(a_0 = g_\alpha(0) = N(\alpha)\), because \(g_\alpha\) is monic of even degree. One integer square-root test on the first coefficient reads the module class off the page.

Both are elementary — two lines each — and are stated as lemmas because that is what they are. Calling them results would be the fourth failure mode in a paper about the first three.

§4 · What the Oracle Returned

Seven submissions, 1,468 polynomials, all accepted. Every figure is verifier output.

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 final row is Lemma 2 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 one module class. Sliding \(k/m\) moves the signature and leaves the group where it was. The prediction was right about the count and blind to the reason.

The result that does not depend on interpretation

Of 588 rows in the first submission, 201 fell on pairs already in the frozen LMFDB baseline. 112 of those 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, margins up to \(10^{14}\). 112 + 89 = 201, in rows; 16 in pairs. Sixteen cells of the degree-24 record now carry a smaller discriminant than they did, verified by a pipeline this project does not control. No sampling assumption, no predicted label, nothing that can later turn out to have been an estimate.

§5 · The Verification Standard, Stated Twice

The series has one standard of claim, and the campaign showed it has two instantiations that behave identically.

Instantiation A · Lean 4

A result counts as proved 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.

Instantiation B · the competition verifier

A polynomial counts when the official Magma pipeline returns status = ok with a computed label and signature. Claimed labels, discriminants and metadata in a submission are discarded by the evaluator, which computes its own — and presenting a baseline pair as new is an explicit integrity violation in the rules.

Both are oracles the author cannot argue with, and that is the whole of their value. Note what the second one does that the first does not: it also catches errors of interpretation. A Lean kernel will not tell you that your 195 spectra were 31 groups, because that claim was never inside Lean. The competition verifier did, because the claim was inside its domain.

Pick the oracle whose domain contains the claim. An oracle outside the claim's domain certifies nothing about it, however rigorous it is elsewhere.

§6 · Pedagogy — What to Teach From This

The teachable content is not the Galois correspondence. It is a habit with three parts, and each part corresponds to one of the failures in §1.

Check the record before the commit, not after. A complete-looking set of bibliographic fields is not a citation. The replacement reference proposed during this work had title, journal, volume, pages and DOI, and described no such article; only the authors and the year were right.
Check the fit, not just the source. A correctly cited theorem about irreducible trinomials says nothing about a trinomial that is reducible by construction. This is invisible to every bibliographic tool and visible to anyone who reads the hypothesis.
Name the unit of every number you report. "195 distinct spectra" was true. "195 is a lower bound on distinct groups" was false, and the gap between them is the difference between a sampled invariant and an exact one. Reporting rows where the reader expects pairs is the same error at smaller scale — this paper's §4 states 112 + 89 = 201 in rows and 16 in pairs precisely because an earlier draft mixed them and produced a number that did not reconcile.

For a 16-week course the natural placement is late — after students have produced something of their own to be wrong about. The exercise that works is not "find the error in this argument" but "state the unit of every number in your own last write-up." The first is a puzzle; the second is the habit.

§7 · Cross-Reference — Where This Lands

The campaign's output is distributed across four repositories. This table is the map, and it is the authoritative statement of what exists versus what is planned.

Destination	Content	Status
`AXLE/chGal-galois.html`	Ch Gal · The Galois Group of the Ladder — the mathematics, Recurrence Ladder chapter	WRITTEN
`book6/wp65-…` (this paper)	The verification standard and the three failure modes	WRITTEN
`AXLE/chapters.html`	A Γ card on the Recurrence Ladder, between η and Δ	TO ADD
`geometry/` galois page	Technical page: Lean status, IGP24 results, corrections ledger	NEEDS EDIT — two inconsistencies listed below
Lean · `NBonacci.lean`	`nBonacci_action_injective` closed; surjectivity open; primitivity absent from Mathlib	1 SORRY
Zenodo · new deposit	The 16 discriminant records + construction note + producing scripts	TO DEPOSIT
Ch Δ · Tetranacci, Ch Ω · Hexabonacci	Consume Γ: composite \(n\), where the obstruction bites	TO CROSS-LINK
Ch φ, Ch η, Ch Σ	Consume Γ: prime \(n\), where the group closes	TO CROSS-LINK

Carried forward — two defects on the geometry galois page

The standard-of-claim section describes tower rows as NOT YET RETURNED while the results table tags them PENDING. One tag, two names, in the section that is specifically about labelling unverified things carefully. Pick one.
The baseline figures were stated as 201 / 112 / 16 without units, and 112 + 16 ≠ 201. The reconciliation is in §4 above: 201 and 112 and 89 are rows, 16 is pairs. Restate on the page in a single unit.

§8 · Open, and What Would Close It

The Lean obligation is precise. Surjectivity of the n-bonacci Galois action needs primitivity; primitivity for trinomials is Movahhedi–Salinier (1996) and Cohen–Movahhedi–Salinier (1997, 1999), which are not in Mathlib; and before that, the transfer from the reducible trinomial \(X^{n+1} - 2X^n + 1\) back to \(p_n\) is a reduction argument that has not been written. Two obligations, in that order. Neither is closed by a tactic search.

The novelty question is unresolved and gates only one item. The quantified clustering correction — the size of the overcount, the \(S/\sqrt{n}\) scaling, the corrected threshold validated against returned labels — is the one thing here with genuine novelty risk. The qualitative caveat is classical; Dedekind gives containment only. Before any novelty claim attaches, the search has to run: zbMATH Open and 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.

The sixteen discriminant records do not depend on that outcome. They are a fact about the mathematical record, externally verified, and they are the artifact to ship first — as a data deposit with the producing scripts, not as a paper.

If the methods note turns out to be known, the records remain. Ship the thing that does not depend on anyone's literature.

Reproducibility, per house rule: every numerical claim in §§3–4 traces to a producing script in the campaign folder and, where the claim is about verifier output, to the competition's own results CSVs — which are the primary record and are not reproduced from this end. The parity law traces to the 2,443-triple check; the clustering correction to the recluster script calibrated against the returned label files.