# Verification report — OWR-14298580-008 (Alfieri–Binns, strong geography restriction for HF⁻)

Verification date: 2026-09-30 (revised the same day after a second independent verification run).

**Verdict.** The answer is no. For the Brieskorn sphere Y = Σ(30,47,83), with either orientation,
HF⁻_red(±Y) ≅ HF⁺_red(±Y) ≅ T(16) ⊕ T(14)^10 ⊕ T(13)^16 ⊕ T(12)^24 ⊕ T(11)^36 ⊕ T(10)^46 ⊕ T(9)^56 ⊕ T(8)^66 ⊕
T(7)^76 ⊕ T(6)^82 ⊕ T(5)^84 ⊕ T(4)^86 ⊕ T(3)^88 ⊕ T(2)^90 ⊕ T(1)^92, where T(k) = F[U]/U^k and F = Z/2. So ℓ = 16,
but F[U]/U^15 is not a direct summand of HF⁻(±Y), graded or not, and the strong geography restriction fails.
Y is an irreducible integral homology sphere (Hatcher's notes, Proposition 1.13; or directly: since
1/30 + 1/47 + 1/83 < 1 and the Euler number is non-zero, Y has the geometry of the universal cover of SL₂(R), so its
universal cover is R³), not an L-space, and satisfies Lin's weaker restriction. The proof is computer-assisted: it
uses published theorems of Ozsváth–Szabó and Némethi and an exact finite computation, for which the paper prints a
certificate (1707 turning points of τ). The note is unrefereed.

## Statement checked
- **Primary source.** A. Alfieri, "Is the geography of Heegaard Floer homology restricted or is the L-space
  conjecture false?", Oberwolfach Reports 21 (2024), no. 3, 1951–1953 (Report 34/2024, Topologie, 21–26 July 2024),
  doi:10.4171/OWR/2024/34. The PDF was read.
  - The definition of the strong geography restriction is on p. 1952 and the question on p. 1953.
  - The question: "Does HF⁻(Y) satisfy the strong geography restriction for every rational homology sphere Y?"
- **Same question.** A. Alfieri, F. Binns, arXiv:2404.00490 (version 1 of March 30, 2024, the only version on
  arXiv as of 2026-09-30), Question 1.10. The LaTeX source was read and compiled.
  - Definition 1.6: an F[U]-module M satisfies the strong geography restriction if it contains a direct summand
    F[U]/U^ℓ ⊕ F[U]/U^{ℓ−1} ⊕ ⋯ ⊕ F[U]/U, where ℓ = min{ℓ ≥ 0 : U^ℓ M_red = 0}.
  - Conventions (Section 2.1): F = Z/2; HF⁻(Y) is a finitely generated F[U]-module; HF⁺ = (copies of T⁺) ⊕ HF⁺_red
    with HF⁺_red ≅ Tor(HF⁻) (Remark 2.2).
  - Context: Theorem 1.7 (surgery on a knot in S³), Theorem 1.8 (large surgery on a link), Remark 1.9
    (null-homologous knots and links in L-spaces), Proposition 1.12, Definition 3.6 ("large").
  - Both sources remark that removing "large" from Theorem 1.8 would give a positive answer.
- **Corpus record.** ulamai/UnsolvedMath, OWR-14298580-008 (status `open`). The `original` field is a
  table-of-contents fragment that runs into the next abstract; the clean statement matches the source.

## Readings
| Reading | Refuted? | Witness |
|---|---|---|
| SGR for HF⁻(Y), every rational homology sphere Y (A–B Question 1.10; OWR p. 1953) | yes | ±Σ(30,47,83): ℓ = 16, no F[U]/U^15 summand |
| the same for integral homology spheres, for irreducible manifolds, or for non-L-spaces | yes | the same |
| the same with HF⁺ (or HF⁺_red) in place of HF⁻ | yes | the same (Lemma 2.3: the multiplicities agree) |
| "direct summand" read as graded or as ungraded summand | yes | there is not even an ungraded summand F[U]/U^15 |
| SGR for all integral surgeries on links in S³ ("large" removed from A–B Thm 1.8) | yes | ±Y, integral surgery on its plumbing link |
| Lin geography restriction (A–B Conjecture 1.5) | not addressed | Y has 92 summands F[U]/U |

