The maximal height of a divisor of x^(p²q²)-1: a conjecture of Ryan, Ward and Ward beyond its verified range, and two explicit formulas

Conjecture 3.3 of Ryan-Ward-Ward (arXiv:1009.5970 = Involve 3 (2010) 451-457) – B(p² q²) is the larger of H(Phiₚ Phi_q Phi_(p² q) Phi_(p q²)) and H(Phiₚ Phi_q Phi_(p²) Phi_(q²)) – holds at 109 pairs OUTSIDE the source's verified box 2 <= p < q < 60: p in 2,3,5,7,11,13 and q >= 61, up to q = 241 (p=2), 199 (p=3), 113 (p=5,7), 97 (p=11,13). Each pair carries a tower certificate (prod_(d|m) f_d = xᵐ - 1 for all nine m | p²q²) pinning the nine coefficient arrays to the nine cyclotomic polynomials, and the exact values B(p²q²), H(Phiₚ Phi_q Phi_(p² q) Phi_(p q²)) and H(Phiₚ Phi_q Phi_(p²) Phi_(q²)). 144 pairs kernel-bound in all (the source's box is reproduced as well); 386 pairs computed in C, largest n = 11² 373² = 16834609 (p=11) and 2² 599² = 1435204 (p=2), zero failures.

B(4 q²) = 4 for every prime q with 3 <= q <= 241, kernel-bound (52 pairs; all 108 primes q <= 599 in C) – a closed formula on the line p = 2 of a kind the source explicitly lacks ('we also lack an explicit formula for the height of the polynomial'). The lower bound B(4q²) >= min4, q² = 4 is the source's Theorem 3.1; the content is the matching upper bound over all 2⁹ divisors of x^(4q²)-1 built from the nine cyclotomic factors.

B(9 q²) = 12 if q = 5 (mod 9), 11 if q = 7 (mod 9), and 9 = min3², q² on the four classes 1, 2, 4, 8 (mod 9), for every prime q with 5 <= q <= 199, kernel-bound (44 pairs; all 76 primes q <= 397 in C, 11 to 14 per class). A closed formula on the line p = 3, and a statement that the source's Theorem 3.1 lower bound is sharp on four of the six residue classes.

Negative controls for the family. Neither branch of Conjecture 3.3's max is B(p²q²) alone (H = 21 < 25 = B at (5,11); H = 9 < 12 = B at (3,5) – the source's own two examples); the source's Theorem 3.1 bound B >= p² is not an equality (B(3² 5²) = 12 > 9); the tower certificate rejects a table with one coefficient bumped and a table with Phi_(p²) replaced by Phiₚ; report p q = report q p, so the source's p < q is a normalisation; and B(p²q²) is not a function of q mod p² (45 vs 49 at 7 = 107 mod 25, 69 vs 92 at 11 = 109 mod 49).

Pomerance-Ryan's B(pq) = minp, q (Illinois J. Math. 51 (2007) 597-604) and Kaplan's B(p² q) = minp², q (J. Number Theory 129 (2009) 2673-2688), recomputed at 11 pairs each by this family's own power-set sweep with the tower certificate passing – the engine control for every B(p²q²) value in the family.

eq_cyclotomicₒfₜower: for n >= 1, if a family f: N -> Z[X] satisfies prod_(d | m) f d = Xᵐ - 1 for every m dividing n, then f d = Polynomial.cyclotomic d Z for every d dividing n. The tower certificate has a unique solution, which is what turns the finite array check Kernel.towerOK into a proof that the nine coefficient arrays are the nine cyclotomic polynomials. Mathlib, kernel-clean (propext, Classical.choice, Quot.sound).

dvd_Xₚowₛubₒneᵢff and heightPₑqₛubsetₚrodₒf_dvd: for n >= 1, f divides Xⁿ - 1 in Z[X] iff f is associated to prod_(d in S) cyclotomic d Z for some S subseteq n.divisors; and since the units of Z[X] are +-1 and the height H is sign-blind, every divisor of Xⁿ - 1 has the height of one of the 2ᵗau(n) subset products, so B(n) is exactly that maximum. This is the reduction Ryan-Ward-Ward assert in one sentence to justify their power-set algorithm, and the statement that makes every native_decide in this family a statement about B(n). Mathlib, kernel-clean.

