Claude Code transcript - page 4/4

Please use the latex skill to build the file using tectonic

Skill
{
  "skill": "tectonic",
  "args": "/home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.tex"
}
Launching skill: tectonic

Base directory for this skill: /home/apanda/code/gleam-as-emulation/.claude/skills/tectonic

Overview

Use tectonic when possible, however if that fails use latexmk.

Using tectonic

To build a file using tectonic do

tectonic <latex file>

This might fail because the latex file uses minted, in this case try

tectonic -Z shell-escape <latex file>

Finally, there are files that tectonic will fail on, even if you use shell-escape. In this case use latexmk

Using latexmk

To build a file using latexmk call

latexmk -pdf <latex file>

ARGUMENTS: /home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.tex

$ Bash
Build PDF with tectonic
tectonic "/home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.tex" 2>&1
note: Running TeX ...
note: downloading SHA256SUM
note: downloading booktabs.sty
warning: computational-search-conclusions.tex:81: Overfull \hbox (2.51067pt too wide) in paragraph at lines 78--81
warning: computational-search-conclusions.tex:138: Overfull \hbox (2.5757pt too wide) in paragraph at lines 111--138
note: Rerunning TeX because "computational-search-conclusions.aux" changed ...
warning: computational-search-conclusions.tex:81: Overfull \hbox (2.51067pt too wide) in paragraph at lines 78--81
warning: computational-search-conclusions.tex:138: Overfull \hbox (2.5757pt too wide) in paragraph at lines 111--138
warning: warnings were issued by the TeX engine; use --print and/or --keep-logs for details.
note: Running xdvipdfmx ...
note: downloading cmex10.pfb
note: Writing `/home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.pdf` (68.58 KiB)
note: Skipped writing 2 intermediate files (use --keep-intermediates to keep them)

Built successfully. The updated PDF is at graph proofs/computational-search-conclusions.pdf.

Now let me write the transcript.

📝 Write transcript.md
/home/apanda/code/gleam-as-emulation/graph proofs/transcript.md
# Transcript: Investigating the BSC Resilient Forwarding Conjecture

This document records the sequence of requests and findings from a conversation exploring the conjecture that for any k-connected graph, static forwarding tables can tolerate k-1 edge failures.

---

## 1. Initial Request

**User:** Write in LaTeX a proof for the conjecture: given a k-connected graph it is possible to find a static forwarding table that allows any pair of nodes to communicate as long as fewer than k-1 edges have been cut. Reference paper: Chiesa et al., "The Quest for Resilient (Static) Forwarding Tables" (INFOCOM 2016).

**Result:** Produced `static-resilient-forwarding-proof.tex` — a proof using O(log k) header bits (HDR model) based on Edmonds' arc-disjoint arborescences, the edge-disjoint partition lemma, and the good arborescence existence argument. Compiled to 6-page PDF.

---

## 2. Generalize Beyond k ≤ 5

**User:** The proof you produced is from the paper, and only applies when k ≤ 5. Can you generalize to arbitrary values of k.

**Finding:** Research confirmed the BSC conjecture (no header bits) is **genuinely open for k > 5** as of 2025 (confirmed by Dai, Foerster, Schmid, arXiv:2410.02021, Oct 2024). The HDR proof (with header bits) already works for all k.

**Result:** Produced `static-forwarding-proof-extended.tex` — a 9-page document with:
- BSC proof for k ≤ 5 (Theorems for k=2,3 and k=4,5)
- HDR proof for all k (using ⌈log k⌉ header bits)
- Identification of the precise open step: the "Reachability Lemma" — proving that BSC bounce-circular routing must visit the good arborescence before looping
- Discussion of why reachability is hard (bounces disrupt circular traversal)

---

## 3. Search for Counterexamples at k = 6

**User:** Given where we are, can you try to find a counterexample when k = 6.

**Approach:** Built Python scripts using networkx to:
1. Generate random 6-connected graphs (n = 8–12)
2. Find arc-disjoint arborescences via randomized greedy BFS
3. Simulate BSC strategies (bounce-circular, circular-only, min-depth)
4. Check AND-OR reachability (determines if ANY BSC strategy can work)

**Scripts:** `search_counterexample.py`, `search_v2.py`, `search_v3.py`

**Results:** 50 random dense graphs tested, thousands of failure sets each — **zero loops, zero AND-OR failures**. Dense graphs have too much redundancy.

For small multigraphs (3-vertex with 9 edges, 4-vertex with 12 edges): exhaustive AND-OR reachability over all failure sets — **zero failures**. Conjecture consistent.

---

## 4. Search for Counterexamples at k = 12

**User:** Hmm, what if you tried k = 12?

**Approach:** Built multigraphs with k = 12 arborescences on 3–13 vertices. Tested star-based arborescences (zero shared arcs) and chain-based arborescences (24 shared arcs with maximal sharing).

