{
"skill": "tectonic",
"args": "/home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.tex"
}Base directory for this skill: /home/apanda/code/gleam-as-emulation/.claude/skills/tectonic
Use tectonic when possible, however if that fails use latexmk.
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
To build a file using latexmk call
latexmk -pdf <latex file>
ARGUMENTS: /home/apanda/code/gleam-as-emulation/graph proofs/computational-search-conclusions.tex
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.
# 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.