# Verification report — OWR-11786-023 (Santos' question on the dual diameter of surfaces with boundary)

Verification date: 2026-10-01.

**Verdict.** The answer is no. The 7-vertex triangulation M7 of the real projective plane minus two disjoint open
discs has dual diameter 5 > n − 3 = 4. Gluing copies along boundary edges gives f̄(2,n) ≥ n − 3 + ⌊(n−2)/5⌋ for all
n ≥ 3, so the excess over n − 3 is unbounded. An orientable genus-2 surface with 10 vertices and dual diameter 8 gives
the same conclusion for orientable surfaces. The complex M7 is already Figure 4 of Holmes (EJC 2018), who did not
identify it as a surface or relate it to Santos' question; together with Holmes' upper bounds (including the value
µ(3,9) = 7, proved in his dissertation) his work already determines f̄(2,n) for 6 ≤ n ≤ 9 once one observes that
surfaces satisfy (S2). The note is unrefereed.

## Statement checked
- **Primary source.** Oberwolfach Report 24/2012, *Triangulations* (organizers W. H. Jaco, F. H. Lutz, F. Santos,
  J. M. Sullivan), Oberwolfach Rep. 9 (2012), no. 2, 1405–1486, doi:10.4171/OWR/2012/24. Minutes of the open problem
  session (reporter B. Benedetti), pp. 1478–1482, problem 9 (F. Santos), p. 1480.
  - The published PDF was read (anonymous download from EMS Press); the formulas were checked on a rendered image of
    p. 1480, in the writing phase and again in the independent verification run.
  - The source defines f(d,n) as the maximal (dual) diameter of a closed simplicial d-manifold with n vertices,
    f̄(d,n) as the same for a manifold with boundary, and analogous functions for pseudomanifolds.
  - It recalls f(2,n) ≤ n − 3 and f̄(2,n) ≤ 2n for surfaces and asks whether f̄(2,n) ≤ n − 3 for surfaces with
    boundary.
  - "Dual diameter" is used in the standard sense of Santos' survey (TOP 21 (2013), Sect. 2.2) and of Criado–Santos
    (DCG 58 (2017)): the diameter of the graph whose vertices are the facets, two facets being adjacent when they share
    a ridge. The survey notes that simplicial manifolds with or without boundary are normal complexes.
- **Corpus record.** ulamai/UnsolvedMath, version 1.6.0, record OWR-11786-023 (status `open`). Its statement asks
  whether the maximal dual diameter of a triangulated surface with boundary and n vertices is at most n − 3, which
  matches the source.
  - The literature note attached to the record describes a different problem (Lagrangian structures and the Novikov
    conjecture) and links to the neighbouring report doi:10.4171/owr/2012/25 (*Analysis and Geometric
    Singularities*, pp. 1487–1562). It should be replaced.

## Readings
| Reading | Refuted? | Witness |
|---|---|---|
| f̄(2,n) ≤ n − 3 for all triangulated surfaces with boundary (source, record) | yes | M7: n = 7, dual diameter 5 |
| the same for orientable surfaces with boundary | yes | G10: n = 10, genus 2, dual diameter 8 |
| f̄(2,n) ≤ n − 3 + C for some constant C | yes | chains of M7: excess ⌊(n−2)/5⌋ |
| "manifold with boundary" allowing empty boundary | yes (same examples) | the certified upper bounds cover closed surfaces too |
| the same question for orientable surfaces of genus 0 or 1 (e.g. discs) | not decided | no violator with at most 10 vertices (orientable n ≤ 9: certified; n = 10: exhaustive enumeration) |

## Results in the paper
- **Theorem 1.1(a).** M7 = {012, 014, 035, 036, 045, 123, 235, 245, 246, 346} is a surface (all links are paths or
  cycles), χ = −1, two boundary circles 0-2-6 and 1-3-4. Capping them gives a closed surface with χ = 1, so M7 is RP²
  minus two disjoint open discs. Its dual diameter is 5.
  - Hand-checkable certificate: the breadth-first layers from 012 are {012}, {014, 123}, {045, 235}, {035, 245},
    {036, 246}, {346}, and every one of the 12 dual edges joins consecutive layers.