## Results in the paper
- **Lemmas 2.1–2.4.** An invariant m_k(M) = dim(ker U ∩ U^{k−1}M) − dim(ker U ∩ U^k M) counts summands F[U]/U^k; a
  summand F[U]/U^k forces m_k ≥ 1. For a rational homology sphere, HF⁻(Y,s) ≅ F[U] ⊕ Tor HF⁻(Y,s) (the free part has
  rank one because F[U,U⁻¹] is flat over F[U], so HF⁻ ⊗ F[U,U⁻¹] ≅ HF^∞ ≅ F[U,U⁻¹]), m_k(HF⁺) = m_k(HF⁻) =
  m_k(Tor HF⁻), and m_k(HF⁻(−Y)) = m_k(HF⁻(Y)) (Ozsváth–Szabó duality, which identifies CF⁺(−Y) degree by degree with
  the graded dual ⊕_d Hom_F(CF⁻_d(Y), F)).
- **Theorem 3.1** (Ozsváth–Szabó, Geom. Topol. 7 (2003), Theorem 1.2; Némethi, Geom. Topol. 9 (2005), Theorem 8.3,
  Proposition 4.7, Theorem 9.3, Sections 11.12–11.13; also Can–Karakurt, Theorem 2.3 of arXiv:1211.4934v2):
  HF⁺(−Σ(a_1,…,a_n)) ≅ ℍ(R_τ) up to a grading shift, with τ(i+1) − τ(i) = 1 − e0·i − Σ⌈iω_l/a_l⌉. The graded-root
  module decomposes by Némethi's Proposition 3.5.2; the passage from Z to F = Z/2 uses the universal coefficient
  theorem.
- **Lemma 3.2.** The summand lengths are n_t(b,d) = N_{d−1}(b) − N_d(b), where N_q(b) counts the components of
  {t ≤ q} with minimum b (the elder rule). **Lemma 3.3.** They can be computed from the turning points.
- **Lemma 3.4.** Δ(i) + Δ(N0 − i) = 0 for all i, Δ ≥ 0 beyond N0 = (n−2)A − ΣA/a_l, and τ(N0+1−i) = τ(i); for n = 3
  this is contained in Can–Karakurt, Theorem 1.3.
- **Proposition 4.1** (exact computation) and **Theorem 1.3** (main result) for Σ(30,47,83): N0 = 109229, min τ =
  −12755 on four plateaus, 1707 turning points, 853 summands, total rank 4864, no length 15, d(Y) = 0.
- **Table 1 and Remark 4.2.** The 27 summands of length ≥ 13, with the elder rule and ties between equal minima broken
  in favour of the smaller index; this convention fixes the index column (54720 for T(16)), while the lengths do not
  depend on it.
- **Corollary 1.5** (unconditional): "large" cannot be removed from A–B Theorem 1.8.
- **Corollary 1.6** (conditional on A–B Theorems 1.7, 1.8 and Remark 1.9, an unrefereed preprint): ±Y is not surgery
  on a knot in S³, not surgery on a null-homologous knot in an L-space, and not large surgery on a link. No novelty
  claimed.
- **Proposition 1.7** (computer search, two independent programs): among Σ(a_1,…,a_n), the counterexamples of
  smallest product are Σ(30,47,83), Σ(2,15,47,83), Σ(3,10,47,83), Σ(5,6,47,83) (product 117030); for n = 3 and
  A ≤ 200000 only Σ(30,47,83); for n = 4 and A ≤ 600000 exactly 12; none for n = 5 (A ≤ 250000), n = 6 (≤ 130000),
  n = 7 (≤ 600000). No per-sphere certificates.
- **Remark 5.1** (observed, not proved): the family qr − pq − pr = 1 has 47 failures among 346 computed members.

