Skip to content

Source Audit: Conjecture 3 Manuscript Skeleton

Created: 2026-05-11

Scope: audit theorem statements in manuscript_conjecture_3 against the local graph, 10_conjectures.bib, and local PDF bundles. This is a source-fidelity audit only; it adds no new theorem claims.

Local Sources Checked

  • leverrierQuantumTannerCodes2022: local PDF resolved and bundled at tmp/paper-bundles/leverrier-zemor-2022.
  • baspinLowerBoundOverhead2023: local PDF resolved and bundled at tmp/paper-bundles/baspin-fawzi-shayeghi-2023.
  • delfosseBoundsStabilizerMeasurement2021: local PDF resolved and bundled at tmp/paper-bundles/delfosse-beverland-tremblay-2021.
  • alonSeparatorTheoremGraphs1990: local PDF resolved and bundled at tmp/paper-bundles/alon-seymour-thomas-1990.

PDF bundle page labels below are extracted-page filenames; final manuscript page references should be checked against the rendered PDFs before submission.

Citation-Key Audit

All citation keys used in the LaTeX files exist in 10_conjectures.bib.

Used keys:

  • alonSeparatorTheoremGraphs1990
  • baspinLowerBoundOverhead2023
  • delfosseBoundsStabilizerMeasurement2021
  • leverrierQuantumTannerCodes2022

Missing keys: none.

Duplicate bibliography keys: none detected.

Suspicious keys: none for the current skeleton. The proof appendix still asks whether the Quantum Tanner citation should point to the FOCS record or an arXiv-form statement; the existing key is the FOCS record and is present.

Source-Theorem Extraction Notes

Baspin-Fawzi-Shayeghi 2023

Bundle: tmp/paper-bundles/baspin-fawzi-shayeghi-2023.

Relevant pages:

  • pages/page-0004.txt: informal Theorem 3 states the syndrome-extraction depth form as Omega(k sqrt(d) / m) for 2D.
  • pages/page-0011.txt to pages/page-0012.txt: formal Theorem 24 states the D-dimensional syndrome-extraction bound Omega(k d^{1/D} / m).

Source-backed use:

  • Specializing Theorem 24 to D=2 gives Omega(k sqrt(d) / m).
  • The theorem is for stabilizer syndrome extraction using a geometrically local circuit model with arbitrary local operations and free classical computation, matching the manuscript's model definition.

Leverrier-Zemor 2022

Bundle: tmp/paper-bundles/leverrier-zemor-2022.

Relevant pages:

  • pages/page-0023.txt: Theorem 17 gives Quantum Tanner code parameters under component-code and robustness hypotheses, including positive rate and linear distance for fixed Delta.
  • pages/page-0024.txt: Theorem 18 gives a random component-code existence mechanism satisfying the hypotheses of Theorem 17 with nonzero probability.

Source-backed use:

  • The manuscript only uses the consequence k = Theta(n) and d = Theta(n) for theorem-level Quantum Tanner families.
  • It does not claim an explicit deterministic component-code construction beyond the source theorem.

Delfosse-Beverland-Tremblay 2021

Bundle: tmp/paper-bundles/delfosse-beverland-tremblay-2021.

Relevant pages:

  • pages/page-0002.txt: Theorem 1 gives depth(C) >= n_cut / (64 |partial L|) for Clifford circuits measuring commuting Pauli operators.
  • pages/page-0013.txt: Lemma 5 gives the mutual-information upper bound with constant 32 |partial L| depth(C).
  • pages/page-0015.txt: proof of Theorem 1 combines Lemmas 4 and 5 to obtain the 1/64 depth constant.
  • pages/page-0003.txt and related application pages state 2D local Clifford consequences for local-expander QLDPC families.

Source-backed use:

  • The 1/64 constant in the stabilizer cut-rank functional is source-backed after using the graph node that proves chi_L(S) <= n_cut for any generating family.
  • The 1/16 SWAP-only service constant is not stated verbatim in this paper. It is a local graph-derived sharpening of the same proof skeleton, so the manuscript now uses an unspecified universal constant c_swap.

Alon-Seymour-Thomas 1990

Bundle: tmp/paper-bundles/alon-seymour-thomas-1990.

Relevant pages:

  • pages/page-0002.txt: Theorem 1.2 gives a weighted separator for graphs excluding an h-vertex minor with order bounded by a constant multiple of h^{3/2} sqrt(n).
  • pages/page-0003.txt: Proposition 1.3 gives the complete-graph-minor formulation with a weighted flap bound.
  • pages/page-0006.txt: Proposition 4.1 gives a removable set with controlled weighted components, with the same h^{3/2} sqrt(n) scale.

Source-backed use:

  • The fixed-minor-free corollary may safely use O(h^{3/2} sqrt(N)).
  • The theorem is vertex-separator based; edge-boundary conversion requires the separate bounded-degree hypothesis already present in the manuscript.