- **Lemma 4.1 (edge sum).** Gluing two surfaces with boundary along boundary edges of triangles T1, T2 gives a surface
  whose dual graph is the disjoint union plus the bridge T1T2, so dual distances add up plus 1.
- **Theorem 1.1(b).** f̄(2,n) ≥ n − 3 + ⌊(n−2)/5⌋ for n ≥ 3. Chains of M7 glued edge 34 to edge 02, plus pendant
  triangles.
- **Theorem 1.1(c).** G10 (20 triangles, coherent orientation listed in the paper) is an orientable genus-2 surface
  with two boundary circles and dual diameter 8. It gives f̄_or(2,n) ≥ n − 3 + ⌊(n−2)/8⌋.
- **Theorem 1.1(d).** Every surface with n ≥ 3 vertices has dual diameter ≤ max(n−3, 2n−8), by a self-contained
  layer/block argument (a variant of Holmes' proof of his Thm. 19). Hence 6/5 ≤ lim inf f̄(2,n)/n and
  lim sup f̄(2,n)/n ≤ 2. Holmes' Thm. 19 gives the stronger max(2n−10, n−2) for n ≥ 7, for all (S2) complexes.
- **Theorem 1.2 (computer-assisted, DRAT-certified).**
  - f̄(2,n) = n − 3 for n ≤ 6 and f̄(2,n) = n − 2 for 7 ≤ n ≤ 10 (for 6 ≤ n ≤ 9 this also follows from Holmes'
    Props. 37, 39–41, Thm. 19 and dissertation Prop. 3.6.7).
  - M7 is the only surface with at most 7 vertices whose dual diameter exceeds n − 3. There are exactly two such
    isomorphism classes on 8 vertices.
  - f̄_or(2,n) = n − 3 for n ≤ 9, and f̄_or(2,10) = 8.
- **Section 6.3 (exhaustive enumeration, uncertified, independent of the SAT encoding).** Confirms Theorem 1.2 and
  shows that G10 is the only orientable surface with at most 10 vertices that violates n − 3.
- **Uncertified.** For n = 11, CaDiCaL answers UNSAT for distance 10 (all and orientable), which suggests
  f̄(2,11) = f̄_or(2,11) = 9. The case n = 12, D = 12 is undecided.

## Checks made while the note was prepared (`reproducibility/search`, `reproducibility/audit`, `reproducibility/crosscheck`)
These programs were written in the writing pipeline (the `audit/` programs separately from the search code); they
are not an independent verification run.
- **Search.** `satsearch.py` implements the encoding E(n,D) / E_or(n,D) of Section 6.1 with lazy link cuts;
  `certify.py` runs Glucose 4.1 (python-sat 1.9.dev15) with DRAT proof logging and writes the final formula and
  the proof. There are 11 certificates for n ≤ 10 (Table 1), 2 redundant orientable ones ((5,3) and (6,4)), and 2
  enumeration certificates ((7,5) and (8,6), with blocking clauses). `tools/drat_check.c` and
  `tools/drat_check2.c` are forward checkers (deletions ignored / applied). The explicit constructions are verified
  by `verify_example7.py`, `verify_orientable10.py`, `glue.py`, `example12.py` and `holmes_check.py`.
- **Audit programs.** `indep_check.py` (explicit constructions with Floyd–Warshall distances; Lemma 4.1 on 150
  random pairs; the block argument on 173 surfaces), `rupcheck.c` (forward RUP checker, both deletion modes, with a
  self-test), `cnf_audit.py` (formula audit), `indep_sat.py` (a second encoding, CaDiCaL 1.9.5) and a third
  encoding in `crosscheck/`. All checks pass; the n = 10 proofs were checked by `drat_check2` and `rupcheck`
  (`audit/outputs/n10_checks.txt`).
- **Certificates.** The 13 certificates with n ≤ 9 are in `certificates/` (compressed, about 8.5 MB). The two
  n = 10 proofs (420 MB and 390 MB) are not included; the search is deterministic, and `certificates/regenerate_n10.sh`
  reproduces them (sha256 in `certificates/n10_certificates.txt`).

## Independent AI-assisted verification run (2026-10-01; `reproducibility/independent_run_2/`)
The first verification run independent of the writing pipeline. It read the source and every proof, checked the
cited results in the original papers, repeated the literature search, and wrote new code (standard library Python
and C) without importing or copying any code of the search or of `audit/`.
- **Proofs.** Lemma 2.2, Theorem 1.1(a)–(d), Lemma 4.1, Lemma 6.1 and the proof of Theorem 1.2 were read line by
  line; no mathematical error was found. Requested corrections: credit to Holmes' dissertation and to Holmes'
  results for 6 ≤ n ≤ 9; an accurate description of the checks (the earlier text called the writing-phase checks
  "independent verification runs"); several precision fixes (applied in the paper).
- **Explicit constructions** (`surfcheck.py`): every printed link, edge list, boundary circle, χ, orientation, dual
  edge list, BFS layer table, geodesic and unique far pair of M7 and G10; the chains for n ≤ 60 (diameters exactly
  n−3+⌊(n−2)/5⌋ and n−3+⌊(n−2)/8⌋); the 12-vertex example; the second 8-vertex class; Holmes' Figures 4, 6,
  6 + EHI (surfaces; Figure 4 = M7 under the stated map) and 7 (not a surface); Lemma 4.1 on 200 random gluings.
  All checks pass.
- **Exhaustive enumeration without SAT** (`enum_surfaces.c`, `classify.py`, `canon_c.c`): all labelled complexes
  for n ≤ 7, and for 5 ≤ n ≤ 10 all surfaces up to isomorphism (vertex 0 of maximal degree with its link in
  canonical position); n = 10 in 10 parts, 3.26·10^11 search nodes. Completeness check: the closed surfaces found
  for n = 4..10 form 1, 1, 3, 9, 43, 655, 42426 isomorphism classes (Lutz's numbers; for n = 10 the 1,533,304
  closed complexes found were reduced to canonical forms with `canon_c.c`). Maximal dual diameters of surfaces
  with boundary for n = 3..10: 0, 1, 2, 3, 5, 6, 7, 8; of closed surfaces for n = 4..10: 1, 2, 3, 3, 4, 5, 5.
  Violators (dual diameter ≥ n−2): 1, 2, 35, 621 classes for n = 7, 8, 9, 10; the n = 7, 8 classes are those of
  Theorem 1.2(b); none is orientable for n ≤ 9; for n = 10 the only orientable one is G10. The program's
  diameters and orientability were re-checked for every violator with the separate Python code (0 inconsistencies).
- **Third RUP checker** (`rup_run2.c`, deletions ignored): all 13 stored certificates VERIFIED with the lemma counts
  of Table 1 (and 773, 7645 for the enumerations); self-test 14/14 (including rejection of the stored proofs against
  the satisfiable formulas E(7,6) and E(9,8) without link cuts).
- **Formula audit from the text** (`cnf_audit_run2.py`): E(n,D) and E_or(n,D) regenerated from Section 6.1; each
  certified formula equals these clauses (as a multiset) followed by valid link cuts, and, for the enumerations,
  by full-assignment blocking clauses for 4 copies of M7 (n = 7) and 8 + 8 copies of the two 8-vertex classes;
  all 15 formulas PASS; self-test 8/8.
- **n = 10 certificates.** Regenerated from a fresh extraction of the package with `regenerate_n10.sh` (6 min,
  820 MB, kept outside the package): all four sha256 hashes equal the recorded ones; `drat_check2` VERIFIED
  (RAT: 0); formula audit PASS for both; `rup_run2`: VERIFIED for both (outputs in `independent_run_2/outputs/n10/`).
- **Rerun of the package** from a fresh extraction of the source archive (`rerun_package.sh`): the explicit
  constructions, both enumerations, the certification runs (all 26 certificate files for n ≤ 9 regenerated bit for
  bit, and the n = 10 regeneration above), the checker self-tests, `recheck_certs.sh`, `indep_check.py`,
  `check_certificates.py` and the third-encoding crosscheck; every output agreed with the recorded one (only two
  timing values in the crosscheck output differ). Not repeated: the long uncertified solver runs (`indep_sat.py`,
  `run_max.py` for n ≥ 10, the n = 11 runs).

## Relation to the literature, novelty and scope
- **Prior art.** B. Holmes, Electron. J. Combin. 25(1) (2018) #P1.60, doi:10.37236/6831 (arXiv:1611.07354) studies
  µ(3,n), the maximal diameter of dual graphs of 2-dimensional (S2) complexes, which are the normal complexes.
  - His Figure 4 (Prop. 39, µ(3,7) = 5) is M7. His examples for µ(3,8) and µ(3,9) are M7 with one and two pendant
    triangles.
  - With his Prop. 37 (µ(3,6) = 3), Thm. 19 (µ(3,n) ≤ max(2n−10, n−2)) and Prop. 41 (µ(3,9) = 7, proved in his
    Ph.D. dissertation, University of Kansas 2018, hdl:1808/28042, Prop. 3.6.7) this gives f̄(2,n) for 6 ≤ n ≤ 9,
    once one notices that these complexes are surfaces. Holmes does not note this and does not mention Santos'
    question (the dissertation was searched for surfaces and manifolds).
  - His 5/4-slope families use complexes with edges in three triangles, so they are not surfaces.
- **Searches (September–October 2026).** arXiv API (dual diameter, Hirsch and surfaces/manifolds, surfaces with
  boundary, normal complexes, pseudomanifolds, Stanley–Reisner dual graphs, and more), Crossref, zbMATH, Semantic
  Scholar, the Kansas repository and the web (one search in each phase). All requests are listed in `queries.log`
  of the working folder (anonymous).
  - Semantic Scholar lists five works citing Holmes: his dissertation and four papers on commutative algebra and
    matroids (abstracts read).
  - OpenAlex citation queries were rate-limited.
  - Nothing found states that surfaces with boundary can exceed n − 3, or answers the question.
- **Not accessed.** Adler–Dantzig (1974) on abstract polytopes; the Klee–Kleinschmidt survey (1987); the discussion
  papers published with Santos' survey in TOP (Terlaky, Eisenbrand, Hiriart-Urruty, De Loera, rejoinder). The proof
  in Holmes' dissertation was not checked. Older unrecognized examples cannot be excluded; this negative search is
  not a proof of priority.
- **Novelty claimed (modest).**
  - The observation that Holmes' complex answers Santos' question.
  - Unbounded excess (non-orientable and orientable families).
  - The orientable threshold n = 10 (and, by the enumeration, uniqueness of G10 there).
  - A short proof of max(n−3, 2n−8).
  - The value f̄(2,10) = 8, uniqueness at n = 7 and the two classes at n = 8, and the orientable values, all
    DRAT-certified; an independent certified verification of the values for n ≤ 9.
- **Open.**
  - Existence and value of lim f̄(2,n)/n (known: between 6/5 and 2).
  - Whether f̄(2,n) = n − 3 + ⌊(n−2)/5⌋ for all n (true for n ≤ 10).
  - The growth of f̄_or.
  - Which topological types (e.g. orientable of genus 0 or 1) can violate n − 3.

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