# Verification report — OWR-17135-036 (Santos' question on combinatorial spheres inside spheres on the same vertex set)

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

**Verdict.** Partial result; the question as posed remains open. Proved in the text (without computer assistance):
- if a combinatorial d-sphere S has an edge vw with lk(v) ∩ lk(w) = lk(vw), equivalently an edge lying in no missing
  face with three or more vertices, then (v * ast(v)) ∪ (w * ast(w)) is an extension; this generalises Datta's
  flag-sphere construction;
- if S has no missing d-face and a stacked vertex link, S has an extension;
- reformulations, closure properties, and restrictions on a smallest counterexample in dimension 3.

Computer-certified:
- every combinatorial 3-sphere with 6 ≤ n ≤ 10 vertices has an extension (relative to the published counts of
  3-spheres; the boundary of the 4-simplex, with 5 vertices, has none, since n ≥ d+3 fails);
- a Z_11-invariant and two Z_13-invariant neighborly 3-spheres have extensions but none with a facet cover by two
  vertices;
- six of nine Z_14-invariant examples extend.

These cyclically invariant spheres are not new: they appear in the enumerations of Kühnel–Lassmann (1985) and
Köhler–Lutz (arXiv:math/0506520, Table 4).

Conditional on a solver result: every 4-sphere with 7 ≤ n ≤ 9 vertices has an extension, if the enumerated list of
337 nine-vertex 4-spheres is complete. The completeness of that list rests on solver answers without proof
certificates, and no published count exists to cross-check it. The note is unrefereed.

## Statement checked
- **Primary source.** Oberwolfach Report 39/2019, *Geometric, Algebraic, and Topological Combinatorics*
  (G. Kalai, I. Novik, F. Santos, V. Welker), open problem 9 "Zero point suspensions" (F. Santos, reported by
  J. S. Doolittle), Question 12, pp. 2466–2467, doi:10.4171/OWR/2019/39. The text was read (again in the second
  verification run).
  - Question 12: for a combinatorial d-sphere S with n ≥ d+3 vertices, is there always a combinatorial (d+1)-sphere
    S′ with the same vertex set and S ⊂ S′?
  - Context in the source: the one-point suspension contains S and has one more vertex. A positive answer would
    follow from the (false) statement that some antistar S∖⋆(v) completes to a d-sphere without new vertices.
    The counterexample to that statement is Altshuler's "peculiar" triangulation of the 3-sphere (10 vertices,
    vertex-transitive, neighborly), which nevertheless lies in a 10-vertex 4-sphere.
- **Datta, arXiv:2006.04470v2** restates the question for (d−1)-spheres (his Question 1). He proves it for
  polytopal spheres (after Criado–Santos), joins, a vertex of minimum degree, flag spheres (Thm 4; Remark 14
  identifies his flag-case sphere as a one-point suspension) and stacked spheres (Thm 5). He also asks whether
  every d-ball lies in a d-sphere with the same vertices (Question 2).
- **Corpus record.** ulamai/UnsolvedMath, OWR-17135-036 (upstream status `partially_solved`; statement identical to
  Question 12).

## Readings
| Reading | Status | Where |
|---|---|---|
| Question 12 as posed (all d, all combinatorial d-spheres, n ≥ d+3) | open | — |
| spheres with an LC edge (includes flag spheres, joins, a vertex of degree d+1, stacked spheres, 2-spheres) | yes | Thm 3.1, Lemma 3.2, Cor 3.4 |
| spheres without missing d-faces that have a stacked vertex link | yes | Lemma 4.2 |
| d = 3, 6 ≤ n ≤ 10 | yes (computer-certified, relative to the published counts 1, 2, 5, 39, 1296, 247882 of 3-spheres with 5..10 vertices) | Thm 6.1 |
| d = 4, 7 ≤ n ≤ 9 | yes for all 2 + 8 + 337 listed 4-spheres; the lists are complete for n ≤ 8; for n = 9 conditional on the enumeration, whose completeness is a solver result | Prop 6.3 |
| stronger statement "some antistar completes" | false (A10; already Santos' remark) | Prop 4.3, Cor 6.2 |
| stronger statement "some extension is a one-point suspension" (facet cover by 2 vertices) | false for A11, Z13_0, Z13_1 (DRUP refutations); true for A10 | Thm 6.4 |
| Datta's Question 2 (every d-ball lies in a d-sphere on its vertices) | false; credit Santos' remark; certified instance: antistars of A10 | Remark 4.6 |

## Results in the paper
Names used in the finder's notes → numbering in the paper (the same mapping is in `reproducibility/README.md`).
- **Theorem A → Theorem 3.1.** C_v ∩ C_w = S iff vw is an LC edge; then C_v ∪ C_w is an extension. Its missing-face
  form is **Lemma 3.2**.
- **Remark 3.3.** C_v ∪ C_w = Σ_{w,v}(S/vw) for all v ≠ w. In the flag case this is Datta's sphere (proof of Thm 4(c),
  Remark 14); Datta's argument uses flagness only through ast_S(v) ∩ D_3 = lk_S(v), which is equivalent to the link
  condition for one edge.