**Scripts:** `search_k12.py`, `search_k12_shared.py`, `search_k12_exhaustive.py`

**Results:**
- Star arborescences: zero shared arcs, trivially no failures
- Chain arborescences (24 shared arcs): **exhaustive enumeration of all 2,496,144 failure sets — zero AND-OR failures**
- Conjecture holds for k = 12 on all tested graphs

---

## 5. Complexity Analysis

**User:** How hard (in terms of computational complexity) is it to find resilient routing tables? I am particularly interested in whether computing resilient routing tables when k = 12 requires substantially more computation than when doing so when k = 6.

**Key findings:**
- **HDR model:** Polynomial, O(knm). k = 12 is just 2× slower than k = 6.
- **BSC model:** Verification is coNP-complete (Bentert et al., OPODIS 2025). Construction for k > 5 is open.
- **k = 6 vs k = 12:** The adversary space grows as C(m, k-1) — a factor of ~10⁵ more failure patterns. The strategy space grows super-exponentially. The gap is qualitative, not just quantitative.

**Result:** Written to `complexity-analysis.md`.

---

## 6. Search on 6-Regular Graphs

**User:** Can you try looking for counterexamples with k = 6, but only consider graphs where all nodes have degree 6.

**Rationale:** 6-regular graphs are the sparsest possible 6-connected simple graphs. The tight arc budget forces heavy edge sharing between arborescences (86–92% of arcs shared), creating the bounce dynamics that make BSC hard.

**Script:** `search_6reg.py`

**Key challenge:** The greedy BFS approach initially failed on 6-regular graphs because the arc constraint is extremely tight (only 6 arcs wasted out of 6n). Solved by using an interleaved random construction with many restarts.

**Results (200 6-regular graphs, ~30 million failure sets):**

| Graph size | Trials | Failure sets/trial | AND-OR fails | Strategy loops |
|---|---|---|---|---|
| n=8 (24 edges) | 50 | 42,504 (exhaustive) | **0** | 1–796 |
| n=10 (30 edges) | 50 | 142,506 (exhaustive) | **0** | 43–1,360 |
| n=12 (36 edges) | 50 | ~155,000 (sampled) | **0** | 5–1,296 |
| n=14 (42 edges) | 50 | ~178,000 (sampled) | **0** | 5–1,003 |

**Critical finding:** AND-OR reachability never fails (the conjecture holds), but the simple circular strategies DO produce forwarding loops on up to ~1% of failure sets. This cleanly separates existence (supported) from construction (open).

---

## 7. Conclusions Document

**User:** Also write out your conclusions as a LaTeX file.

**Result:** Produced `computational-search-conclusions.tex` — a 4-page document covering all search results, complexity analysis, and implications. Updated with 6-regular graph findings.

---

## Overall Conclusions

1. **No counterexample found** across ~30 million failure sets on 200+ graphs spanning multiple families (dense random, multigraph, 6-regular) at k = 6 and k = 12.

2. **Simple strategies fail on sparse graphs.** Circular and interleaved-circular BSC strategies produce loops on 6-regular graphs (up to ~1% of failure sets), but AND-OR reachability confirms a valid strategy always exists.

3. **Edge sharing is the key difficulty.** Dense graphs (low sharing) are easy. 6-regular graphs (86–92% sharing) are where the conjecture is stressed.

4. **The conjecture is almost certainly true.** The difficulty is purely proof-theoretic — proving that BSC routing can find the good arborescence without header state.

5. **HDR vs BSC complexity gap.** HDR scales linearly (polynomial). BSC scales super-exponentially due to the consistency requirement across exponentially many failure patterns.

---

## Files Produced

| File | Description |
|---|---|
| `static-resilient-forwarding-proof.tex` | First proof (HDR, all k) |
| `static-forwarding-proof-extended.tex` | Extended proof (BSC k≤5, HDR all k, open problem) |
| `complexity-analysis.md` | Complexity of computing resilient tables |
| `computational-search-conclusions.tex` | LaTeX conclusions document |
| `counterexample-search/search_counterexample.py` | Initial k=6 search (dense graphs) |
| `counterexample-search/search_v2.py` | Sparse graph search |
| `counterexample-search/search_v3.py` | AND-OR reachability on multigraphs |
| `counterexample-search/search_k12.py` | k=12 star arborescences |
| `counterexample-search/search_k12_shared.py` | k=12 chain arborescences (shared) |
| `counterexample-search/search_k12_exhaustive.py` | k=12 exhaustive (2.5M sets) |
| `counterexample-search/search_6reg.py` | 6-regular graphs (main result) |
| `transcript.md` | This file |
File created successfully at: /home/apanda/code/gleam-as-emulation/graph proofs/transcript.md

Done. The transcript is at graph proofs/transcript.md and the updated conclusions PDF has been built with tectonic at graph proofs/computational-search-conclusions.pdf.