Theorem-By-Theorem Verification

Label Current manuscript statement Source-backed statement Classification Required correction
thm:static-2d-lower-bound Quantum Tanner good family with k=Theta(n), d=Theta(n) has 2D local syndrome-extraction depth Omega(k sqrt(d)/m)=Omega(n^{3/2}/m). Baspin-Fawzi-Shayeghi Theorem 24 gives Omega(k d^{1/D}/m); Leverrier-Zemor Theorems 17/18 supply theorem-level families with linear k,d. EXACT, using the model definition. None. Keep the model definition explicit about arbitrary local operations and free classical computation.
cor:swap-only-static-grid SWAP-only static near-square 2D grid in linear space has Omega(sqrt n) depth. SWAP-only nearest-neighbor grid compilation is a special case of the 2D local syndrome-extraction model used above. EXACT as a corollary. None.
thm:weighted-separator-depth Bounded-degree hardware with weighted separator profile s_hw(N) gives depth Omega(n/(Delta_hw s_hw(N))) for local Clifford measurement of bounded-weight local-expander QLDPC codes, if s_hw(N)=o(n). Graph-derived corollary: weighted separator gives a balanced data cut with edge boundary O(Delta_hw s_hw(N)); DBT local-expander cut-to-depth gives the depth lower bound. EXACT relative to graph source package; proof expanded in the proof-polish pass. No theorem-statement edit.
cor:fixed-minor-free-depth Excluding a fixed h-vertex minor gives depth Omega(n/(Delta_hw h^{3/2} sqrt N)) in the useful balanced regime. AST weighted excluded-minor separator gives vertex separators of size O(h^{3/2} sqrt N); bounded degree converts this to edge capacity. EXACT asymptotically. None.
thm:stabilizer-cut-rank-functional Clifford measurement depth is at least (1/64) max_L chi_L(S)/|partial L|; rank formula for chi_L. DBT Theorem 1 gives n_cut/(64 |partial L|). Local graph rank nodes prove chi_L(S) <= n_cut and chi_L = rank(H_L)+rank(H_R)-rank(H). EXACT. None.
lem:lambda-symmetric-submodular lambda_S(L)=chi_L(S) is integer-valued, symmetric, and submodular. Local rank formula identifies lambda_S with the column-matroid connectivity function. Matroid connectivity is symmetric and submodular. EXACT. None.
thm:swap-only-submodular-cd After edit: there is a universal c_swap>0 such that SWAP-only depth is at least c_swap CD_sub. Local graph service-bound node derives a universal service constant from DBT proof bookkeeping, but the numerical 1/16 is not stated verbatim in DBT. CONSTANT-ONLY, fixed by weakening. Replaced 1/16 with c_swap; keep TODO only for optional numerical constant polishing.

Constants Audit

  • 1/64 in thm:stabilizer-cut-rank-functional: source-backed by DBT Theorem 1, after replacing n_cut by the smaller intrinsic quantity chi_L(S) using local graph nodes.
  • Former 1/16 in thm:swap-only-submodular-cd: graph-derived, not source-verbatim. The manuscript now uses c_{\mathrm{swap}}>0.
  • Fixed-minor-free factor: O(h^{3/2}\sqrt N) is source-backed by AST. The corollary's asymptotic denominator h^{3/2}\sqrt N is acceptable under big-O/big-Omega notation. Do not state a sharp leading constant.

Model-Scope Audit

The skeleton cleanly distinguishes:

  • arbitrary 2D-local syndrome-extraction circuits, only for the Baspin-Fawzi-Shayeghi parameter theorem;
  • local Clifford stabilizer-measurement circuits, for separator and stabilizer cut-rank lower bounds;
  • measurement-free SWAP-only circuits with final local measurements, for CD_sub;
  • arbitrary compilers, explicitly not covered.

Sentences checked for blurring:

  • Introduction paragraph 2 is safe because the model definition supplies the arbitrary-local/free-classical scope.
  • Introduction paragraph 3 is safe because it explicitly says local Clifford stabilizer-measurement model.
  • Discussion paragraph 3 is safe because it states partial resolution and excludes arbitrary compilers.

No model-scope manuscript edit was required beyond the constant weakening in the SWAP-only theorem.

Remaining Source-Fidelity TODOs

  • Final rendered page numbers should be checked against source PDFs before submission.
  • The weighted-separator proof has been expanded in sections/separator_barriers.tex; final page references for the separator source should still be inserted before submission.
  • The cross-cut rank formula placement has been decided: the main text gives the proof sketch and appendices/proof_details.tex contains the full linear-algebra proof.
  • If explicit constants matter, derive and document the numerical value of c_{\mathrm{swap}}; otherwise leave the theorem with a universal constant.