diff --git a/CslibFrontier.lean b/CslibFrontier.lean
index cb1d0673a3..9cf5bbe533 100644
--- a/CslibFrontier.lean
+++ b/CslibFrontier.lean
@@ -3892,6 +3892,7 @@ public import CslibFrontier.Computability.QueryComplexity.ApproximateDegree
 public import CslibFrontier.Computability.QueryComplexity.ApproximateDegree.Or
 public import CslibFrontier.Computability.QueryComplexity.BernsteinVazirani
 public import CslibFrontier.Computability.QueryComplexity.CertificateComposition
+public import CslibFrontier.Computability.QueryComplexity.Connectivity
 public import CslibFrontier.Computability.QueryComplexity.Degree
 public import CslibFrontier.Computability.QueryComplexity.DeutschJozsa
 public import CslibFrontier.Computability.QueryComplexity.Huang
@@ -5315,6 +5316,7 @@ public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Berge
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.CFI
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.CliqueCover
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.ColorRefinement
+public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Connectivity.Bridges
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Connectivity.Connected
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
 public import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Connectivity.VertexConnectivity
@@ -5419,6 +5421,7 @@ public import CslibFrontier.Foundations.Data.BitString.Discriminator
 public import CslibFrontier.Foundations.Data.BitString.Enumeration
 public import CslibFrontier.Foundations.Data.BitString.Flip
 public import CslibFrontier.Foundations.Data.BitString.FunctionTables
+public import CslibFrontier.Foundations.Data.BitString.Graph
 public import CslibFrontier.Foundations.Data.BitString.HalfSplit
 public import CslibFrontier.Foundations.Data.BitString.Hamming
 public import CslibFrontier.Foundations.Data.BitString.InitialTests
diff --git a/CslibFrontier/Computability/Circuit/Clique.lean b/CslibFrontier/Computability/Circuit/Clique.lean
index 04dd8665ed..3999ebc0f8 100644
--- a/CslibFrontier/Computability/Circuit/Clique.lean
+++ b/CslibFrontier/Computability/Circuit/Clique.lean
@@ -7,16 +7,15 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Cslib.Foundations.Data.BitString
+public import CslibFrontier.Foundations.Data.BitString.Graph
 public import Mathlib.Combinatorics.SimpleGraph.Clique
 public import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
-public import Mathlib.Data.Sym.Card
 
 /-!
 # The clique function
 
 A Boolean function of the possible edges of a graph on `n` vertices, the unordered pairs of distinct
-vertices (`Cslib.Circuits.Clique.Edge`), reads its input as a graph (`Cslib.Circuits.Clique.graph`).
+vertices (`Cslib.BitString.Graph.Edge`), reads its input as a graph (`Cslib.BitString.Graph.graph`).
 The `k`-clique function `Cslib.Circuits.clique n k` says whether that graph has a clique of `k`
 vertices.
 
@@ -31,10 +30,10 @@ circuit computing a separating function, not only of those computing `k`-clique.
 
 ## Main definitions
 
-* `Cslib.Circuits.Clique.Edge`, `Cslib.Circuits.Clique.edgeCount`,
-  `Cslib.Circuits.Clique.edgeEquiv`, `Cslib.Circuits.Clique.edge`: the possible edges, their count,
+* `Cslib.BitString.Graph.Edge`, `Cslib.BitString.Graph.edgeCount`,
+  `Cslib.BitString.Graph.edgeEquiv`, `Cslib.BitString.Graph.edge`: the possible edges, their count,
   their numbering, and the edge between two distinct vertices.
-* `Cslib.Circuits.Clique.graph`: the graph of an input.
+* `Cslib.BitString.Graph.graph`: the graph of an input.
 * `Cslib.Circuits.Clique.Contains`: the input contains all edges inside a set of vertices.
 * `Cslib.Circuits.Clique.CliqueSet`, `Cslib.Circuits.Clique.Coloring`: sets of `k` vertices and
   vertex colourings.
@@ -45,9 +44,9 @@ circuit computing a separating function, not only of those computing `k`-clique.
 
 ## Main results
 
-* `Cslib.Circuits.Clique.edgeCount_eq_choose`: there are `n.choose 2` possible edges.
+* `Cslib.BitString.Graph.edgeCount_eq_choose`: there are `n.choose 2` possible edges.
 * `Cslib.Circuits.clique_eq_true_iff`: the clique function in terms of `SimpleGraph.IsNClique`.
-* `Cslib.Circuits.Clique.graph_adj`: adjacency in the graph of an input.
+* `Cslib.BitString.Graph.graph_adj`: adjacency in the graph of an input.
 * `Cslib.Circuits.clique_ofFinset`, `Cslib.Circuits.clique_ofColoring`,
   `Cslib.Circuits.Clique.colorable_graph_ofColoring`: the test inputs.
 * `Cslib.Circuits.Clique.separates_clique`: `k`-clique separates the graphs with a `k`-clique from
@@ -60,27 +59,12 @@ circuit computing a separating function, not only of those computing `k`-clique.
 
 namespace Cslib.Circuits
 
+open BitString.Graph
+
 namespace Clique
 
 variable {n r : ℕ}
 