The explicit height formula the source says it lacks, on two lines. Ryan-Ward-Ward write, immediately after Conjecture 3.3: 'In addition to not having a proof for this conjecture, we also lack an explicit formula for the height of the polynomial.' Here: H(Phi₂ Phi_q Phi_(4q) Phi_(2q²)) = 4 for every prime 3 <= q <= 241, and H(Phi₃ Phi_q Phi_(9q) Phi_(3q²)) = 12, 11, 9 according as q = 5, 7, or 1,2,4,8 (mod 9), for every prime 5 <= q <= 199. Also: on the whole line p = 3 the maximum of Conjecture 3.3 is attained by its FIRST product (B = hOdd at all 44 pairs), i.e. that product never falls below the Theorem 3.1 value 9; and on the line p = 2 both products have height 4. Read off the certified tables of Line2/Line3 by kernel decide – Heights.lean contains no native_decide.

The mod-p² refinement (Conjecture 6.1 of families/cyclo-height-p2q2/paper/draft.tex: B(p²q²) = B(p²q'²) for primes q = q' (mod p²) with q, q' > p²) SURVIVES its first tests at p = 13 (1 class) and at 5 classes at p = 11 (all but 10 mod 121 new; that one reproduces the founding run's decisive pair). At p = 13: 64 mod 169 (q = 233, 571, all B = 169). At p = 11: 10 mod 121 (q = 131, 373, all B = 121); 16 mod 121 (q = 137, 379, all B = 161); 46 mod 121 (q = 167, 409, all B = 253); 58 mod 121 (q = 179, 421, all B = 220); 76 mod 121 (q = 197, 439, all B = 166). Every one of the 12 residue classes tested here – classes at p = 2, 3, 5, 7, 11, 13, each of whose computed members exceeds p² – has a constant B, with no exception; 50 pairs computed in C, largest n = p²q² = 55,100,929 at (p,q) = (13,571), 3595 CPU-s in all. The tested pairs at p = 11 and p = 13 differ by exactly 2p², so the agreement also discriminates against any larger modulus such as p³. The journal also restates the conjecture without a congruence: for q > p² the map q mod p² -> (sigma, rho mod p) of the Lam-Leung parameters of Phiₚq is well defined and injective (checked exhaustively for p = 3, 5, 7, 11, 13 by tools/classᵣeport.py –lamleung), so Conjecture 6.1 says exactly that B(p²q²) is a function of the shape of Phiₚq that survives letting q grow; sigma alone (= q mod p) is provably not enough, since sigma = 9 at p = 11 carries B = 121 at q = 131, 373 and B = 166 at q = 197, 439, separated by rho mod p = 0 against 6.

A strengthening of the refinement that the same runs support: on a residue class mod p² all of whose members exceed p², not only B(p²q²) but the entire FAMILY of maximising subsets agrees, read as subsets of 0,1,2² via d = pᵃ qᵇ. Verified on 12 of the 12 classes tested, including the class 10 mod 121 where the maximum 121 is attained by 22 different subsets at q = 131 and by the same 22 at q = 373, and the class 64 mod 169 where the same happens at q = 233 and q = 571 (n = 9 174 841 and n = 55 100 929). A further regularity, at odd p: whenever B(p²q²) = p² the maximisers are exactly 22 subsets and they are the SAME 22 subsets of 0,1,2² for every p and q tested (nine pairs over p = 3, 11, 13). The two boundary cases fit: (5,11) has q = 11 < 25 = p² and its 6 maximisers are a proper subset of the 22; p = 2, where B(4q²) = 4 = p² always, has 36 maximisers (the same 36 at q = 5,7,11,13,17,19,23) which CONTAIN the 22 plus 14 more, because Phi_(2q)(x) = Phi_q(-x) is flat there. This is the statement a Kaplan-style bijection between index sets would produce, and it is cheaper to falsify than the value statement.

Negative control on the shape of the refinement: the +- fold of Wang's Theorem 1.8 (q = +-r mod p forces B(pqᵇ) = B(prᵇ), b <= 5) does NOT survive the passage from p to p². Three refutations with BOTH members above p², so the refinement's own hypothesis holds on each side: B(3² 23²) = 12 vs B(3² 13²) = 9 with 4 = -5 (mod 9); B(5² 107²) = 49 vs B(5² 43²) = 45 with 18 = -7 (mod 25); B(7² 151²) = 63 vs B(7² 241²) = 69 with 45 = -4 (mod 49). One accidental agreement recorded so the control is not overread: B(7² 59²) = B(7² 137²) = 98 with 39 = -10 (mod 49). Together with the founding run's controls this pins the refinement from both sides: the modulus must be p² and not p, the threshold q > p² cannot be dropped, and the classes must not be folded by sign.

Conjecture 3.3 of Ryan-Ward-Ward holds at every one of the 50 pairs computed by this dispatch, of which 32 are OUTSIDE the source's verified box 2 <= p < q < 60 (the rest reproduce values inside it as controls), with the tower certificate passing on each; the largest is n = 55,100,929 at (p,q) = (13,571). Each pair carries the exact B, H₁ = H(Phiₚ Phi_q Phi_(p²q) Phi_(pq²)) and H₂ = H(Phiₚ Phi_q Phi_(p²) Phi_(q²)) in the format the family's genₘodule.py already parses (families/cyclo-height-p2q2/tools/p11p13-classes.log), so any of them can be turned into a kernel-bound Rows table without recomputing.

A corrected cost model for this family's C sweep, and the measured price of the p = 17 test. The founding journal's fit C-seconds 7.2e-8 (pq)² (p+q) is good only to a factor of 2 because it treats nnz(Phiₚq) as 0.28 pq; by Lam-Leung nnz(Phiₚq) = (rho+1)(sigma+1) + (q-1-rho)(p-1-sigma) with rho p + sigma q = (p-1)(q-1), which swings by a factor of about (p-1)²/4 across the classes of q mod p. Fitting C-seconds c. pq(p+q-1) nnz(Phiₚq) instead gives c between 0.84e-7 and 1.53e-7 over nine representative pairs – a spread of 1.8 where the old model spreads by 3.2 – with the residual a systematic upward drift of c with n rather than scatter. Peak RSS is 6 bytes per unit of n (measured 16.7 MB at n = 2.08e6, 55.2 MB at n = 9.17e6), not the 10*4*n allocation bound, so the founding journal's '2.2 GB' for (13,571) was an over-estimate by a factor of about 8. Consequence: the p = 17 test – q = 359 against q' = 937, the cheapest pair with both members above 289 – prices at 3.4 to 6.7 CPU-h in C (an extrapolation: c was fitted only up to n = 5.5e7 and this is n = 253 733 041) and 1.5 GB, dominated by the single run (17,937). PARKED at that price, which is over the 4 CPU-h per-statement cap either way.

B(11². 137²) = B(11². 379²) = 161, KERNEL-BOUND (sorry-free, native_decide confined to the polynomial arithmetic), with Conjecture 3.3 of Ryan-Ward-Ward and the nine-factor tower certificate holding at both pairs. 137 and 379 are the two primes below 500 in the residue class 16 mod 121; both exceed p² = 121, they differ by exactly 2. 121, and the common value 161 is strictly ABOVE p² – so this is the first kernel-bound instance of the family's mod-p² refinement (rows CH9-CH10, C-only until now) at a class where the agreement is not the trivial one forced by the source's Theorem 3.1 B(pᵃ qᵇ) >= minpᵃ, qᵇ. n = 11². 379² = 17,380,561 is the largest instance kernel-bound in this family, 10.9x the previous largest (13². 97² = 1,590,121 in Strip1113.lean). A STRENGTHENING also bound here: splitting the 2⁹ subsets into the eight blocks given by the inclusion pattern of Phi₁, Phi₁1, Phi₁21, the maximum height inside EACH block agrees across the class – (68, 99, 161, 121, 121, 121, 121, 121) at q = 137 and at q = 379 – a strictly finer invariant than B, which is the maximum of the eight. The maximum sits in the block holding Conjecture 3.3's first product (Phi₁1 in, Phi₁ and Phi₁21 out); its second product sits in the block whose maximum is 121 = p². C-measured (not bound): the same block profile agrees across the classes 10 mod 121 ((109, 110, 121, 121, 121, 121, 121, 121) at q = 131 and 373) and 46 mod 121 ((71, 66, 253, 121, 121, 121, 121, 121) at q = 167 and 409), and differs between classes.

Negative controls for the class 16 mod 121, all kernel-checked from the certified values. TOO SMALL: B(11² q²) <= 160 fails at q = 137 and at q = 379, and B(11² q²) = 121 = p² fails at both – 121 is exactly the value on the other tested p = 11 class (10 mod 121, q = 131, 373), so the control separates the two classes rather than refuting an arbitrary number. TOO LARGE: 162 <= B(11² q²) fails at both, so the certified value is exact and not a lower bound. NON-VACUITY: 11, 137 and 379 are prime (trial division in the kernel), 137 and 379 are distinct and congruent mod 121, and both exceed 121 – the class hypothesis has two witnesses. SPLIT CONTROL: the eight-block split of CH16, evaluated at (11, 137), reassembles to exactly the value that the UNDIVIDED sweep of the same pair certifies (Class16A.c137ₒk against Class16S.bOf137ₛplit), so the split neither drops nor double-counts subsets.

Kernel-clean lemmas that split ONE native_decide accumulator fold across independent files, in LeanProblemSpec/CycloHeightP2q2/Split.lean: sweepₛplit3 (a depth-first sweep over a list of at least three factors equals its eight depth-3 leaves chained in the binary order of the inclusion pattern – by rfl, three unfoldings of the defining equation); sweepₘx (sweep l cur (mx a b) = mx a (sweep l cur b), so the running maximum's seed is only ever maxed against, hence every leaf can be certified with seed 0 and the chain rebuilt afterwards by kernel arithmetic on numerals – this is what makes the files INDEPENDENT rather than sequential); and reportₒfₚarts, which rebuilds the family's Report structure from separately certified towerOK, bOf, H1 and H2 values so a split pair re-enters the existing Rows machinery unchanged. The split is even by construction: the three factors fixed are the three cheapest (Phi₁, Phi₁1, Phi₁21, coefficient-array sizes 2, 11, 111 against the six others up to 15,758,821), so the eight leaves cost 1/8 each to within a part in 10⁴. MEASUREMENTS that made it necessary, all from this dispatch: the undivided (11,379) sweep is 65 minutes of compiled Lean against a 30-45 minute per-file stop rule; the Lean-to-C ratio with –load-dynlib is 19.4x-24.9x at this scale (the founding run's 21x from eight small pairs holds up); and user CPU time on this box is itself load-dependent by 46% (the same two C runs: 302.2 CPU-s recorded at load 49 in journal/2026-09-03-cyclo-height-p13.md against 207.3 CPU-s here at load 25), which is why a Lean price extrapolated from a loaded-box C measurement runs high.

B(11². 131²) = B(11². 373²) = 121 = p², KERNEL-BOUND with Conjecture 3.3 and the tower certificate at both pairs: the founding run's decisive p = 11 refinement test (class 10 mod 121, the two primes below 500 in it, both above p², differing by 2. 121), which had been C-only. This is the TRIVIAL-VALUE side of the refinement – the common value is exactly the lower bound minp², q² of the source's Theorem 3.1 – and binding it next to the class 16 mod 121 (value 161) turns the refinement's content into a theorem: classes₁0₁6_differ states that over the four primes 131, 373, 137, 379, all above p² = 121, B(11²q²) is CONSTANT on each residue class mod 121 and DIFFERS between the two classes (121 against 161). So the residue does real work: B is neither eventually constant in q nor forced to minp², q². That is a non-vacuity control for the refinement conjecture itself, and it complements Controls.noₘodₚ2ₗawₐt₅/ₐt₇, which refute the same law when members q < p² are admitted. The eight-block profile is again class-invariant and again distinguishes the classes: (109, 110, 121, 121, 121, 121, 121, 121) at q = 373 against (68, 99, 161, 121, 121, 121, 121, 121) at q = 137, 379. Controls: B <= 120 fails, 122 <= B fails, and B = 161 (the other class's value) is refuted at both pairs; 131 and 373 are prime, distinct, congruent mod 121.