- **Corollary A → Corollary 3.4.** Flag spheres, joins, a vertex of degree d+1 (hence stacked spheres), 2-spheres.
- **Proposition B → Proposition 4.1.** Completable antistars ⇔ extensions containing a cone C_v ⇔ a completing ball L.
- **Lemma H → Lemma 4.2**, with **Lemma 2.3** on stacked balls. Part (a) is stated for d ≥ 2; part (b) is due to
  Datta–Singh (JCTA 120 (2013), Lemma 2.1; quoted as Lemma 13 in Datta's preprint); part (c): a 3-ball without
  interior vertices and edges is stacked (counting argument).
- **Proposition 4.3.** If ast_S(v) is completable and every two vertices of lk_S(v) span an edge, then lk_S(v) is
  stacked. Hence a neighborly 3-sphere without stacked links has no completable antistar.
- **Proposition E → Proposition 4.4** (one-point-suspension form). **Proposition D → Proposition 4.5** (ball form).
  **Corollary B → Remark 4.6** (Datta's Question 2, credited to Santos' remark).
- **Proposition C → Proposition 5.1** (connected sums; Alexander's theorem for missing tetrahedra).
  **Proposition F → Proposition 5.2** (stellar subdivisions).
- **Corollary G → Corollary 5.3** (smallest counterexample in dimension 3: n ≥ 11, non-polytopal, prime, not a stellar
  subdivision, every edge in a missing triangle, no stacked link, no completable antistar).
- **Computations.** Thm 6.1 (3-spheres with 6 ≤ n ≤ 10 vertices), Cor 6.2 (A10 is the unique 10-vertex 3-sphere
  without a completable antistar, and the unique vertex-transitive neighborly one without LC edge), Prop 6.3
  (4-spheres with 7 ≤ n ≤ 9 vertices, conditional), Thm 6.4 (Table 1 spheres), Lemma 6.5 (soundness of the CNF
  Φ(S,u,v)). Table 1 gives the names of its spheres in Köhler–Lutz and in Kühnel–Lassmann; §6.2 identifies A10 with
  Altshuler's sphere through Köhler–Lutz, Table 4.

## Computations (exact; scripts and outputs in reproducibility/)
- **Author** (`lead/`, standard library only).
  - `check_certificates.py` (about three minutes on 16 cores) reports ALL CHECKS PASSED:
    - [1] the 3-sphere lists: certified spheres, pairwise non-isomorphic, the published counts, and the f_1
      distribution of Lutz 2008, Table 2; LC edges; the three vertex-transitive neighborly 10-vertex spheres;
    - [2] the 1320 extension certificates and the classification 1318 + 1 + 1;
    - [3] the 4-sphere lists;
    - [4] Table 1: 26 extension/completion certificates and 20 DRUP refutations, with the CNFs regenerated by
      its own encoder;
    - [5] negative controls: 138 non-sphere 3-manifolds and corrupted certificates and proofs are rejected.

    In this revision one comment of the program was corrected (Prop. 4.4 → Prop. 4.3). One run of the revised
    program from an extracted copy of the revised source archive passed all checks and reproduced the recorded
    output apart from timing fields.
  - `check_koehler_lutz.py` (new in this revision, about 20 seconds) reports ALL CHECKS PASSED. It rebuilds the 19
    neighborly 3-spheres with 10 to 14 vertices of Köhler–Lutz, Table 4, from orbit lists transcribed from the PDF
    (their Table 13 gives the generators of the one non-cyclic, non-dihedral group). It checks facet numbers and
    neighborliness, and computes canonical forms and automorphism groups with its own code, cross-checked with
    `sphere_tools.canonical_form`. Results:
    - Table 1 = 3_10^1_1, 3_11^1_1, 3_13^1_3, 3_13^1_5, 3_14^1_{17,14,26,18,27,4,8,7,11};
    - for each n = 10..14 the entries with an n-cycle in their automorphism group are exactly the orbit-search
      spheres (2, 2, 1, 3, 10); 3_10^4_2 has a group of order 20 without a 10-cycle;
    - the three vertex-transitive neighborly 10-vertex spheres of the list are 3_10^3_1 (the boundary of C_4(10)),
      3_10^4_2 and 3_10^1_1 ≅ A10.
  - `make_pairform_proofs.py` produced the DRUP proofs with Glucose 4 through PySAT: 24 to 8949 lemmas; CNFs with
    3330 to 15777 variables. `prepare_data_from_finder.py` reproduces `lead/data/` from the finder's files byte for
    byte. The finder's own DRUP proofs (A11 and Z13 pair forms, another encoding) were re-checked by the author's RUP
    checker on the original CNFs: 17 of 17 accepted.
- **Finder** (`claimant/`).
  - Bistellar-flip BFS for 3-spheres (n ≤ 10) and 4-spheres (n ≤ 9).
  - Exhaustive SAT enumeration of 9-vertex 4-spheres (same 337) and of neighborly 3-spheres (1, 4, 50, 3540 for
    n = 7..10).
  - SAT/CEGAR extension searches, which found the 1320 certificates and those of Table 1; completable-antistar
    searches; orbit-SAT searches for cyclic spheres.
  - DRUP-checked pair-form refutations for A11 and Z13.
  - Triple covers: 14 of the 15 rotation classes of A11; one class for Z13_1.
- **Independent verification run 1** (`verifier/`, AI-assisted, separate code).
  - A C checker (manifold test, collapsibility, own canonical form, LC edges) on the finder's lists.
  - Own sphere recognition for the 1320 extension certificates and the completion certificates (rerun in the
    release layout: 1320 of 1320; 1319 completion certificates, none for A10).
  - Own flip BFS: 1, 2, 5, 39, 1296 and 1, 2, 8, 337, identical sets.
  - Own SAT encoding of the pair forms via Prop 4.4: A10 exactly {0,1}, {0,5}; UNSAT for all other classes of A10
    and all classes of A11, Z13_0, Z13_1.
  - Verification of all Table 1 certificates.
- **Independent verification run 2** (`independent_run_2/`, AI-assisted, separate code written before reading the
  author's, the finder's or the first run's programs; rerun in the release layout during this revision with the
  same results).
  - Own C checker `sph.c` on all lists. Counts 1, 2, 5, 39, 1296, 247882, pairwise distinct canonical forms. The
    f_1 distribution for n = 10 equals Lutz 2008, Table 2; neighborly counts 1, 4, 50, 3540. Exactly 1320 spheres
    without LC edge, all prime, 1318 with a stacked vertex link. Lemma 3.2 holds on every sphere. Exactly three
    vertex-transitive neighborly 10-vertex spheres.
  - The 1320 extension certificates, the construction of Lemma 4.2 on the 1318, Table 1 as printed, and the 27
    special certificates.
  - PL certification independent of collapsing: every extension certificate (1320 and the 25 of Table 1) reduces by
    bistellar moves to the boundary of the 5-simplex, and both completion 3-spheres to the boundary of the
    4-simplex.
  - Own CNF for the pair forms (exact sequential counters): the same answers as the paper. All 20 Glucose DRUP
    proofs were verified by its own RUP checker `rup.c`, with negative controls.
  - The 4-sphere lists (1, 2, 8, 337). The finder's SAT enumeration was rerun with a patch that records the rejected
    candidates: 4149, of which 4148 have a vertex link that is not a closed combinatorial 3-manifold and one is a
    combinatorial 4-manifold with χ = 3. So completeness of the 337 rests only on the solver's final UNSAT answers.
    Random flip walks through 10–12 vertices met no 9-vertex 4-sphere outside the list (evidence only).
  - Theorem 3.1 and Remark 3.3 checked on 17,820 ordered vertex pairs of 210 sampled spheres.
  - Comparison with Köhler–Lutz, Table 4 (own transcription): all 13 Table 1 spheres matched; A10 ≅ 3_10^1_1.
  - One run of the author's checker from the previous release archive: ALL CHECKS PASSED.

## Independent verification
### Run 1 (2026-09-30, AI-assisted)
| Item | Verdict |
|---|---|
| Source fidelity (OWR p. 2467, Question 12 and the Altshuler remark; Datta's preprint) | CONFIRMED |
| Proofs (Theorem A and its missing-face form, Corollary A, Lemma H, Props B–F, Cor G, Cor B) | CONFIRMED (re-derived in the AI-assisted verification run) |
| Computations (lists and counts, 1320 certificates, completion certificates, 4-sphere lists, Table 1 certificates, pair forms) | CONFIRMED with own code; one error found (Z14 sphere #5, see fix 1) |
| Novelty | Theorem A is essentially Datta's flag-case construction with flagness replaced by the link condition: modest |
| Classification | PARTIAL_PAPER (correct: true; status partially_solved) |

Required fixes of run 1 and how they were applied:
1. *Z14 sphere #5 is settled by Lemma H* (prime, all links stacked; the finder's own completion certificate
   verifies). **Applied:**
   - Thm 6.4(d) says six of nine Z_14 spheres extend (Z14^i, i = 0, 2, 4, 7, 8 by certificates, i = 5 by Lemma 4.2);
     open: Z14^1, Z14^3, Z14^6.
   - The finder's RESULT.md, sections 0 and 3, was corrected; the pre-audit text is kept as
     RESULT_preaudit_2026-09-30.md.
2. *Theorem A as a generalisation of Datta's construction; modest novelty.* **Applied:** Remark 3.3 derives the
   identity with Datta's sphere and locates the only use of flagness. The introduction and "Scope and priority" call
   Theorem 3.1 a modest generalisation and cite the edge-contraction literature.
3. *Credit Santos for Datta's Question 2; identify A10 with Altshuler's sphere only via uniqueness or direct
   comparison.* **Applied:**
   - Remark 4.6 credits Santos' remark.
   - The identification first rested on Cor 6.2 together with the report's description. Since run 2 it rests on
     Köhler–Lutz, Table 4 (see below), with Cor 6.2 as an independent confirmation.
   - Altshuler (1976) could not be retrieved (HTTP 403); the paper says so.
4. *337 without literature cross-check; the A11 triple {0,1,9} UNSAT is solver-only.* **Applied:** in the text after
   Prop 6.3 and after Thm 6.4.

Additional changes after run 1:
- An independent checker by the author.
- A third, simpler CNF encoding of the pair forms with DRUP proofs. These also certify the A10 pairs {0,2}, {0,3},
  {0,4}, previously solver-only.
- Prop 4.3 and Lemma 2.3(c) made explicit.
- The vertex-transitivity check behind Cor 6.2.
- The f-vector cross-check with Lutz's Table 2.
- Negative controls.

### Run 2 (2026-09-30, AI-assisted; code and outputs in `reproducibility/independent_run_2/`)
| Item | Verdict |
|---|---|
| Statement fidelity (OWR 39/2019 pp. 2466–2467 re-read; Datta's preprint read in full; Criado–Santos, proof of Thm 3.5) | FAITHFUL; one slip in the abstract (the 3-sphere statement needs n ≥ 6) |
| Proofs (Sections 2–6, line by line) | CORRECT (re-derived in the AI-assisted verification run); two precision or credit fixes in Lemma 2.3 |
| Computations | REPRODUCED with own code (see above); the author's checker run once from the release archive: ALL CHECKS PASSED |
| Novelty and credit | partial results, modest novelty, no prior publication of the same results; the spheres of Table 1 are in Köhler–Lutz and Kühnel–Lassmann, and Köhler–Lutz attribute the Z_10 sphere to Altshuler |
| Overall | no mathematical error (not fatal); minor revision with 7 required fixes |

Required fixes of run 2 and how they were applied:
1. *Restrict the 3-sphere statement to 6 ≤ n ≤ 10* (the boundary of the 4-simplex has no extension). **Applied** in
   the abstract, the Zenodo description, the Verdict, the Readings and the Suggested corpus update above. The
   4-sphere statement is given everywhere for 7 ≤ n ≤ 9 and labelled as conditional on a solver result.
2. *No "by hand" for the independent checks.* **Applied:**
   - Verification item 3 of the paper now says that the AI-assisted verification runs re-derived the proofs and
     rechecked the computations with separate code.
   - The Scope paragraph says the results of Sections 3–5 are "proved in the text, without computer assistance".
   - In this report: "CONFIRMED (re-derived in the AI-assisted verification run)" and "Proved in the text".
3. *Credit the known enumeration of the Table 1 spheres.* **Applied:**
   - New references: Köhler–Lutz, arXiv:math/0506520 (Tables 2 and 4), and Kühnel–Lassmann, Israel J. Math. 52
     (1985) 147–166, doi:10.1007/BF02776088. Both were verified anonymously (arXiv export API; Crossref). The arXiv
     preprint is by E. G. Köhler and F. H. Lutz, so it is cited under both names.
   - Table 1 has two new columns with the names of its spheres in Köhler–Lutz and in Kühnel–Lassmann (the latter as
     quoted by Köhler–Lutz). The correspondence is the one found by run 2. It was checked again in this revision
     against a new transcription of Table 4 from the rendered PDF, with the author's own code
     (`lead/check_koehler_lutz.py`).
   - Köhler–Lutz also quote a Kühnel–Lassmann label for A10 (1_10), so all 13 spheres, not only those with 11, 13
     and 14 vertices, carry one.
   - §6.4 replaces "the completeness of this search is a solver result" by the statement that the counts
     2, 2, 1, 3, 10 agree with the enumeration of Köhler–Lutz. It adds that for n = 10..14 the neighborly spheres of
     their Table 4 with an n-cycle in the automorphism group are exactly the spheres of the orbit search. The
     abstract, the introduction and "Scope and priority" say that the spheres are known.
4. *Identify A10 with Altshuler's sphere through Köhler–Lutz, Table 4.* **Applied.**
   - Their Z_10-invariant sphere 3_10^1_1, with orbits 1235, 1236, 1246 and 1368_5, is attributed there to
     Altshuler 1976 and to Altshuler 1977 (N^10_3574).
   - The isomorphism with A10 was checked with the author's own code and by run 2 (`altshuler_lutz.py`).
   - Updated: §6.2 (the paragraph after Cor 6.2), Remark 4.6 and "Scope and priority"; Alt77 is now cited. Cor 6.2
     stays as an independent confirmation.
5. *Lemma 2.3(a) needs d ≥ 2.* **Applied** ("Let d ≥ 2" in (a)); the lemma is used only with d ≥ 2.
6. *Credit Datta–Singh for Lemma 2.3(b).* **Applied.**
   - The statement cites Datta–Singh, J. Combin. Theory Ser. A 120 (2013) 2148–2163, Lemma 2.1 (doi:
     10.1016/j.jcta.2013.08.005, verified on Crossref), quoted as Lemma 13 in Datta's preprint (checked in
     arXiv:2006.04470v2). The proof stays.
   - "Scope and priority" repeats the credit.
7. *Reword the Scope paragraph.* **Applied.** Non-existence statements are verified either by exhaustive direct
   computation (absence of LC edges and of stacked vertex links, primeness, non-isomorphism, vertex-transitivity) or
   by a DRUP refutation, except those labelled as solver results.

Optional suggestions of run 2:
- *Applied:*
  - (a) The count 322 of simplicial 5-polytopes with 9 vertices is credited to Fukuda–Miyata–Moriyama, DCG 49
    (2013) 359–381, doi:10.1007/s00454-012-9470-0 (verified on Crossref; Firsching's Table 1 names it as the
    source).
  - (e) The finder's names in code and outputs (Lemma H, Prop.-B, Proposition E, …) are mapped to the paper's
    numbering in `reproducibility/README.md`, and the recorded outputs are left unchanged. The comment in
    `lead/check_certificates.py` that pointed to Prop. 4.4 now points to Prop. 4.3.
  - (f), in part: the re-examination of the rejected SAT candidates is mentioned in the Verification paragraph.
  - (h), in effect: Table 1 now gives the Kühnel–Lassmann labels of all spheres, including the undecided ones.
- *Not applied in this revision:* (b) a remark on the use of flagness in Remark 3.3; (c) Datta's Theorem 8 in
  Remark 4.6; (d) a remark that the sphere with f = (10,40,60,30) is itself vertex-transitive; (g) a description of
  the collapse strategy in §6.1.

### Final check (2026-09-30, AI-assisted)
- The revised source archive was extracted afresh. The paper builds from it, with the same text as the released PDF.
  `lead/check_koehler_lutz.py` passes and reproduces its recorded output. `lead/check_certificates.py --quick`
  passes; its sections [2] to [5] agree with the recorded full run.
- Two identifications of Table 1 were confirmed with separate code by explicit isomorphisms: A10 with 3_10^1_1 and
  Z14^3 with 3_14^1_18. The orbit lists and remarks of Köhler–Lutz, Table 4, were compared with the rendered PDF.
- The bibliographic data of the new references were verified again on Crossref and with the arXiv export API.
- Changes:
  - "Scope and priority" now also names Datta–Singh and Fukuda–Miyata–Moriyama among the works not seen; what the
    paper says about them is taken from Datta's preprint and from Firsching's Table 1;
  - the header comment of `reproducibility/verifier/sat/ops_sat.py` was reworded.

## Relation to the literature, novelty and scope
- **Read:**
  - the Oberwolfach problem session;
  - Datta, arXiv:2006.04470v2 (again in this revision, for Lemma 13 and its source);
  - Köhler–Lutz, arXiv:math/0506520v1 (Tables 2, 4 and 13, and the references of Table 4), in this revision;
  - Lutz, "Combinatorial 3-manifolds with 10 vertices" (arXiv version; Tables 1 and 2);
  - Sulanke–Lutz (arXiv version; Table 9);
  - Lutz's survey "Triangulated manifolds with few vertices: combinatorial manifolds" (arXiv:math/0506372; neighborly
    counts 1, 4, 50, 3540);
  - Firsching, Math. Program. 166 (2017) (arXiv version; Table 1);
  - Criado–Santos, arXiv:1807.03030v3 (in run 2; the proof of Thm 3.5 contains the lifting argument).
- **Not seen** (bibliographic data verified on Crossref; content as quoted by Köhler–Lutz, Datta or Firsching):
  - Altshuler, Proc. AMS 54 (1976) 449–452 (access refused);
  - Altshuler, Canad. J. Math. 29 (1977) 400–420;
  - Kühnel–Lassmann, Israel J. Math. 52 (1985) 147–166;
  - Datta–Singh, J. Combin. Theory Ser. A 120 (2013) 2148–2163;
  - Fukuda–Miyata–Moriyama, Discrete Comput. Geom. 49 (2013) 359–381;
  - the published version of Criado–Santos;
  - Nevo (2007), for which only the abstract was read.
- **Searches (September 2026, anonymous, logged).**
  - arXiv API; Crossref (all DOIs in the bibliography verified); OpenAlex (Datta's preprint has no citations; the
    works citing Criado–Santos concern realizability, diameters and Hirsch-type questions); zbMATH; Semantic
    Scholar (in the verification runs); two web searches by the author and one in run 2.
  - In this revision: the arXiv export API and PDF for math/0506520, the arXiv PDF of 2006.04470v2, and Crossref for
    the four new or newly cited DOIs (Kühnel–Lassmann, Datta–Singh, Fukuda–Miyata–Moriyama, Altshuler 1977).
  - No resolution of Question 12 and no statement of Theorem 3.1 or Lemma 4.2 was found; both are elementary and may
    be known to experts. This negative search is not a proof of priority.
- **Scope.**
  - The general question is open. Thm 6.1 depends on the published counts of 3-spheres, which our flip search
    reproduced independently. Prop 6.3 is conditional for 9 vertices.
  - Not used anywhere, being solver results without certificates:
    - the completeness of the orbit searches (their counts agree with Köhler–Lutz);
    - the completeness of the SAT enumeration of 9-vertex 4-spheres;
    - the finder's UNSAT answer for the A11 triple {0,1,9}.
  - The spheres of Table 1 are known (Kühnel–Lassmann; Köhler–Lutz). The results about their extensions
    (Thm 6.4) appear to be new.
  - Undecided: Z14^1, Z14^3, Z14^6 (Kühnel–Lassmann 9_14, 11_14, 4_14; Köhler–Lutz 3_14^1_14, 3_14^1_18, 3_14^1_8).

## Suggested corpus update (not performed)
Keep OWR-17135-036 as `partially_solved` and add a note citing this preprint:

> Partial progress on Santos' question. If some edge vw of S satisfies lk(v) ∩ lk(w) = lk(vw), then
> (v*ast(v)) ∪ (w*ast(w)) is an n-vertex (d+1)-sphere containing S. This generalises Datta's flag case
> (arXiv:2006.04470). The same holds for spheres without missing d-faces that have a stacked vertex link. With
> certified computations, every combinatorial 3-sphere with 6 ≤ n ≤ 10 vertices lies in a 4-sphere on the same vertex
> set. All 337 enumerated 9-vertex 4-spheres have such an edge; the completeness of that enumeration is a solver
> result without certificates. A Z11-invariant and two Z13-invariant neighborly 3-spheres (known from Kühnel–Lassmann
> and Köhler–Lutz) extend, but admit no extension in which every facet meets a fixed pair of vertices. The general
> question remains open.

## 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/