-/-- The possible edges of a graph on `n` vertices: unordered pairs of distinct vertices. -/
-abbrev Edge (n : ℕ) : Type := {e : Sym2 (Fin n) // ¬e.IsDiag}
-
-/-- The number of possible edges of a graph on `n` vertices. -/
-abbrev edgeCount (n : ℕ) : ℕ := Fintype.card (Edge n)
-
-/-- A graph on `n` vertices has `n.choose 2` possible edges. -/
-theorem edgeCount_eq_choose (n : ℕ) : edgeCount n = n.choose 2 := by
-  rw [edgeCount, Sym2.card_subtype_not_diag, Fintype.card_fin]
-
-/-- A numbering of the possible edges by the inputs of a circuit. -/
-noncomputable def edgeEquiv (n : ℕ) : Edge n ≃ Fin (edgeCount n) := Fintype.equivFin _
-
-/-- The graph of an input: its edges are the possible edges set to `true`. -/
-def graph (x : Fin (edgeCount n) → Bool) : SimpleGraph (Fin n) :=
-  SimpleGraph.fromEdgeSet {e | ∃ h : ¬e.IsDiag, x (edgeEquiv n ⟨e, h⟩) = true}
-
 /-- The input `x` contains all edges between the vertices of `s`. -/
 def Contains (x : Fin (edgeCount n) → Bool) (s : Finset (Fin n)) : Prop :=
   ∀ e : Edge n, e.1.toFinset ⊆ s → x (edgeEquiv n e) = true
@@ -90,24 +74,6 @@ noncomputable instance (x : Fin (edgeCount n) → Bool) (s : Finset (Fin n)) :
     Decidable (Contains x s) :=
   inferInstanceAs (Decidable (∀ _, _))
 
-/-- The edge between two distinct vertices. -/
-def edge {u v : Fin n} (h : u ≠ v) : Edge n := ⟨s(u, v), by simpa using h⟩
-
-/-- The endpoints of `edge h` are `{u, v}`. -/
-@[simp] theorem toFinset_edge {u v : Fin n} (h : u ≠ v) : (edge h).1.toFinset = {u, v} :=
-  Sym2.toFinset_mk_eq
-
-/-- The edge between `u` and `v` is the edge between `v` and `u`. -/
-theorem edge_comm {u v : Fin n} (h : u ≠ v) : edge h = edge (Ne.symm h) :=
-  Subtype.ext Sym2.eq_swap
-
-/-- Two distinct vertices are adjacent in the graph of an input exactly when the input sets the
-edge between them. -/
-theorem graph_adj {x : Fin (edgeCount n) → Bool} {u v : Fin n} (h : u ≠ v) :
-    (graph x).Adj u v ↔ x (edgeEquiv n (edge h)) = true := by
-  rw [graph, SimpleGraph.fromEdgeSet_adj]
-  exact ⟨fun ⟨⟨_, hx⟩, _⟩ => hx, fun hx => ⟨⟨_, hx⟩, h⟩⟩
-
 /-- Containing all edges inside a vertex set is antitone in the vertex set. -/
 theorem Contains.mono {x : Fin (edgeCount n) → Bool} {s t : Finset (Fin n)} (hst : s ⊆ t)
     (h : Contains x t) : Contains x s :=
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Approximator.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Approximator.lean
index eb15cdccea..0ba8e91501 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Approximator.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Approximator.lean
@@ -46,6 +46,8 @@ on the two kinds of test inputs, counted in
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone
 
 open Cslib.Circuits.Clique Finset
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Asymptotic.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Asymptotic.lean
index 42d4285311..9de194965f 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Asymptotic.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Asymptotic.lean
@@ -68,6 +68,8 @@ for circuits computing `k`-clique are their instances.
 
 public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone
 
 open Cslib.Circuits.Clique
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Approximator.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Approximator.lean
index fe6c910c80..4ba6e67e18 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Approximator.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Approximator.lean
@@ -57,6 +57,8 @@ at most `(r - 1) ^ j` minimal sets of at most `j ≤ l` vertices
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Closure
 
 open Cslib.Circuits.Clique Finset Relation
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Asymptotic.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Asymptotic.lean
index 5cad312dd4..82f640a432 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Asymptotic.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Asymptotic.lean
@@ -59,6 +59,8 @@ has more than `2 ^ (⌊√⌊√n⌋⌋ / 2)` gates, where `⌊√⌊√n⌋⌋
 
 public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone
 
 open Cslib.Circuits.Clique Finset
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/LowerBound.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/LowerBound.lean
index 805845de84..50223c3a90 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/LowerBound.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/LowerBound.lean
@@ -50,6 +50,8 @@ step bound; both change only constants. The bounds are explicit
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Closure
 
 open Cslib.Circuits.Clique Finset
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Negative.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Negative.lean
index a2e014b359..1457d893e1 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Negative.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Negative.lean
@@ -48,6 +48,8 @@ cruder bound suffices.
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Closure.Negative
 
 open Cslib.Circuits.Clique Finset Relation Cslib.Circuits.Monotone.Closure.Approximator
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Positive.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Positive.lean
index ac5240c24e..edefebb829 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Positive.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Closure/Positive.lean
@@ -45,6 +45,8 @@ what removes the square of the family bound from Razborov's estimate
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Closure.Positive
 
 open Cslib.Circuits.Clique Finset Cslib.Circuits.Monotone.Closure.Approximator
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Essential.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Essential.lean
index 53a8eb89b2..3e8ad3c9d0 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Essential.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Essential.lean
@@ -43,6 +43,8 @@ for it are not vacuous.
 -/
 public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits
 
 open Finset
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/LogarithmicPetals.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/LogarithmicPetals.lean
index 67b8e9c2b9..702b57ec9f 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/LogarithmicPetals.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/LogarithmicPetals.lean
@@ -55,6 +55,8 @@ against the monotone model beyond the literature.
 
 public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone
 
 open Cslib.Circuits.Clique
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/LowerBound.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/LowerBound.lean
index f80a1a35ce..05fb6e6ded 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/LowerBound.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/LowerBound.lean
@@ -53,6 +53,8 @@ feasible interpolation [Krajíček, Section 7][Krajicek1997].
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone
 
 open Cslib.Circuits.Clique Finset Approximator
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Negative.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Negative.lean
index dfaec9ee76..51d3d2705a 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Negative.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Negative.lean
@@ -60,6 +60,8 @@ least twice the number `w ^ 2` of pairs inside a set (`half_le_card_acceptedColo
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Negative
 
 open Cslib.Circuits.Clique Finset Relation Approximator
diff --git a/CslibFrontier/Computability/Circuit/Monotone/Clique/Positive.lean b/CslibFrontier/Computability/Circuit/Monotone/Clique/Positive.lean
index 604123cda6..e4dddb2c16 100644
--- a/CslibFrontier/Computability/Circuit/Monotone/Clique/Positive.lean
+++ b/CslibFrontier/Computability/Circuit/Monotone/Clique/Positive.lean
@@ -42,6 +42,8 @@ a conjunction of two approximators has at most `sunflowerBound p w ^ 2` pairs of
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Circuits.Monotone.Positive
 
 open Cslib.Circuits.Clique Finset Approximator
diff --git a/CslibFrontier/Computability/QueryComplexity/Connectivity.lean b/CslibFrontier/Computability/QueryComplexity/Connectivity.lean
new file mode 100644
index 0000000000..aea2034b65
--- /dev/null
+++ b/CslibFrontier/Computability/QueryComplexity/Connectivity.lean
@@ -0,0 +1,195 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import CslibFrontier.Computability.DecisionTree.Basic
+public import CslibFrontier.Foundations.Data.BitString.Graph
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+import CslibFrontier.Foundations.Combinatorics.SimpleGraph.Connectivity.Bridges
+import CslibFrontier.Foundations.Data.BitString.PartialAssignment
+
+/-!
+# Graph connectivity requires every edge query
+
+The total connectivity function on labelled undirected simple graphs has deterministic query
+complexity `n.choose 2`, one query per possible edge [AroraBarak07] (public draft, Theorem 11.4).
+Queries may be
+repeated. The bridge adversary answers false unless deleting the queried edge disconnects the
+remaining possible graph; confirmed edges remain bridges of that graph.
+
+The empty graph is disconnected and the one-vertex graph is connected, following Mathlib's
+conventions. Both functions have zero query complexity.
+
+## Main definitions
+
+* `Cslib.BitString.Graph.connectivity`: the total labelled simple-graph connectivity function.
+
+## Main results
+
+* `Cslib.BitString.Graph.complexity_connectivity`: its exact deterministic query complexity.
+* `Cslib.BitString.Graph.connectivity_zero`, `connectivity_one`: the empty and singleton cases.
+
+## References
+
+* [S. Arora and B. Barak, *Computational Complexity: A Modern Approach*, public draft,
+  Theorem 11.4][AroraBarak07]
+-/
+
+public section
+
+namespace Cslib.BitString.Graph
+
+/-- Whether the graph encoded by the edge bits is connected. The vertex set is all of `Fin n`,
+including isolated vertices. -/
+noncomputable def connectivity (n : ℕ) : BooleanFunction (edgeCount n) :=
+  fun x => @decide ((graph x).Connected) (Classical.propDecidable _)
+
+@[simp] theorem connectivity_eq_true {n : ℕ} {x : BitString (edgeCount n)} :
+    connectivity n x = true ↔ (graph x).Connected := by
+  simp [connectivity]
+
+@[simp] theorem connectivity_zero (x : BitString (edgeCount 0)) : connectivity 0 x = false := by
+  simp [connectivity, SimpleGraph.connected_iff]
+
+@[simp] theorem connectivity_one (x : BitString (edgeCount 1)) : connectivity 1 x = true :=
+  connectivity_eq_true.mpr SimpleGraph.Connected.of_subsingleton
+
+private def lowerGraph {n : ℕ} (ρ : PartialAssignment (Fin (edgeCount n))) :
+    SimpleGraph (Fin n) := graph (ρ.fill fun _ => false)
+
+private def upperGraph {n : ℕ} (ρ : PartialAssignment (Fin (edgeCount n))) :
+    SimpleGraph (Fin n) := graph (ρ.fill fun _ => true)
+
+private theorem lowerGraph_le_upperGraph {n : ℕ} (ρ : PartialAssignment (Fin (edgeCount n))) :
+    lowerGraph ρ ≤ upperGraph ρ := by
+  apply graph_mono
+  intro i hi
+  cases h : ρ i <;> simp_all [PartialAssignment.fill]
+
+private theorem free_card_le_depth {n : ℕ} (t : DecisionTree (Fin (edgeCount n)) Bool)
+    (ρ : PartialAssignment (Fin (edgeCount n)))
+    (ht : ∀ x, ρ.Agrees x → t.eval x = connectivity n x)
+    (hU : (upperGraph ρ).Connected)
+    (hbridge : ∀ e ∈ (lowerGraph ρ).edgeSet, (upperGraph ρ).IsBridge e) :
+    ρ.free.card ≤ t.depth := by
+  classical
+  induction t generalizing ρ with
+  | leaf b =>
+    have heval : connectivity n (ρ.fill fun _ => false) =
+        connectivity n (ρ.fill fun _ => true) :=
+      (ht (ρ.fill fun _ => false) (ρ.agrees_fill _)).symm.trans
+        (ht (ρ.fill fun _ => true) (ρ.agrees_fill _))
+    have hL : (lowerGraph ρ).Connected := connectivity_eq_true.mp
+      (heval.trans (connectivity_eq_true.mpr hU))
+    have heq : lowerGraph ρ = upperGraph ρ :=
+      hL.preconnected.eq_of_forall_isBridge (lowerGraph_le_upperGraph ρ) hbridge
+    have hwords := graph_injective heq
+    have hfree : ρ.free = ∅ := by
+      apply Finset.eq_empty_iff_forall_notMem.mpr
+      intro i hi
+      have h := congrFun hwords i
+      simp [PartialAssignment.fill, PartialAssignment.mem_free.mp hi] at h
+    simp [hfree]
+  | node i left right ihl ihr =>
+    have hdepthl : left.depth ≤ (DecisionTree.node i left right).depth := by
+      simp only [DecisionTree.depth_node]; omega
+    have hdepthr : right.depth ≤ (DecisionTree.node i left right).depth := by
+      simp only [DecisionTree.depth_node]; omega
+    cases hρi : ρ i with
+    | some b =>
+      have hquery (x) (hx : ρ.Agrees x) : x i = b := hx i b hρi
+      cases b with
+      | false =>
+        apply (ihl ρ (fun x hx => ?_) hU hbridge).trans hdepthl
+        simpa only [DecisionTree.eval_node, hquery x hx, Bool.cond_false] using ht x hx
+      | true =>
+        apply (ihr ρ (fun x hx => ?_) hU hbridge).trans hdepthr
+        simpa only [DecisionTree.eval_node, hquery x hx, Bool.cond_true] using ht x hx
+    | none =>
+      have hi : i ∈ ρ.free := PartialAssignment.mem_free.mpr hρi
+      have hbranch (b : Bool) (x) (hx : PartialAssignment.Agrees (Function.update ρ i (some b)) x) :
+          (cond b right left).eval x = connectivity n x := by
+        have hxi : x i = b := hx i b (Function.update_self _ _ _)
+        have hxρ : ρ.Agrees x := ((PartialAssignment.Extends.refl ρ).update_some hi b).agrees hx
+        cases b <;> simpa only [DecisionTree.eval_node, hxi, Bool.cond_false, Bool.cond_true]
+          using ht x hxρ
+      let e : Edge n := (edgeEquiv n).symm i
+      by_cases hb : (upperGraph ρ).IsBridge e.1
+      · have hUeq : upperGraph (Function.update ρ i (some true)) = upperGraph ρ := by
+          simp only [upperGraph, PartialAssignment.fill_update]
+          rw [Function.update_eq_self_iff.mpr
+            (PartialAssignment.fill_of_eq_none hρi (fun _ => true)).symm]
+        have hB : ∀ a ∈ (lowerGraph (Function.update ρ i (some true))).edgeSet,
+            (upperGraph (Function.update ρ i (some true))).IsBridge a := by
+          intro a ha
+          rw [hUeq]
+          have hdiag := (lowerGraph (Function.update ρ i (some true))).not_isDiag_of_mem_edgeSet ha
+          have hbit := (mem_edgeSet_graph _ ⟨a, hdiag⟩).mp ha
+          change PartialAssignment.fill (Function.update ρ i (some true)) (fun _ => false)
+            (edgeEquiv n ⟨a, hdiag⟩) = true at hbit
+          rw [PartialAssignment.fill_update] at hbit
+          by_cases hai : edgeEquiv n ⟨a, hdiag⟩ = i
+          · have hae : a = e.1 := congrArg Subtype.val
+              ((edgeEquiv n).injective (hai.trans (Equiv.apply_symm_apply _ _).symm))
+            exact hae ▸ hb
+          · rw [Function.update_of_ne hai] at hbit
+            exact hbridge a ((mem_edgeSet_graph _ ⟨a, hdiag⟩).mpr hbit)
+        have hbound := ihr _ (hbranch true) (hUeq ▸ hU) hB
+        rw [PartialAssignment.free_update] at hbound
+        have hcard := Finset.card_erase_add_one hi
+        simp only [DecisionTree.depth_node]
+        omega
+      · have hUeq : upperGraph (Function.update ρ i (some false)) =
+            (upperGraph ρ).deleteEdges {e.1} := by
+          simp only [upperGraph, PartialAssignment.fill_update, graph_update_false, e]
+        have hLeq : lowerGraph (Function.update ρ i (some false)) = lowerGraph ρ := by
+          simp only [lowerGraph, PartialAssignment.fill_update]
+          rw [Function.update_eq_self_iff.mpr
+            (PartialAssignment.fill_of_eq_none hρi (fun _ => false)).symm]
+        have hconn : (upperGraph (Function.update ρ i (some false))).Connected := by
+          rw [hUeq]
+          exact hU.preconnected.connected_deleteEdges_of_not_isBridge hb
+        have hB : ∀ a ∈ (lowerGraph (Function.update ρ i (some false))).edgeSet,
+            (upperGraph (Function.update ρ i (some false))).IsBridge a := by
+          intro a ha
+          rw [hLeq] at ha
+          rw [hUeq]
+          exact (hbridge a ha).anti (SimpleGraph.deleteEdges_le _)
+        have hbound := ihl _ (hbranch false) hconn hB
+        rw [PartialAssignment.free_update] at hbound
+        have hcard := Finset.card_erase_add_one hi
+        simp only [DecisionTree.depth_node]
+        omega
+
+/-- **Connectivity is evasive:** deciding connectivity of a labelled undirected simple graph
+requires every possible edge in the worst case [AroraBarak07] (public draft, Theorem 11.4). -/
+theorem complexity_connectivity (n : ℕ) :
+    DecisionTree.complexity (connectivity n) = n.choose 2 := by
+  classical
+  apply le_antisymm
+  · simpa only [Fintype.card_fin, edgeCount_eq_choose] using
+      DecisionTree.complexity_le_card (connectivity n)
+  · rw [← edgeCount_eq_choose]
+    apply DecisionTree.le_complexity_iff.mpr
+    intro t ht
+    by_cases hn : n = 0
+    · subst n
+      simp
+    · have : NeZero n := ⟨hn⟩
+      have hU : (upperGraph (PartialAssignment.empty :
+          PartialAssignment (Fin (edgeCount n)))).Connected := by
+        simp [upperGraph]
+      have hB : ∀ e ∈ (lowerGraph (PartialAssignment.empty :
+          PartialAssignment (Fin (edgeCount n)))).edgeSet,
+          (upperGraph (PartialAssignment.empty :
+            PartialAssignment (Fin (edgeCount n)))).IsBridge e := by
+        simp [lowerGraph]
+      simpa only [PartialAssignment.free_empty, Finset.card_univ, Fintype.card_fin] using
+        free_card_le_depth t PartialAssignment.empty (fun x _ => ht x) hU hB
+
+end Cslib.BitString.Graph
diff --git a/CslibFrontier/Foundations/Combinatorics/SimpleGraph/Connectivity/Bridges.lean b/CslibFrontier/Foundations/Combinatorics/SimpleGraph/Connectivity/Bridges.lean
new file mode 100644
index 0000000000..f40371df7d
--- /dev/null
+++ b/CslibFrontier/Foundations/Combinatorics/SimpleGraph/Connectivity/Bridges.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate (Mathlib, `Mathlib/Combinatorics/SimpleGraph/Connectivity/Bridges.lean`)
+
+public import CslibFrontier.Init
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+
+/-!
+# Spanning subgraphs of bridges
+
+A preconnected spanning subgraph whose edges are all bridges of the ambient graph equals that
+graph. An additional ambient edge would close a subgraph path to a cycle containing a bridge.
+The statement requires neither finiteness nor a nonempty vertex type.
+
+## Main results
+
+* `SimpleGraph.Preconnected.eq_of_forall_isBridge`: a preconnected spanning subgraph of
+  ambient bridges is the entire graph.
+-/
+
+public section
+
+namespace SimpleGraph
+
+/-- A preconnected spanning subgraph consisting of bridges of the ambient graph
+is the whole ambient graph. No finiteness or nonemptiness hypothesis is needed. -/
+theorem Preconnected.eq_of_forall_isBridge
+    {V : Type*} {H G : SimpleGraph V}
+    (hH : H.Preconnected) (hHG : H ≤ G)
+    (hbridge : ∀ e ∈ H.edgeSet, G.IsBridge e) : H = G := by
+  classical
+  apply le_antisymm hHG
+  intro u v huv
+  by_contra hnot
+  obtain ⟨p, hp⟩ := hH.exists_isPath u v
+  have hmiss : s(v, u) ∉ (p.mapLe hHG).edges := by
+    rw [Walk.edges_mapLe_eq_edges]
+    intro he
+    exact hnot (H.mem_edgeSet.mp (p.edges_subset_edgeSet he)).symm
+  have hc : (Walk.cons huv.symm (p.mapLe hHG)).IsCycle :=
+    Path.cons_isCycle ⟨p.mapLe hHG, hp.mapLe hHG⟩ huv.symm hmiss
+  obtain ⟨e, he⟩ := p.edges.exists_mem_of_ne_nil (by
+    intro hempty
+    exact huv.ne (Walk.Nil.eq (Walk.edges_eq_nil.mp hempty)))
+  apply (hbridge e (p.edges_subset_edgeSet he)).notMem_edges_of_isCycle hc
+  simp only [Walk.edges_cons, List.mem_cons, Walk.edges_mapLe_eq_edges]
+  exact Or.inr he
+
+end SimpleGraph
diff --git a/CslibFrontier/Foundations/Data/BitString/Graph.lean b/CslibFrontier/Foundations/Data/BitString/Graph.lean
new file mode 100644
index 0000000000..3756ccf751
--- /dev/null
+++ b/CslibFrontier/Foundations/Data/BitString/Graph.lean
@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger, Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger, Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import CslibFrontier.Init
+public import Cslib.Foundations.Data.BitString
+public import Mathlib.Combinatorics.SimpleGraph.DeleteEdges
+public import Mathlib.Data.Sym.Card
+
+/-!
+# Graphs encoded by edge bits
+
+A simple graph on `n` labelled vertices is encoded by one Boolean coordinate for each unordered
+pair of distinct vertices. `edgeEquiv` numbers these coordinates without changing the layout
+formerly used by the clique function. The common encoding supports graph properties such as
+clique containment and connectivity without importing either application.
+
+## Main definitions
+
+* `Cslib.BitString.Graph.Edge`, `edgeCount`, `edgeEquiv`: the possible edges and their numbering.
+* `Cslib.BitString.Graph.graph`, `ofGraph`: graph/edge-word conversion.
+
+## Main results
+
+* `Cslib.BitString.Graph.edgeCount_eq_choose`: the coordinate count is `n.choose 2`.
+* `Cslib.BitString.Graph.graph_adj`: adjacency is the corresponding edge bit.
+* `Cslib.BitString.Graph.graph_ofGraph`, `ofGraph_graph`: both conversions are inverse.
+
+The encoding and its original lemmas were extracted from Samuel Schlesinger's clique module.
+-/
+
+public section
+
+namespace Cslib.BitString.Graph
+
+variable {n : ℕ}
+
+/-- The possible edges of a graph on `n` vertices: unordered pairs of distinct vertices. -/
+abbrev Edge (n : ℕ) : Type := {e : Sym2 (Fin n) // ¬e.IsDiag}
+
+/-- The number of possible edges of a graph on `n` vertices. -/
+abbrev edgeCount (n : ℕ) : ℕ := Fintype.card (Edge n)
+
+/-- A graph on `n` vertices has `n.choose 2` possible edges. -/
+theorem edgeCount_eq_choose (n : ℕ) : edgeCount n = n.choose 2 := by
+  rw [edgeCount, Sym2.card_subtype_not_diag, Fintype.card_fin]
+
+/-- A numbering of the possible edges by the inputs of a circuit. -/
+noncomputable def edgeEquiv (n : ℕ) : Edge n ≃ Fin (edgeCount n) := Fintype.equivFin _
+
+/-- The graph of an input: its edges are the possible edges set to `true`. -/
+@[expose] def graph (x : Fin (edgeCount n) → Bool) : SimpleGraph (Fin n) :=
+  SimpleGraph.fromEdgeSet {e | ∃ h : ¬e.IsDiag, x (edgeEquiv n ⟨e, h⟩) = true}
+
+/-- The edge between two distinct vertices. -/
+@[expose] def edge {u v : Fin n} (h : u ≠ v) : Edge n := ⟨s(u, v), by simpa using h⟩
+
+/-- The endpoints of `edge h` are `{u, v}`. -/
+@[simp] theorem toFinset_edge {u v : Fin n} (h : u ≠ v) : (edge h).1.toFinset = {u, v} :=
+  Sym2.toFinset_mk_eq
+
+/-- The edge between `u` and `v` is the edge between `v` and `u`. -/
+theorem edge_comm {u v : Fin n} (h : u ≠ v) : edge h = edge (Ne.symm h) :=
+  Subtype.ext Sym2.eq_swap
+
+/-- Two distinct vertices are adjacent in the graph of an input exactly when the input sets the
+edge between them. -/
+theorem graph_adj {x : Fin (edgeCount n) → Bool} {u v : Fin n} (h : u ≠ v) :
+    (graph x).Adj u v ↔ x (edgeEquiv n (edge h)) = true := by
+  rw [graph, SimpleGraph.fromEdgeSet_adj]
+  exact ⟨fun ⟨⟨_, hx⟩, _⟩ => hx, fun hx => ⟨⟨_, hx⟩, h⟩⟩
+
+/-- A possible edge belongs to the encoded graph exactly when its bit is set. -/
+@[simp] theorem mem_edgeSet_graph (x : Fin (edgeCount n) → Bool) (e : Edge n) :
+    e.1 ∈ (graph x).edgeSet ↔ x (edgeEquiv n e) = true := by
+  simp [graph, SimpleGraph.edgeSet_fromEdgeSet, e.property]
+
+/-- Distinct edge words encode distinct graphs. -/
+theorem graph_injective : Function.Injective (graph (n := n)) := by
+  intro x y h
+  funext i
+  have hi : x i = true ↔ y i = true := by
+    simpa only [Equiv.apply_symm_apply] using
+      (mem_edgeSet_graph x ((edgeEquiv n).symm i)).symm.trans
+        ((congrArg (fun G : SimpleGraph (Fin n) =>
+          ((edgeEquiv n).symm i).1 ∈ G.edgeSet) h).to_iff.trans
+          (mem_edgeSet_graph y ((edgeEquiv n).symm i)))
+  cases hx : x i <;> cases hy : y i <;> simp_all
+
+/-- Setting more edge bits preserves graph inclusion. -/
+theorem graph_mono {x y : Fin (edgeCount n) → Bool}
+    (h : ∀ i, x i = true → y i = true) : graph x ≤ graph y := by
+  intro u v huv
+  exact (graph_adj huv.ne).2 (h _ ((graph_adj huv.ne).1 huv))
+
+@[simp] theorem graph_false : graph (n := n) (fun _ => false) = ⊥ := by
+  ext u v
+  by_cases h : u = v
+  · subst v; simp
+  · simp [graph_adj h]
+
+@[simp] theorem graph_true : graph (n := n) (fun _ => true) = ⊤ := by
+  ext u v
+  by_cases h : u = v
+  · subst v; simp
+  · simp [graph_adj h, h]
+
+/-- Clearing a coordinate deletes precisely that edge. -/
+theorem graph_update_false (x : Fin (edgeCount n) → Bool) (i : Fin (edgeCount n)) :
+    graph (Function.update x i false) =
+      (graph x).deleteEdges {((edgeEquiv n).symm i).1} := by
+  apply SimpleGraph.edgeSet_injective
+  ext e
+  by_cases he : e.IsDiag
+  · simp [he]
+  · rw [mem_edgeSet_graph _ ⟨e, he⟩, SimpleGraph.edgeSet_deleteEdges]
+    simp only [Set.mem_sdiff, Set.mem_singleton_iff, mem_edgeSet_graph x ⟨e, he⟩]
+    by_cases hi : edgeEquiv n ⟨e, he⟩ = i
+    · have hei : e = ((edgeEquiv n).symm i).1 :=
+        congrArg Subtype.val ((edgeEquiv n).injective (hi.trans (Equiv.apply_symm_apply _ _).symm))
+      simp [hei]
+    · have hei : e ≠ ((edgeEquiv n).symm i).1 := by
+        intro hh
+        apply hi
+        rw [show (⟨e, he⟩ : Edge n) = (edgeEquiv n).symm i from Subtype.ext hh,
+          Equiv.apply_symm_apply]
+      simp [hi, hei]
+
+/-- The edge word of a labelled simple graph, in the same numbering as `graph`. -/
+noncomputable def ofGraph (G : SimpleGraph (Fin n)) : BitString (edgeCount n) :=
+  fun i => @decide (((edgeEquiv n).symm i).1 ∈ G.edgeSet) (Classical.propDecidable _)
+
+/-- Encoding a graph and reading its edge word recovers the graph. -/
+@[simp] theorem graph_ofGraph (G : SimpleGraph (Fin n)) : graph (ofGraph G) = G := by
+  ext u v
+  by_cases huv : u = v
+  · subst v; simp
+  · rw [graph_adj huv]
+    simp only [ofGraph, Equiv.symm_apply_apply, decide_eq_true_eq]
+    exact G.mem_edgeSet
+
+/-- Encoding an edge word's graph recovers the edge word. -/
+@[simp] theorem ofGraph_graph (x : BitString (edgeCount n)) : ofGraph (graph x) = x :=
+  graph_injective (graph_ofGraph (graph x))
+
+end Cslib.BitString.Graph
diff --git a/CslibFrontier/Logics/Propositional/CliqueColoring.lean b/CslibFrontier/Logics/Propositional/CliqueColoring.lean
index bb83256a61..aad7d90772 100644
--- a/CslibFrontier/Logics/Propositional/CliqueColoring.lean
+++ b/CslibFrontier/Logics/Propositional/CliqueColoring.lean
@@ -17,7 +17,7 @@ import Mathlib.Data.Finset.Sort
 
 Krajíček's formulas `Clique_{n,k}(p, q)` and `Color_{n,r}(p, r)` [Krajíček, Definition 7.1]
 [Krajicek1997] share the variables `p` of the possible edges of a graph on `n` vertices, numbered
-as the inputs of the clique function (`Cslib.Circuits.Clique.edgeEquiv`). The clique formula
+as the inputs of the clique function (`Cslib.BitString.Graph.edgeEquiv`). The clique formula
 (`Cslib.Logic.PL.CNF.clique`) has a variable `q (u, i)` for each `u : Fin k` and vertex `i`, read
 as "the `u`-th member of the clique is `i`", and says that
 
@@ -74,6 +74,8 @@ formula, which is what monotone feasible interpolation needs.
 
 @[expose] public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Logic.PL
 
 open Cslib.Circuits Cslib.Circuits.Clique
diff --git a/CslibFrontier/Logics/Propositional/Resolution/CliqueColoring.lean b/CslibFrontier/Logics/Propositional/Resolution/CliqueColoring.lean
index a4bbaf891d..78e1b573be 100644
--- a/CslibFrontier/Logics/Propositional/Resolution/CliqueColoring.lean
+++ b/CslibFrontier/Logics/Propositional/Resolution/CliqueColoring.lean
@@ -87,6 +87,8 @@ lines.
 
 public section
 
+open Cslib.BitString.Graph
+
 namespace Cslib.Logic.PL
 
 open Cslib.Circuits Cslib.Circuits.Clique
diff --git a/CslibFrontierResults/Entries.lean b/CslibFrontierResults/Entries.lean
index 275bd7c274..696cd9d762 100644
--- a/CslibFrontierResults/Entries.lean
+++ b/CslibFrontierResults/Entries.lean
@@ -123,6 +123,7 @@ import CslibFrontier.Computability.MCSP.PartialHardness.Reduction
 import CslibFrontier.Computability.PCP.Approximation.UniqueGames.Complexity
 import CslibFrontier.Computability.PCP.Completeness
 import CslibFrontier.Computability.PolyTime.LinearAlgebra.RationalElimination
+import CslibFrontier.Computability.QueryComplexity.Connectivity
 import CslibFrontier.Computability.QueryComplexity.Quantum.NayakWuConsequences
 import CslibFrontier.Computability.QueryComplexity.Quantum.PermutationInversion
 import CslibFrontier.Computability.QueryComplexity.Quantum.SpectralAdversary
@@ -231,6 +232,21 @@ left out: they are original results, which `results/README.md` admits only once
 have an explicit representation.
 -/
 
+register_result "connectivity-evasiveness" where
+  title := "Graph connectivity requires every possible edge query"
+  topic := "query complexity"
+  sources := [
+    { paper := AroraBarak07, theorem := "Theorem 11.4 (2007 public draft)",
+      locator := "2007 public draft, PDF 228 / printed p. 212" }
+  ]
+  theorems := [Cslib.BitString.Graph.complexity_connectivity]
+  scope := "For every m, the total connectivity function on labelled undirected simple graphs \
+    on Fin m has deterministic decision-tree complexity m.choose 2. Each input coordinate \
+    represents one unordered pair of distinct vertices; repeated queries are allowed. Mathlib \
+    regards the empty graph as disconnected and the one-vertex graph as connected, and both \
+    functions have complexity zero. No graph promise, arbitrary edge-permutation symmetry, \
+    randomized bound or machine-runtime bound is asserted."
+
 register_result "cook-levin" where
   title := "Cook–Levin: SAT is NP-complete"
   topic := "NP-completeness"
diff --git a/CslibFrontierTests/ConnectivityEvasiveness.lean b/CslibFrontierTests/ConnectivityEvasiveness.lean
new file mode 100644
index 0000000000..52e14744e3
--- /dev/null
+++ b/CslibFrontierTests/ConnectivityEvasiveness.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+import CslibFrontier.Computability.QueryComplexity.Connectivity
+import Mathlib.Combinatorics.SimpleGraph.Hasse
+
+/-! Concrete edge-query clients, including the empty graph and two graphs with the same number
+of edges but different connectivity. The theorem also applies to trees that repeat a query. -/
+
+open Cslib Cslib.BitString.Graph
+
+namespace CslibFrontierTests.ConnectivityEvasiveness
+
+example (x : BitString (edgeCount 0)) : connectivity 0 x = false := connectivity_zero x
+example (x : BitString (edgeCount 1)) : connectivity 1 x = true := connectivity_one x
+example : DecisionTree.complexity (connectivity 0) = 0 := complexity_connectivity 0
+example : DecisionTree.complexity (connectivity 1) = 0 := complexity_connectivity 1
+example : DecisionTree.complexity (connectivity 2) = 1 := complexity_connectivity 2
+example : DecisionTree.complexity (connectivity 3) = 3 := complexity_connectivity 3
+example : DecisionTree.complexity (connectivity 4) = 6 := complexity_connectivity 4
+
+example : connectivity 3 (ofGraph (SimpleGraph.pathGraph 3)) = true := by
+  rw [connectivity_eq_true, graph_ofGraph]
+  exact SimpleGraph.connected_pathGraph_add_one 2
+
+private def triangleWithIsolate : SimpleGraph (Fin 4) where
+  Adj u v := u ≠ v ∧ u < 3 ∧ v < 3
+  symm := ⟨fun _ _ h => ⟨h.1.symm, h.2.2, h.2.1⟩⟩
+  loopless := ⟨fun _ h => h.1 rfl⟩
+
+private instance : DecidableRel triangleWithIsolate.Adj :=
+  fun _ _ => inferInstanceAs (Decidable (_ ≠ _ ∧ _ < 3 ∧ _ < 3))
+
+example : (SimpleGraph.pathGraph 4).edgeFinset.card = 3 := by decide
+example : triangleWithIsolate.edgeFinset.card = 3 := by decide
+
+example : connectivity 4 (ofGraph (SimpleGraph.pathGraph 4)) = true := by
+  rw [connectivity_eq_true, graph_ofGraph]
+  exact SimpleGraph.connected_pathGraph_add_one 3
+
+example : connectivity 4 (ofGraph triangleWithIsolate) = false := by
+  apply Bool.eq_false_iff.mpr
+  intro htrue
+  have hc : triangleWithIsolate.Connected := by
+    simpa only [graph_ofGraph] using connectivity_eq_true.mp htrue
+  have hzero : triangleWithIsolate.neighborSet 3 = ∅ := by
+    ext v
+    simp [SimpleGraph.mem_neighborSet, triangleWithIsolate]
+  exact SimpleGraph.not_reachable_of_neighborSet_left_eq_empty
+    (by decide : (3 : Fin 4) ≠ 0) hzero (hc 3 0)
+
+/-- A redundant first query may be added to an optimal tree; both remaining queries read that
+same unique possible edge. Its depth is two, while connectivity's minimum depth is one. -/
+example : ∃ t : DecisionTree (Fin (edgeCount 2)) Bool,
+    t.Computes (connectivity 2) ∧ t.depth = 2 := by
+  obtain ⟨t, ht, hd⟩ := DecisionTree.exists_computes_depth_eq_complexity (connectivity 2)
+  let i : Fin (edgeCount 2) := ⟨0, by rw [edgeCount_eq_choose]; decide⟩
+  refine ⟨.node i t t, ?_, ?_⟩
+  · intro x
+    simp only [DecisionTree.eval_node, Bool.cond_self]
+    exact ht x
+  · rw [DecisionTree.depth_node, max_self, hd, complexity_connectivity]
+    rfl
+
+end CslibFrontierTests.ConnectivityEvasiveness
diff --git a/CslibFrontierTests/MonotoneCliqueClosure.lean b/CslibFrontierTests/MonotoneCliqueClosure.lean
index 71005154bb..06215acf7c 100644
--- a/CslibFrontierTests/MonotoneCliqueClosure.lean
+++ b/CslibFrontierTests/MonotoneCliqueClosure.lean
@@ -22,6 +22,7 @@ more than `2 ^ 512 / 2` lines.
 
 namespace CslibFrontierTests.MonotoneCliqueClosure
 
+open Cslib.BitString.Graph
 open Cslib Cslib.Circuits Cslib.Circuits.Clique Cslib.Logic.PL
 
 /-- Two singletons form an implication-minimal family for `3`. -/
diff --git a/CslibFrontierTests/MonotoneCliqueParameters.lean b/CslibFrontierTests/MonotoneCliqueParameters.lean
index 94162096b7..6a871f5c8a 100644
--- a/CslibFrontierTests/MonotoneCliqueParameters.lean
+++ b/CslibFrontierTests/MonotoneCliqueParameters.lean
@@ -12,6 +12,7 @@ The second supplies a finite minimum complexity at a vertex count below `k ^ 4`.
 
 namespace CslibFrontierTests.MonotoneCliqueParameters
 
+open Cslib.BitString.Graph
 open Cslib Cslib.Circuits Cslib.Circuits.Clique Cslib.Circuits.Monotone
 
 /-- A real monotone implementation exists, and the stronger bound applies to it. -/
diff --git a/CslibFrontierTests/ProofComplexity/CliqueColoring.lean b/CslibFrontierTests/ProofComplexity/CliqueColoring.lean
index d79de8d66c..6de96a4643 100644
--- a/CslibFrontierTests/ProofComplexity/CliqueColoring.lean
+++ b/CslibFrontierTests/ProofComplexity/CliqueColoring.lean
@@ -29,6 +29,7 @@ four vertices separates, so it has at least `C(4, 2) - 1 = 5` gates.
 
 namespace CslibFrontierTests.ProofComplexity.CliqueColoring
 
+open Cslib.BitString.Graph
 open Cslib Cslib.Circuits Cslib.Circuits.Clique Cslib.Logic.PL
 
 /-- Every pair of vertices is adjacent in the graph of the all-`true` input. -/
diff --git a/manual/circuits-logic-and-other-models/query-and-communication.md b/manual/circuits-logic-and-other-models/query-and-communication.md
index d18b610fba..f0579e1a63 100644
--- a/manual/circuits-logic-and-other-models/query-and-communication.md
+++ b/manual/circuits-logic-and-other-models/query-and-communication.md
@@ -26,6 +26,37 @@ The [zero-error module](../../CslibFrontier/Computability/QueryComplexity/Random
 
 Quantum queries use arbitrary input-independent isometries and a controlled phase oracle, charging only oracle uses. Their definitions and BBBV/polynomial/adversary/Grover endpoints are described in [algebraic and quantum models](algebraic-and-quantum.md). That chapter also covers the exponential separation between quantum and randomized queries for Simon's problem, whose classical side is the randomized decision-tree lower bound [simon_randomized_lower_bound](../../CslibFrontier/Computability/QueryComplexity/Simon.lean). It also covers Deutsch–Jozsa. The deterministic bound `N/2 + 1` is in [DeutschJozsa](../../CslibFrontier/Computability/QueryComplexity/DeutschJozsa.lean). Three random queries with error `1/4` on the promise ([Randomized/DeutschJozsa](../../CslibFrontier/Computability/QueryComplexity/Randomized/DeutschJozsa.lean), through `RandomizedDecisionTree.errorProb_uniformMixture`) show that its quantum advantage holds only for exact algorithms.
 
+## Connectivity edge queries
+
+Import [QueryComplexity/Connectivity](../../CslibFrontier/Computability/QueryComplexity/Connectivity.lean)
+and open `Cslib.BitString.Graph`. The function `connectivity m` reads a labelled undirected simple
+graph on all vertices of `Fin m`, including isolated vertices. Its input has one coordinate for
+each unordered pair of distinct vertices. `complexity_connectivity m` proves
+$D(\mathrm{connectivity}_m)=\binom m2$ for every `m`. Queries may repeat, and local computation is
+free; this is a deterministic worst-case query bound, with no graph promise or runtime claim.
+The empty graph is disconnected and the single-vertex graph is connected, so both corresponding
+functions have complexity zero.
+
+The shared [edge encoding](../../CslibFrontier/Foundations/Data/BitString/Graph.lean) supplies `Edge`,
+`edgeCount`, `edgeEquiv`, `graph` and `graph_adj`, formerly in `Cslib.Circuits.Clique`. Import this
+module and open `Cslib.BitString.Graph` when migrating a clique client. The definitions preserve
+the old coordinate numbering; `ofGraph G` turns a labelled graph into its edge word, and
+`graph_ofGraph` and `ofGraph_graph` discharge the conversions. The numbering and graph-property
+functions are noncomputable Lean definitions; the theorem concerns decision-tree query counts.
+
+The [complete checked client](../../CslibFrontierTests/ConnectivityEvasiveness.lean) covers zero
+through four vertices, graph/word conversion and a redundant repeated query. It also contrasts
+a connected four-vertex path and a triangle with an isolated vertex: both have three edges, so
+connectivity cannot be replaced by a function of edge count alone. From the repository root run:
+
+```bash
+lake build CslibFrontierTests.ConnectivityEvasiveness --wfail --iofail
+```
+
+The bridge adversary behind the lower bound answers false whenever deleting an unqueried edge
+preserves possible connectivity; otherwise it answers true. All confirmed edges remain bridges
+of the possible graph, so a correct tree cannot stop while any edge remains free.
+
 ## Adaptive cell-probe trees and schemes
 
 [`CslibFrontier.Computability.CellProbe.Defs`](../../CslibFrontier/Computability/CellProbe/Defs.lean), [`CslibFrontier.Computability.CellProbe.DecisionTree`](../../CslibFrontier/Computability/CellProbe/DecisionTree.lean), and [`CslibFrontier.Computability.CellProbe.Randomized`](../../CslibFrontier/Computability/CellProbe/Randomized.lean) formalize the adaptive cell-probe model (`Cslib.CellProbe`), originating in Minsky and Papert and developed in dynamic form by Fredman and static form by Yao. In a time-invariant deterministic `Scheme`, persistent state between operations consists solely of `S` cells of `w`-bit words (`Mem S w := Fin S → Fin (2 ^ w)`), with no persistent registers across operation boundaries; `IndexedScheme` is a **time-aware relaxation** whose `step` additionally receives the global operation index `t : ℕ` (a free clock outside cell memory). Each deterministic operation is an adaptive read/write decision tree `ProbeTree S w α` (`OracleComp (@ProbeOp.Result S w) α`): reading cell `i` branches `2 ^ w`-ways on `m i`, writing `v` updates cell `i` and returns `PUnit`, reads and writes are charged separately at one probe each (at most twice the cost of combined read-and-write nodes), and local computation and initial memory (`Scheme.init`, equivalent for deterministic schemes to `zeroMem` via uncharged XOR relabeling) charge zero probes.
diff --git a/results/README.md b/results/README.md
index 883156fa7d..a2d43d7cd5 100644
--- a/results/README.md
+++ b/results/README.md
@@ -18,6 +18,8 @@ The [Arora–Barak 2007 draft audit](arora-barak-2007.md) records a source-pinne
 coverage comparison, including missing endpoints, partial matches and source/model problems.
 Its chapters 6–7 records distinguish native circuit/randomized endpoints from uniformity,
 expected-time and expander-concentration gaps and identify literal source defects.
+Its Chapter 11 connectivity milestone records the exact total edge-query lower bound and its
+empty-graph conventions; it does not establish the other chapter endpoints.
 Its chapters 8–10 record distinguishes constant-round protocols, counting-oracle interfaces
 and quantitative crypto bounds. Its Chapter 14 record includes a checked degree obstruction to the draft's literal
 circuit-to-determinant statement.
diff --git a/results/arora-barak-2007.md b/results/arora-barak-2007.md
index f8d050970a..42fe7a66bb 100644
--- a/results/arora-barak-2007.md
+++ b/results/arora-barak-2007.md
@@ -266,6 +266,27 @@ Snapshot: `b91d5151fd7dc665a5e3efcb466077caf44e690d` (2026-11-12), CSLib pin
 - Exact finite query-measure inequalities are available without a machine-encoding translation.
 - Bounded-error depth minimax and zero-error expected cost are distinct contracts; their separate APIs do not by themselves prove 11.17.
 
+### Connectivity evasiveness after the audited snapshot
+
+This later formalization fills the historical snapshot’s connectivity gap.
+Theorem 11.4 (printed 212 / PDF 228 in the source-pinned public draft) is formalized by
+`Cslib.BitString.Graph.complexity_connectivity` in
+[QueryComplexity/Connectivity](../CslibFrontier/Computability/QueryComplexity/Connectivity.lean):
+for every vertex count $m$, the total labelled undirected simple-graph connectivity function has
+exact deterministic edge-query complexity $\binom m2$. Repeated queries are allowed. The proof
+uses the draft's bridge adversary with existing partial assignments and Mathlib graph paths;
+its graph/edge-word representation is the shared encoding extracted from the clique library.
+
+The result includes the conventions that the empty graph is disconnected and the one-vertex
+graph is connected; both functions have complexity zero. The
+[checked clients](../CslibFrontierTests/ConnectivityEvasiveness.lean) include a connected path and
+a triangle with an isolated vertex, each with three edges, so the claim is not a surrogate based
+only on edge count. It does not assert a randomized or machine-runtime lower bound. This is one
+formalized mathematical endpoint with validation, review and integration tracked in #4984.
+The remaining Chapter 11 theory objectives, including
+[expected-cost Yao minimax](https://github.com/cslib-community/cslib-frontier/issues/5005), and the
+broader #4711 objective remain open; the chapter audit is recorded above.
+
 ## Chapter 12: communication complexity
 
 Snapshot: `b91d5151fd7dc665a5e3efcb466077caf44e690d` (2026-11-12), CSLib pin