# Verification report — AMR-150-0035 (A. Nies, Tianyuan problem list 2025, Problem 16: Hausdorff dimensions of computable subgroups of topologically finitely generated computable profinite groups)

Verification dates: 2026-10-18 (two independent verification runs on the first written version of the results; a
third independent verification run on the note as written; the program `check_note.py`).

**Verdict.** The note answers the question, under the conventions of Mayordomo and Nies: **the values are exactly
the left-Σ₂ reals in [0, 1]; finite generation imposes no restriction.**
- **The statement.** Every left-Σ₂ real r ∈ [0, 1] is the Hausdorff dimension of a computable subgroup of a computable
  profinite group; which values occur when the group is also topologically finitely generated?
- **Conventions (the source prints none; taken from Mayordomo–Nies and Nies's 2025 slides).** A computable profinite
  group is given by a computable inverse system (L_n, p_n) of finite groups with surjective maps (L_0 = 1); a
  computable subgroup is a closed subgroup whose images U_n ⊆ L_n are uniformly decidable; the Hausdorff dimension is
  the Barnea–Shalev lower limit liminf_n log|U_n| / log|L_n| for the given system.
- **Settled.** Theorem 1.1(a) / Lemma 2.2: the dimension of a computable (or Π⁰₁) closed subgroup, with respect to the
  given system or to any computable filtration, is left-Σ₂. Theorem 1.1(b): for every prime p and every left-Σ₂ real
  r ∈ [0, 1] there is a computable set A such that the elementary abelian subgroup U_A of power series supported in
  A is a computable closed subgroup of the 2-generated pro-p lamplighter group W = Z_p ⋉ F_p[[t]] with dimension r
  simultaneously for the wreath presentation (W/K_k ≅ C_p ≀ C_{p^k}, with the trivial group L_0 prepended), the
  p-power series, the iterated p-power series, the Frattini series and the dimension subgroup series, and r/2 for the
  lower p-series. Corollary 1.2: the answer to the question (also with respect to the p-power series, Nies's natural
  inverse system, for finitely generated pro-p groups whose p-power series is computable — for instance groups given
  by this series as their inverse system — and likewise for P*, F, D). Theorem 1.3: the dimensions of the computable
  (or Π⁰₁) closed subgroups of W with respect to the lower p-series are exactly the left-Σ₂ reals in [0, 1/2], the
  numbers 1/2 + m/(2pⁿ) with 0 < m < pⁿ, and 1 (all primes p).
- **Reading caveat (in the abstract and in Corollary 1.2).** If "computable subgroup" meant "closed subgroup generated
  by finitely many computable elements", the question would become an effective version of the problem of finitely
  generated Hausdorff spectra; this is not addressed.
- **Credit.** The question and the statement without finite generation are from Nies's section of the 2025 list; the
  list gives that statement without proof. It follows from the Barnea–Shalev formula, the example C₂^ω of
  Mayordomo–Nies (their Example 4.2, which they attribute essentially to Barnea–Shalev, Lemma 4.1) and the theorem of
  Downey–Jockusch–Schupp that the lower densities of computable sets are exactly the left-Σ₂ reals (their Theorem 5.1,
  (i) ⟺ (iii), numbering of arXiv:1307.0040v1). The Hausdorff spectra of W are classical: [0, 1] for P, D, F (Klopsch
  1999, as recalled by de las Heras–Klopsch 2022); the set above without effectivity for the lower p-series
  (Klopsch–Thillaisundaram 2019, Corollary 2.11). The subgroups U_A are the coordinate subgroups of
  Klopsch–Thillaisundaram 2019, Lemma 2.3. Lemma 3.1 (left-Σ₂ reals are the lower limits of computable rational
  sequences) is Downey–Jockusch–Schupp 2013, Theorem 5.1 ((ii) ⟺ (iii)).
- **What the note adds.** The steering lemma (Lemma 3.2: one computable set with lower limit r of its densities along
  every increasing sequence of bounded ratio; a variant of Downey–Jockusch–Schupp, Lemma 5.3 — which prescribes the
  lower and the upper density — with holds of growing multiplicative length), which makes one subgroup work for
  several filtrations at once; the effective realisation in one finitely generated group; and the computable
  lower-p-series spectrum of W (Theorem 1.3; Step 2 of its proof follows the proof of Klopsch–Thillaisundaram 2019,
  Theorem 2.10). This is a straightforward effective version of known constructions; the novelty is modest and no
  priority is claimed.
- **Not settled.** The effective finitely generated reading (above); the set of values for the lower p-series over
  all finitely generated computable pro-p groups; groups whose standard series are not computable.

The note is unrefereed. Under the v1.8.0 policy of the dataset (solved only if peer-reviewed), the record keeps its
status, with an unrefereed-claim note pointing to this note.

## Statement checked
- **Primary source.** G. Barmpalias, N. Bazhenov, C. T. Chong, W. Dai, S. Gao, J. L. Goh, J. He, K. M. S. Ng, A. Nies,
  T. Slaman, R. Thornton, W. Wang, J. Yu, L. Yu, "Open Problems in Computability Theory and Descriptive Set Theory",
  arXiv:2507.03972 (v1, 2025-07-05; the list is dated June 2025, Tianyuan workshop). LaTeX source
  `Problem_List_arXiv.tex` (710 lines), section "Andre Nies", subsection "Profinite groups", lines 364–368: the
  displayed statement, then a `problem` environment with the question. The `problem` environment shares the global
  `theorem` counter (`\newtheorem{problem}[theorem]{Problem}`); before line 366 there are 12 problems, 2 theorems and
  1 proposition, so the question is **printed as Problem 16** and is the **13th problem environment** of the file.
  No definitions, no proof, no reference and no attribution for the displayed statement, no update. Read in the source
  by all three runs and when the note was written.
- **2026 list.** arXiv:2608.26628v2, "Open Problems in Mathematical Logic" (G. Barmpalias, S. Gao, J. He, T. Kihara,
  A. Nies, T. Slaman, C.-M. Tran, D. Turetsky, P. Welch, L. Yu, H. Zhang), LaTeX source `ProblemList20260901.tex`:
  the first `\end{document}` is at line 1307; the text of the record occurs at lines 1743–1746, inside a copy of the
  2025 list placed after it (second `\end{document}` at line 2090), so it is not part of the compiled 2026 document.
  The compiled 2026 Nies section contains no Hausdorff-dimension problem.
- **Corpus record.** ulamai/UnsolvedMath v1.8.0 (snapshot d371ee9), record AMR-150-0035, status `open`, title
  "Open Problems in Mathematical Logic — Problem 35" (a running number of the extraction), source arXiv:2608.26628;
  the statement is the displayed sentence and the question, verbatim.
- **Conventions.** Mayordomo–Nies, arXiv:2502.09995v3 (source, Section 4: inverse systems of epimorphisms with L_0
  trivial, ultrametric 1/|L_n|, Theorem 4.1 = the Barnea–Shalev formula, reproved from the tree structure, Example 4.2
  = C₂^ω and densities, "essentially [Barnea–Shalev], Lemma 4.1"; no computability statement about dimensions);
  journal version Proc. Amer. Math. Soc. (online 2026-06-12, doi:10.1090/proc/17729; Crossref record only). Nies,
  slides "Profinite groups and computability theory", Tianyuan 2025: slide 11 (computable profinite groups, Smith
  1981, La Roche 1981), slide 18 (the inverse system is arbitrary in general), slide 19 (the natural inverse system
  G/G^{pⁿ} of a topologically finitely generated pro-p group), slide 22 (the C₂^ω example, "Barnea-Shalev 1997,
  essentially"). The left-Σ₂ sentence is not on the slides.

## Readings
| Reading | Answer | Where |
|---|---|---|
| dimension with respect to the given computable inverse system (Mayordomo–Nies) | exactly the left-Σ₂ reals in [0, 1] | Corollary 1.2 |
| dimension with respect to the p-power series (Nies's natural inverse system), for finitely generated pro-p groups whose p-power series is computable (for instance groups given by it) | the same set | Corollary 1.2 |
| the same for the iterated p-power, Frattini or dimension subgroup series | the same set | Corollary 1.2 |
| lower p-series, the group W | left-Σ₂ reals in [0, 1/2], 1/2 + m/(2pⁿ) (0 < m < pⁿ), 1 | Theorem 1.3 |
| lower p-series, all finitely generated groups | not determined | Section 1.2 |
| canonical index filtration (intersection of the open normal subgroups of index ≤ p^j), the group W | U_A has dimension r/2, as for the lower p-series | Remark 5.4 |
| Π⁰₁ closed subgroups instead of computable ones | the same sets | Theorem 1.1(a), Theorem 1.3 |
| "computable subgroup" = closed subgroup generated by finitely many computable elements | values are left-Σ₂; which ones occur is not addressed (effective finitely generated spectrum problem) | Remark 5.5 |
| normal subgroups | not asked; the normal spectra of W are {0, 1} and {0, 1/2, 1} | Remark 5.5 |
| computable finitely generated pro-p groups whose standard series are not computable | not treated | Scope and priority |

## Results in the paper
- Lemma 2.2 (upper bound): for a computable filtration (Definition 2.1) and a computable or Π⁰₁ closed subgroup,
  q < dim ⟺ ∃ε ∃N ∀i ≥ N: |U S_i : S_i|^d ≥ |G : S_i|^c (q + ε = c/d), a Σ⁰₂ condition.
- Lemma 3.1: Downey–Jockusch–Schupp 2013, Theorem 5.1 ((ii) ⟺ (iii)); the rationals may be taken in [0, 1].
- Lemma 3.2 (steering): clipped targets q'_k ∈ (0, 1); a density profile ρ with the unit-increment property (3), moving
  at maximal speed to q'_k and then holding it on [M_k, N_{k+1}] with N_{k+1} = (k + 2)M_k; A = {n : ⌊g(n+1)⌋ > ⌊g(n)⌋},
  g(n) = nρ(n); |A ∩ [0, m)| = ⌊mρ(m)⌋; every sequence with ratio ≤ C meets each hold with k ≥ C.
- Lemma 4.1: the product rule (7), powers (8), commutators (9), S(a, b) normal of index p^{a+b} when p^a ≥ b; the wreath
  presentation L_0 = 1, L_{k+1} = W_k = W/S(k, p^k) ≅ C_p ≀ C_{p^k}.
- Proposition 4.2: P_i = S(i−1, i−1), π_i = π*_i = S(i, p^i − 1), Φ_i = S(i, (p^i − 1)/(p − 1)),
  D_i = S(⌈log_p i⌉, i − 1); all six filtrations are computable (n(i) = k + 1 with k = max(a_i, e(b_i)), e(c) the least
  e ≥ 0 with p^e ≥ c).
- Lemma 4.3: log_p|U_A S(a, b) : S(a, b)| = |A ∩ [0, b)| (12), hence (13); the coset criterion, so U_A is computable.
- Theorem 5.1: for (a_i, b_i) with a_i ≥ 0, b_i ≥ 1, p^{a_i} ≥ b_i, (a_i) non-decreasing and unbounded, (b_i) strictly
  increasing of bounded ratio and a_i/b_i → 0, dim(U_A) = r; for a_i = b_i, r/2. Proofs of Theorem 1.1 and Corollary 1.2.
- Remarks: 5.2 (the statement without finite generation, C₂^ω); 5.3 (a computable set with lower density 7/16 for
  which dim^D(U_A) = 7/16 but dim^P(U_A) = 1/2, p = 3: the steering is needed); 5.4 (the index filtration:
  I_j = S(j, β_j), dimension r/2); 5.5 (other readings; finitely generated spectra; normal spectra).
- Section 6: proof of Theorem 1.3 (Step 1: closed subgroups of the base group, jump sets; Step 2: K = ⟨h⟩(K ∩ B),
  h = x^{pⁿ}z, K ∩ B an F_p[[t^{pⁿ}]]-module, log_p|K P_i : P_i| = (i − 1 − n) + |J ∩ [0, i − 1)|, using that
  h^{p^{i−1−n}} ∈ P_i and P_i is closed; Step 3: realisation by U_A with 2r, and by K_{n,m} = ⟨x^{pⁿ}⟩U_{A(n,m)};
  Step 4).

## Computations (programs and outputs in reproducibility/)
- `check_note.py` (standard library, exact arithmetic; 97 checks, 0 failed, about 28 seconds): the group law and
  (6)–(9) in W_k for nine pairs (p, k), the maps W_k → W_j and generation; Lemma 4.1(c) with non-normality for
  p^a < b as a control, and the five standard series computed from their definitions, for twelve pairs (p, k), p ≤ 7,
  up to |W_k| = 2^37, 3^30, 5^27, 7^51: all 551 terms agree with Proposition 4.2, with a brute-force cross-check on
  three groups and wrong formulas detected; (12) in 5,900 comparisons (the (1+t)^j-coordinates violate it 87 times);
  the coset criterion on 120,114 cosets; Step 2 of the proof of Theorem 1.3 in 765 comparisons on 360 random
  subgroups, and J + pⁿ ⊆ J; the subgroups K_{n,m} (31 cases); the integer inequalities of the proofs; Lemma 3.2 on
  six rational sequences up to 2·10⁴ (including the hits of the holds by the index sequences); Remark 5.3; Remark 5.4
  on W_2, W_3 (p = 2) and W_1 (p = 3) by brute force.
- `original/` (the three programs of the first version, standard library; 16.0 s, 1.6 s, 3.1 s, about 20 s in
  total): the series in W_k for six pairs (104 steps, all MATCH), the count of Theorem 1.3 (116 comparisons), the
  steering construction (five sequences, 10⁵). Re-run when the note was written and by the third run: outputs
  identical to the recorded ones apart from a trailing `EXIT 0` line written by the shell.
- `verification_run_A/`, `verification_run_B/`, `independent_run_2/`: the programs of the three runs, with their
  recorded outputs (see below).
- These are TESTED data on finite cases; no theorem depends on them.

## Independent verification runs
All three runs were AI-assisted, re-derived the proofs and wrote their own programs. Runs A and B examined the first
written version of the results, and neither read the other's report; the third run examined the note as written.

**Run A (statement and proofs).** Compared the record with the LaTeX sources of both lists (problem numbering, the
text after `\end{document}` in the 2026 list), the conventions with Mayordomo–Nies v3 and Nies's slides (slides 11,
12, 18, 19, 22, 27, 28), and re-derived every proof line by line: the window construction then used for Lemma 3.1
(claims A–C), Lemma 3.2, Lemma 4.1 and Proposition 4.2 (all inequalities, for all p including p = 2), Lemma 4.3, the
upper bound for computable and Π⁰₁ subgroups, Theorems 5.1/1.1 and Corollary 1.2, Theorem 1.3. Own programs: the
series of W_k for six pairs (p, k) from a different group encoding and closure routine (217 recursion steps), the
count of Theorem 1.3 on 501 instances with non-monomial generators and twists, the steering construction up to 10⁵
with adversarial bounded-ratio sequences. Verdict: no mathematical error; five fixes.

**Run B (independent computation, literature, bibliography).** A different model of W_k (the wreath product with the
shift action) and exact linear algebra: the five series computed from W_k for fourteen pairs (p, k), p ≤ 7, 1,608
terms (brute-force cross-check on three groups; D by two recursions); (12) in 11,860 comparisons with a negative
control; the count of Theorem 1.3 in 1,594 comparisons on 796 random subgroups; the steering construction by
step-by-step simulation (2·10⁵) and in closed form (about 10⁷⁰), with negative controls (an unbounded-ratio sequence
has a different lower limit); the window construction on five Σ₂ definitions; a naive computable set with different
dimensions along D and P (so the steering is needed); the index filtration by brute force (p = 2, j ≤ 5; p = 3, j ≤ 3;
p = 5, j ≤ 2). It re-ran the three programs of the first version from a copy (identical outputs), repeated the
literature search (arXiv, Semantic Scholar, OpenAlex, zbMATH Open, Crossref, Nies's home page with talks and the Logic
Blog 2025–2026, two web searches) and checked the bibliography against Crossref. Verdict: no mathematical error; six
fixes.

**Corrections required by runs A and B**, all applied in the note:
- A1: the question is the 13th `problem` environment of arXiv:2507.03972, printed as Problem 16 (shared counter) —
  Section 1.1 and Scope and priority.
- A2: the wreath inverse system needs L_0 = 1 prepended — Section 4 ("The wreath presentation"): L_0 := 1,
  L_{k+1} := W_k.
- A3: Step 2 of the proof of Theorem 1.3 uses that h^{p^{i−1−n}} lies in P_i and P_i is a closed subgroup.
- A4: the reading caveat (finitely many computable generators) is in the abstract and in Corollary 1.2.
- A5, B2: Klopsch–Thillaisundaram 2019 is cited with the numbering of arXiv v2 (Lemma 2.3, Proposition 2.6,
  Corollary 2.8, Theorem 2.10, Corollary 2.11), and its appendix makes Section 2 valid for p = 2.
- B1: the side remark that it is open whether a finitely generated pro-p group can have uncountable finitely
  generated spectrum was outdated: Fariña-Asategui–Garaialde Ocaña–Uria-Albizuri (arXiv:2504.11948, Trans. Amer.
  Math. Soc. 2026) show that the closure of the first Grigorchuk group has finitely generated spectrum [0, 1] for the
  2-central lower series and the dimension subgroup series, answering a question of de las Heras and
  Thillaisundaram; Fariña-Asategui–Merladet Urigüen (arXiv:2601.16869) give further pro-2 examples — Remark 5.5.
- B3: running times corrected (about 20 seconds in total for the three programs of the first version).
- B4: bibliography: Mayordomo–Nies, Proc. Amer. Math. Soc. 2026, doi:10.1090/proc/17729; de las Heras–
  Thillaisundaram, J. Algebra 606 (2022) 266–297; de las Heras–Klopsch–Thillaisundaram, J. London Math. Soc. 112(2)
  (2025) e70271, doi:10.1112/jlms.70271; Barnea–Shalev pages 5073–5091; Downey–Jockusch–Schupp article 1350005;
  Koh–Melnikov–Ng, J. Symb. Log. 90 (2025) 188–220 (all checked with Crossref).
- B5: Theorem 5.1 states p^{a_i} ≥ b_i and a_i → ∞ (with (a_i) non-decreasing).
- B6: the novelty paragraph names Klopsch–Thillaisundaram 2019 Lemma 2.3 / Corollary 2.11, Klopsch 1999 and
  Downey–Jockusch–Schupp 2013 as the results made effective; the index filtration is Remark 5.4.

**Changes made when the note was written** (not examined by runs A and B; examined first by the third run): the
notion of a computable filtration (Definition 2.1) and the restriction of the p-power reading in Corollary 1.2 to
groups whose p-power series is computable (the upper bound needs it); the proof of Lemma 3.1 of the first version
(the window construction, checked by runs A and B) replaced by the reference to Downey–Jockusch–Schupp, Theorem 5.1;
the comparison with their Lemma 5.3; the example of Remark 5.3 (a different set from the one of run B: gaps
[4·9^m, 8·9^m), p = 3, dimensions 7/16 and 1/2); the proof in Remark 5.4 (shape of the open normal subgroups of W,
I_j = S(j, β_j)); the program `check_note.py`, which re-checks the finite parts of these additions as well.

**Third run (the note as written).** It examined the note line by line as if nothing had been checked, and the
additions above first. It read again the LaTeX sources of arXiv:2507.03972v1, arXiv:2608.26628v2, Mayordomo–Nies
arXiv:2502.09995v3, Klopsch–Thillaisundaram arXiv:1812.02322v2, de las Heras–Klopsch arXiv:2004.02846v2 and
Downey–Jockusch–Schupp arXiv:1307.0040v1 (with the printed PDF of that version, for its numbering), Nies's 2025 slides
and the Crossref records of all twelve DOIs of the bibliography. It re-derived every proof: Definition 2.1 and the
restriction of Corollary 1.2 (needed for the proof as given, correctly stated, and true for W: n(i) = k + 1 with
k = max(a_i, e(b_i))); Lemma 2.2; Lemma 3.1 against Theorem 5.1 of Downey–Jockusch–Schupp (exactly (ii) ⟺ (iii));
Lemma 3.2; Section 4 and Proposition 4.2; Lemma 4.3; Theorem 5.1 and its hypotheses; Theorem 1.3; Remark 5.3 (lower
density 7/16 attained along 8·9^m, δ_A(9^m − 1) = 1/2, δ_A(3·9^m − 1) → 5/6, hence dim^D = 7/16 and dim^P = 1/2);
Remark 5.4 (N = ⟨x^{p^a}z⟩B_b with p^a ≥ b, z ∈ B_{b−1}, index p^{a+b}; I_j = S(j, β_j); dimension r/2). Own programs
(`independent_run_2/`, standard library, written before reading `check_note.py`): the product rule (7) against the
wreath product with the shift action; (6)–(11) and Lemma 4.1(c) on random elements; the five standard series of W_k
from their definitions for fourteen pairs (p, k) with p ≤ 13 (635 terms; D also by Lazard's formula; brute force on
sets for three groups); (12) in 4,496 comparisons (control: 1,460 violations in the (1+t)^j-coordinates) and Lemma
4.3(c) by brute force on 2,400 cosets; Step 2 of Theorem 1.3 in 832 comparisons on 420 random subgroups and the 63
subgroups K_{n,m}; all normal subgroups of index ≤ p^j of W/S(j, j) for p = 2, 3, 5, 7 and j ≤ 6, 4, 3, 2 (their
numbers agree with those of run B where both exist), which confirm Remark 5.4; Lemma 3.2 by simulation as printed
(six sequences, 2·10⁵) and in closed form (36 phases, up to about 10⁵⁶), with the hits of the holds by the index
sequences of K, P, F for p = 2, 3, 5, 7 and the quotients of (13) for K, P, F, D, L and the index filtration; Remark
5.3 (direct counting up to 9⁶, exact values for m < 40); the integer facts (p ≤ 13). All 147 checks passed. It
re-ran the whole package from an extracted copy of the archive: every recorded output was reproduced up to timing
lines (`check_note.py`; the three programs of the first version; the recorded runs of runs A and B, among them
`series_check.py 5 3`, 590 s), and `ua_dims.py` of run B, whose seeds were not recorded, gave the same results with
seed 1 for its seven pairs (p, k). It repeated the literature search (arXiv API, OpenAlex, zbMATH Open, Crossref, one
web search). Verdict: no error in the theorems; thirteen required fixes, all applied:
- the statement without finite generation is credited as in the sources (Nies's section of the list, without proof;
  it rests on the example of Mayordomo and Nies, essentially Barnea–Shalev's, and on Downey–Jockusch–Schupp), instead
  of "due to Mayordomo and Nies" — abstract, Sections 1.1 and 1.3, Remark 5.2, Scope and priority, this report;
- Downey–Jockusch–Schupp are cited by their Theorem 5.1 (the arXiv version prints two statements numbered 1.4), and the
  bibliography says that the numbering is that of arXiv version 1;
- Lemma 3.2 is called a variant of Downey–Jockusch–Schupp, Lemma 5.3 (which also prescribes the upper density), not a
  strengthening;
- the attribution of the C₂^ω example essentially to Barnea–Shalev, Lemma 4.1, as in Mayordomo–Nies, is added;
- Section 7 describes `check_note.py` correctly (nine pairs for (6)–(9), twelve for Lemma 4.1(c) and the series;
  765 comparisons on 360 random subgroups), and the Verification paragraph and this report describe run B correctly
  (1,594 comparisons on 796 random subgroups);
- Remark 5.4: v and e defined before use, the step x^{p^j} ∈ N justified, a separate bound variable in β_j;
- Theorem 5.1 states b_i ≥ 1; the computability sentence after Proposition 4.2 uses e(b_i) (defined also for b_i = 0);
- Lemma 2.2: "integers c and d ≥ 1";
- Klopsch 1999's [0, 1] for P, D, F is "as recalled in de las Heras–Klopsch 2022";
- the Verification and Scope paragraphs describe the third run and count four web searches; Corollary 1.2 mentions
  groups given by the series as their inverse system;
- package: the local interpreter path in the shell timing lines of ten recorded outputs of run B was replaced by
  `python` (README); `independent_run_2/` added; README, archive, Zenodo files and hashes updated.

## Relation to the literature, novelty and scope
- **Searched** (all requests anonymous and logged): the LaTeX sources of both lists; Mayordomo–Nies (arXiv v1–v3;
  Crossref record of the journal version); citing works (none in OpenAlex for Mayordomo–Nies and the 2025 list, none
  in Semantic Scholar for the two lists; Semantic Scholar refused the query for Mayordomo–Nies); Nies's Logic Blogs
  2023–2024 (arXiv:2503.12673) and 2025–2026; Nies's slides of December 2024, August 2025, May 2026 and June 2026;
  abstracts of Nies's arXiv papers of 2025–2026; the literature on Hausdorff spectra (arXiv searches "Hausdorff
  spectrum/spectra", "Hausdorff dimension" with "profinite" and "computable"; zbMATH Open), including
  Klopsch–Thillaisundaram 2019, de las Heras–Klopsch 2022, de las Heras–Thillaisundaram 2022 (two papers), de las
  Heras–Klopsch–Thillaisundaram 2025, Fariña-Asategui–Garaialde Ocaña–Uria-Albizuri 2025/2026, Fariña-Asategui–
  Merladet Urigüen 2026, Barnea–Vannacci 2018, de las Heras 2020; work on computable profinite and topological groups
  (Smith 1981, La Roche 1981, Koh–Melnikov–Ng 2025, zbMATH "computable profinite"); four web searches in total; on 17
  and 18 October 2026. The third run repeated the arXiv searches (also by author: Nies, Mayordomo), the OpenAlex
  citation counts, two zbMATH Open searches and one web search on 18 October 2026 (nothing new).
- **Found:** no printed statement of the answer, in print or in talks. A search that finds nothing is not a proof of
  novelty. The constructions made effective are classical (see Credit).
- **What was read:** the sources of both lists, of Mayordomo–Nies v3, Klopsch–Thillaisundaram 2019 (arXiv v2), de las
  Heras–Klopsch 2022 (arXiv v2), Downey–Jockusch–Schupp 2013 (arXiv v1) and of the Logic Blog 2023–2024, in the parts
  used; Nies's 2025 slides; the abstracts of the other spectrum papers. Barnea–Shalev 1997, Klopsch's thesis, Smith
  1981 and La Roche 1981 were not read (statements taken from Mayordomo–Nies, Klopsch–Thillaisundaram, de las
  Heras–Klopsch and Nies's slides). The journal versions were not compared (numbering of Mayordomo–Nies,
  Klopsch–Thillaisundaram and Downey–Jockusch–Schupp as in the arXiv versions). The proofs of cited theorems were not
  checked.
- **Suggested label for the dataset:** AMR-150-0035 solved (exactly the left-Σ₂ reals in [0, 1]: finite generation
  imposes no restriction, under the Mayordomo–Nies conventions), with the reading caveat (if "computable subgroup"
  meant a closed subgroup generated by finitely many computable elements, the question would become the open effective
  finitely generated spectrum problem) and the remark that the note is unrefereed (under the v1.8.0 policy: status
  unchanged, unrefereed-claim note).

## Public release and license
The note, its source files, this report and the reproducibility package are released under CC BY 4.0
(`LICENSE.txt`). The package contains `check_note.py` with its recorded output, the three programs of the first
version and the programs of the three verification runs, with their recorded outputs. The note is an unrefereed
preprint.