## Computations (exact; scripts and outputs in reproducibility/)
- **Certificate and checker** (`verifier/`, standard library only). The 1707-point certificate
  (SHA-256 6d7130dbc0ecf948286ed5d2b7e51a2cdad322da0588a97f3c9ddf7a43f72943) is printed in Appendix A.
  - `check_certificate.py` recomputes τ, validates the certificate and computes the lengths from the 1707 values by
    the rank formula, without the elder rule: T(16) + T(14)^10 + … + T(1)^92, ℓ = 16, missing [15].
  - `make_certificate.py` regenerates the certificate; it is byte-identical to the finder's file.
- **Second implementation** (`verifier/`, written for the paper, separately from the finder's code).
  - `pipeline_check.py`: τ from the generalized Laufer sequence on the 32-vertex lattice equals the closed formula
    and the Can–Karakurt semigroup form on [0, N0+1]; Némethi's explicit cycles agree at 110 samples; K² + s =
    −102040, d = 0; union-find and a stack algorithm agree (853 bars, rank 4864); Brieskorn's signature σ = −38912,
    σ/8 = −4864 = −rank − d/2 (Casson invariant).
  - `scan2.c` (union-find on streamed turning points): n = 3, A ≤ 200000: 423020 spheres, 1 failure; n = 4,
    A ≤ 600000: 401831 spheres, 12 failures; n = 5, A ≤ 250000: 9556, 0; n = 6, A ≤ 130000: 46, 0; n = 7,
    A ≤ 600000: 2, 0. These equal the finder's counts, and all 13 decompositions are identical.
  - `crossval_scan2_python.py`: scan2 against pipeline_check.py on 400 random tuples, 0 mismatches.
  - `surgery_check.py`: the 102308 spheres Σ(p,q,pqn−1) with pq(pqn−1) ≤ 10⁶ (1/n-surgeries on torus knots) agree
    exactly with the rational surgery formula T(V_0)^(n−1) ⊕ ⊕_{k≥1} T(V_k)^(2n); longest summand 125.
  - `family_check.py`: 346 family members with p ≤ 230, 47 failures (45 even p, 2 odd p).
- **Finder** (`claimant/`).
  - τ three ways (closed formula, Hilbert series, Laufer lattice) and two barcode algorithms for the examples.
  - Full-lattice brute force (no reduction theorem) agrees with the τ-method on 15 small Seifert spheres.
  - Casson invariant by Dedekind sums (and Brieskorn's formula for n = 3) agrees with −(rank + d/2) for the 7 main
    examples and 551 small spheres.
  - Known results reproduced: Σ(2,3,6k±1); the F[U]/U² summand of Σ(2,2n+1,4n+3) (Rustamov, cited by A–B);
    1588 torus-knot surgeries satisfy the restriction, as A–B Theorem 1.7 predicts.
  - The first search program (barrier algorithm) produced Proposition 1.7.

## Independent verification runs
Two independent verification runs, both AI-assisted and both with their own code, checked the record.

### Run 1
An AI-assisted independent verification run (2026-09-30) checked the record against the sources and re-derived
the claims with its own code.

| Item | Verdict |
|---|---|
| Statement fidelity (OWR p. 1952–1953; arXiv v1 Question 1.10, same definition) | CONFIRMED |
| Correctness (Seifert data, plumbing, τ by Laufer's algorithm and closed/semigroup forms, finite range re-proved and checked numerically, barcode by two new methods, Casson invariant) | CONFIRMED (853 bars, rank 4864; exactly one bar of length ≥ 15, and it has length 16) |
| Pipeline check against a different theory (1/n-surgery formula on 265 spheres Σ(p,q,pqn−1), bars up to 20) | CONFIRMED (0 mismatches) |
| Searches (own C scanner: n = 3 up to 200000, n = 4 up to 200000, n = 5, 6, 7) | CONFIRMED (minimal product 117030, exactly four spheres) |
| Other listed examples (8 further four-fibred spheres, family members) | CONFIRMED |
| Answer as posed and as intended | CONFIRMED (negative) |
| Novelty | CONFIRMED as far as can be checked (no priority claim) |

Required fixes and how they were applied:
1. *Include the 1707-point certificate so that the barcode can be checked without the search code; give exact
   theorem numbers.* Appendix A prints the certificate with its checksum and describes the check; the standalone
   checker is `verifier/check_certificate.py`. Theorem numbers: Ozsváth–Szabó 2003, Theorem 1.2 (over F: Theorem
   2.1); Némethi 2005, Theorem 8.3, Proposition 4.7, Theorem 9.3, Proposition 3.5.2, Example 3.4(3), Sections
   11.12–11.13; Can–Karakurt, Theorems 1.3 and 2.3 (arXiv:1211.4934v2 numbering).
2. *State the knot-surgery and large-link-surgery consequences as conditional on A–B Theorems 1.7/1.8.* Corollary 1.6
   is stated as conditional; Corollary 1.5 (that "large" cannot be dropped) is separated and unconditional.
3. *The count of 12 four-fibred counterexamples up to product 600000 rested on one implementation.* It was re-run
   with a second, separately written program (`verifier/scan2.c`, different barcode algorithm): same 401831
   spheres, same 12 failures, identical decompositions. Proposition 1.7 is still labelled a computer-search result.
4. *Optional: the 1/n-surgery validation.* Included, extended to 102308 spheres (0 mismatches), together with the
   265-sphere check of the verification run.
5. *(For the dataset record, not the paper:)* the corpus status and literature assessment should be updated when the
   note is announced.

### Run 2
A second AI-assisted independent verification run (2026-09-30) reviewed the unrefereed preprint as released (14 pages,
paper sha256 `c8634dc0…b8a8b`, source archive sha256 `f61eae38…23e4`). It fetched the sources anonymously, wrote its own
code before reading the author's scripts, and reran the released archive. Its code and outputs are in
`reproducibility/independent_run_2/`.

| Item | Verdict |
|---|---|
| Statement fidelity (OWR 34/2024 pp. 1952–1953, same PDF checksum as the cached copy; arXiv:2404.00490, only v1, same e-print checksum; Definition 1.6, Question 1.10 and all cited numbers) | CONFIRMED: Σ(30,47,83) is an integral homology sphere, ℓ = 16 and there is no summand F[U]/U^15, graded or not; no misprint or loophole is used |
| Proofs (every cited theorem number checked against the arXiv sources of Ozsváth–Szabó, Némethi and Can–Karakurt; Lemmas 2.1–3.4 and the proofs of Theorem 1.3, Remark 1.4, Corollaries 1.5–1.6 line by line) | CONFIRMED, with four small precision or citation gaps (required fixes 1–4 below) |
| Computations | CONFIRMED, see below |
| Novelty (arXiv API, OpenAlex, Semantic Scholar, zbMATH, Crossref, one web search) | no earlier answer found; the paper's cautious priority wording is appropriate |
| Presentation | good; minor fixes (required fix 5 and optional suggestions) |
| Fatal problems | none |

Computations of run 2, all exact:
- **Σ(30,47,83).** e0 = −1, ω = (29,1,1), N0 = 109229; Δ ∈ {−1,0,1}; τ ∈ [−12755, 1], with the minimum exactly on
  [54390,54420], [54480,54510], [54720,54750], [54810,54840] and barriers of heights 7, 16, 7 between them.
- **τ three ways**, equal on all of [0, 109230]: the closed formula, the semigroup form ⟨3901, 2490, 1410⟩, and χ_K(x(i))
  from its own generalized Laufer sequence on the 32-vertex lattice (plus from-scratch Laufer runs at sample points).
  The plumbing is negative definite (exact LDLᵀ), has determinant 1 and one bad vertex; K² = −102072, s = 32, d = 0.
- **Bars three ways**, identical: (A) union-find with the elder rule on all 109231 indices, (B) the rank function
  N_q(b) from level scans of the compressed list, (C) the explicit graded root, the module ℍ(R) over F₂ and ranks of U^k
  by Gaussian elimination. Result: T(16) ⊕ T(14)^10 ⊕ T(13)^16 ⊕ … ⊕ T(1)^92, 853 summands, rank 4864, ℓ = 16, only 15
  missing. Its list of 1707 turning points equals the certificate and the Appendix A listing; all 27 rows of Table 1
  (index, birth, death) are reproduced.
- **Consistency.** Brieskorn's signature σ = −38912 gives λ = σ/8 = −4864 = −(rank + d/2); the geometric genus from a
  lattice count is p_g = 17619 = −min τ + rank.
- **Published values**, gradings included: HF⁺(−Σ(2,3,5)), HF⁺(−Σ(2,3,7)), HF⁺(−Σ(3,5,7)) (Ozsváth–Szabó 2003, §3.4)
  and HF⁺(−Σ(2,3,11)) (Can–Karakurt, Example 2.4) all match. Rustamov's summands F[U]/U²: Σ(2,7,15) = T(2) ⊕ T(1)^4,
  Σ(2,9,19) = T(2)^3 ⊕ T(1)^4, Σ(2,11,23) = T(3) ⊕ T(2)^4 ⊕ T(1)^4.
- **Different theory.** All 102308 spheres Σ(p,q,pqn−1) with pq(pqn−1) ≤ 10⁶ agree with the 1/n-surgery formula
  T(V_0)^(n−1) ⊕ ⊕_{k≥1} T(V_k)^(2n) (V_k from the Alexander polynomial and from semigroup gaps, which agree on all 1494
  torus knots): 0 mismatches, longest summand 125.
- **Searches, with a third C program** (written separately from `scan.c` and `scan2.c`): n = 3, A ≤ 200000: 423020
  spheres, only Σ(30,47,83) fails; n = 4, A ≤ 600000: 401831 spheres, exactly the 12 of Table 2; n = 5 (A ≤ 250000):
  9556, n = 6 (A ≤ 130000): 46, n = 7 (A ≤ 600000): 2, no failures. All 36 spheres of product 117030 were run: exactly
  the four listed fail (for example Σ(2,3,5,47,83) satisfies the restriction, with T(16) ⊕ T(15)^10 ⊕ T(14)^16 ⊕ …).
  All 22 rows of Table 2 (ℓ, missing lengths, top terms, rank) are reproduced.
- **Remark 5.1.** 346 family members (106 with p even, 240 with p odd), 47 failures (45 and 2), with the same two odd-p
  failures Σ(187,317,456) and Σ(207,257,1064).
- **Rerun of the released archive** from a fresh extraction: `check_certificate.py` (output identical, about 1.3 s of
  CPU time), `make_certificate.py` (byte-identical certificate), `scan2 -v 30,47,83`, `pipeline_check.py`,
  `long_bars.py`, `crossval_scan2_python.py` (400 tuples, 0 mismatches), `surgery_check.py 1000000`, `family_check.py`,
  `scan2 -f further_examples.txt` and the finder's `minimal_check_30_47_83.py` all reproduce the recorded outputs.

Required fixes of run 2 and how they were applied:
1. *Irreducibility needs a reference* (Remark 1.4(a), the proof in §4, the abstract). Remark 1.4(a) and the proof now
   cite Hatcher's notes (Proposition 1.13: a Seifert fibred manifold is irreducible unless it is S¹×S², the twisted
   S²-bundle over S¹ or RP³#RP³). The proof also gives the direct argument: 1/30 + 1/47 + 1/83 < 1 and e ≠ 0, so Y
   has the geometry of the universal cover of SL₂(R) (Scott, Bull. London Math. Soc. 15 (1983),
   doi:10.1112/blms/15.5.401) and universal cover R³, and a manifold with an irreducible covering space is irreducible
   (Hatcher, Proposition 1.6).
2. *Justify the rank-one free part* (Lemma 2.3, Theorem 1.3). Lemma 2.3 now states HF⁻(Y,s) ≅ F[U] ⊕ Tor HF⁻(Y,s) and
   proves it: F[U,U⁻¹] is flat over F[U], so HF^∞ ≅ HF⁻ ⊗ F[U,U⁻¹] ≅ F[U,U⁻¹]^r, and r = 1. The proof of Theorem 1.3
   cites this for both orientations.
3. *Graded dual in Lemma 2.4.* The proof now uses the graded dual ⊕_d Hom_F(CF⁻_d(Y,s), F), says that the
   identification in Ozsváth–Szabó's Proposition 2.5 is made degree by degree, and notes that the full Hom is the
   product over degrees.
4. *Tie-breaking in Table 1 and Remark 4.2.* The caption states the convention (ties between equal minima go to the
   smaller index, which is the elder) and defines the index column; Remark 4.2 says "the one chosen as elder by this
   rule". With this convention all 27 rows, including 54720 for T(16), were recomputed and agree; the lengths do not
   depend on the convention.
5. *Certificate checker.* The comment in `verifier/check_certificate.py` now refers to Lemma 3.4, and the docstring
   says "runs in a few seconds", in agreement with the README and the paper. The checker was rerun: exit 0, output
   identical to `verifier/check_certificate_output.txt` (0.7 s wall time). The source archive and the Zenodo files were
   rebuilt and their checksums updated.

Optional suggestions of run 2: applied were a related-work paragraph (Hanselman–Kutluhan–Lidman 2019;
Bodnár–Plamenevskaya 2021 and Rustamov 2003, as credited by Alfieri–Binns; Karakurt–Lidman 2015; Dai–Manolescu 2019;
all bibliographic data checked on Crossref or the arXiv API), a manual line break in the title, identical keyword
lists in the PDF metadata and the Zenodo metadata (math.GT only), alpha labels in page order ([OS04a] is now the
first Annals paper, pp. 1027–1158), and the precise wording "up to orientation, the Seifert fibred integral homology
spheres other than S³ are the manifolds Σ(a_1,…,a_n)" before Proposition 1.7. Not applied in this revision: a
self-contained proof of the decomposition (2), the remark that a₀ = … = a_ν = 0 for the canonical class, remarks on
coefficient fields, reducible counterexamples, Alfieri–Binns Proposition 1.12, the p_g check in the paper, the
explicit count of 36 spheres of product 117030, taut foliations, and a pointer to the mapping cone. The second run
found none of these necessary for correctness.

## Relation to the literature, novelty and scope
- **Searches (September 2026).** arXiv API (the source; "strong geography", "geography restriction", graded roots,
  lattice homology, Seifert/taut-foliation summand queries, all papers of Alfieri, Binns and Karakurt), Crossref,
  OpenAlex (no citing works found), zbMATH Open (the source listed as a preprint only), Semantic Scholar (two citing
  works: one on Khovanov homology and a 2026 survey mentioning only Lin's F-summand), and three web searches in
  total. None addresses Question 1.10 or reports a counterexample.
- **Related work cited in the revised paper.** Hanselman–Kutluhan–Lidman (geography restrictions of a different
  kind), Bodnár–Plamenevskaya (Lin's restriction for a large class of graph manifolds) and Rustamov (summands F[U]/U² of
  Σ(2,2n+1,4n+3)), both as credited by Alfieri–Binns, and Karakurt–Lidman and Dai–Manolescu (graded roots for Seifert
  homology spheres and almost rational plumbings). None of them addresses Question 1.10.
- **Caveats.** The contents of the K3 problem list (AMS Surveys 295, 2026) were not accessed. Results of A–B used in
  Corollary 1.6 are from an unrefereed preprint. This negative search is not a proof of priority.
- **Scope.** The note answers the question as stated, negatively, with an explicit irreducible integral homology
  sphere. Open: whether infinitely many Brieskorn (or Seifert) spheres fail the restriction, and which non-large
  surgeries on links satisfy it. The Lin geography restriction is untouched.

## Public release and license
This paper, its source files, and this verification report are licensed under the Creative Commons Attribution
4.0 International License (CC BY 4.0): https://creativecommons.org/licenses/by/4.0/