# P2570: Leaf complexity of six-vertex graph connectivity

- ID: `P2570`
- Reference: `connectivity-decision-tree-six-leaves`
- Page: https://theoremdb.org/statements/P2570
- Record maturity: Reviewed problem with recorded work

## Problem

An algorithm learns an unknown simple graph on six labeled vertices by adaptively querying edges and must decide whether the graph is connected. What is the minimum possible number \(L_6\) of leaves in its deterministic binary decision tree?

### Remarks

- **Remark.** Each internal node queries one of the 15 possible edges and branches on absence or presence.
- **Remark.** A leaf is labeled connected or disconnected and must be correct for every graph consistent with its path.

### What counts as a solution

- Exhibit a correct decision tree and a lower-bound certificate proving its leaf count is minimal.

## The answer

An exact recurrence over partial edge assignments gives a 1,693-leaf policy and a matching lower certificate. [3](#reference-3)

**Review status:** Reproduced.

**Lean verification:** not Lean-verified.

### Verification

Let \(P\) be the set of queried-present edges and \(A\) the set of queried-absent edges. Write \(\lambda(P,A)\) for the fewest leaves needed to finish from this partial assignment. Monotonicity gives two terminal cases. If \((V,P)\) is connected, every completion is connected. If \((V,K_6\setminus A)\) is disconnected, every completion is disconnected. A terminal state has value 1.

At every remaining state, the root of a continuation queries some unknown edge. Its two branches are independent subproblems, so
\[
\lambda(P,A)=\min_{e\notin P\cup A}
\bigl(\lambda(P,A\cup\{e\})+\lambda(P\cup\{e\},A)\bigr).
\]
This recurrence is an equality. Each query supplies an upper bound by joining optimal child trees. Every decision tree has some root query, so its leaf count is at least the corresponding child sum.

A permutation of the six vertices preserves the recurrence. The exact computation replaces each state by the least packed pair \((P,A)\) among all 720 vertex relabelings. It evaluates every query choice, records an attaining edge, and obtains
\[
\lambda(\varnothing,\varnothing)=1693.
\]
The resulting certificate contains 23,352 canonical states. A separate pass checks each record. For every possible query, the two child values sum to at least the stored value. The recorded query attains equality. Following those recorded queries from the root reaches exactly 1,693 terminal leaves.

For a labeled state, choose a vertex permutation carrying it to its canonical representative, read the stored canonical edge, and query the inverse image of that edge. Repeating this after each answer reconstructs an optimal policy. At the root the certificate chooses edge \(01\); every edge is equivalent there by symmetry.

## Work

### Proof and evidence for the resolution

**Computation 1 (The minimum decision-tree leaf count is 1,693).** An exact recurrence over partial edge assignments gives a 1,693-leaf policy and a matching lower certificate.

Let \(P\) be the set of queried-present edges and \(A\) the set of queried-absent edges. Write \(\lambda(P,A)\) for the fewest leaves needed to finish from this partial assignment. Monotonicity gives two terminal cases. If \((V,P)\) is connected, every completion is connected. If \((V,K_6\setminus A)\) is disconnected, every completion is disconnected. A terminal state has value 1.

At every remaining state, the root of a continuation queries some unknown edge. Its two branches are independent subproblems, so
\[
\lambda(P,A)=\min_{e\notin P\cup A}
\bigl(\lambda(P,A\cup\{e\})+\lambda(P\cup\{e\},A)\bigr).
\]
This recurrence is an equality. Each query supplies an upper bound by joining optimal child trees. Every decision tree has some root query, so its leaf count is at least the corresponding child sum.

A permutation of the six vertices preserves the recurrence. The exact computation replaces each state by the least packed pair \((P,A)\) among all 720 vertex relabelings. It evaluates every query choice, records an attaining edge, and obtains
\[
\lambda(\varnothing,\varnothing)=1693.
\]
The resulting certificate contains 23,352 canonical states. A separate pass checks each record. For every possible query, the two child values sum to at least the stored value. The recorded query attains equality. Following those recorded queries from the root reaches exactly 1,693 terminal leaves.

For a labeled state, choose a vertex permutation carrying it to its canonical representative, read the stored canonical edge, and query the inverse image of that edge. Repeating this after each answer reconstructs an optimal policy. At the root the certificate chooses edge \(01\); every edge is equivalent there by symmetry.

### Background and intake notes

Current rigorous bounds are 1327 <= L_6 <= 7171. The lower bound counts 1296 labeled spanning trees and 31 maximal disconnected bipartitions.

- Original intake status: Status unknown. Query complexity of graph properties is classical, while the leaf-minimization value may be tabulated.
- Monotonicity certifies a partial assignment as soon as its present edges connect the graph or its absent edges disconnect even the maximal completion.
- Memoize ternary edge states. Isomorphic partial graphs are the main available reduction beyond the 3^15 raw state space.

- Recorded example: On vertices 0 through 5, querying edges in the fixed order 14,01,34,24,03,25,04,35,15,02,45,05,13,23,12 and stopping once connectivity or disconnection is forced gives 7171 leaves.

### Supporting results

- **Computation 2** (reproduced): The 1,296 labeled spanning trees and 31 complete two-part graphs must reach distinct monochromatic leaves.
- **Claim 1** (supported): The edge-query model is classical, while the exact value 1,693 was not located in the published sources searched. [3](#reference-3) [1](#reference-1) [2](#reference-2)

### Runnable artifacts

- **Artifact 1** (reproduced): Standard C++ evaluates the exact recurrence, checks all stored lower bounds, and replays the optimal policy. [3](#reference-3)

### Computational notes

- A direct recursive verifier recomputed 7171 leaves for the displayed fixed order, using present-edge connectivity and possible-edge disconnection as terminal tests. Complete memoized minimization proved L_5=181 after visiting 56023 partial states.

### Working on this

Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `connectivity-decision-tree-six-leaves`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome.

## Lean verification

An informal proof is recorded. A Lean formalization still needs to be attached.

[Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20connectivity-decision-tree-six-leaves%0A%0AExact%20title%3A%20Leaf%20complexity%20of%20six-vertex%20graph%20connectivity%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Fconnectivity-decision-tree-six-leaves%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.).

## References

1. <a id="reference-1"></a>Ronald L. Rivest and Jean Vuillemin, “On recognizing graph properties from adjacency matrices,” Theoretical Computer Science 3(3) (1976), 371-384. DOI 10.1016/0304-3975(76)90053-0. main evasiveness theorem for nontrivial monotone graph properties https://doi.org/10.1016/0304-3975(76)90053-0
   - Also cited at Ronald L. Rivest and Jean Vuillemin, On recognizing graph properties from adjacency matrices, Theoretical Computer Science 3 (1976), 371-384
   - scholarly_publication; reference source; checked 2026-08-01
   - Source use: citation_only
   - For Leaf complexity of six-vertex graph connectivity, this source places connectivity in the graph-property decision-tree framework; it does not give the exact six-vertex leaf count.
2. <a id="reference-2"></a>Jeff Kahn, Michael E. Saks, and Dean Sturtevant, “A topological approach to evasiveness,” 24th Annual Symposium on Foundations of Computer Science (1983), 31-33. DOI 10.1109/SFCS.1983.4. topological evasiveness result for graph properties https://doi.org/10.1109/SFCS.1983.4
   - Also cited at Jeff Kahn, Michael Saks, and Dean Sturtevant, A topological approach to evasiveness, FOCS 1983; expanded in Combinatorica 4 (1984), 297-306
   - scholarly_publication; reference source; checked 2026-08-01
   - Source use: citation_only
   - For Leaf complexity of six-vertex graph connectivity, this source supplies general topological evasiveness context; it does not give the exact six-vertex leaf count.
3. <a id="reference-3"></a>Arkadev Chattopadhyay, Yogesh Dahiya, Nikhil S. Mande, Jaikumar Radhakrishnan, and Swagato Sanyal, “Randomized versus Deterministic Decision Tree Size”. Proceedings of the 55th Annual ACM Symposium on Theory of Computing (2023), 867-880. DOI 10.1145/3564246.3585199. Literature search completed 2026-07-24; Chattopadhyay et al. 2023, Definition 2.6 and Proposition 2.12; Rivest and Vuillemin 1976; Kahn, Saks, and Sturtevant 1984 https://doi.org/10.1145/3564246.3585199
   - Also cited at Arkadev Chattopadhyay, Yogesh Dahiya, Nikhil S. Mande, Jaikumar Radhakrishnan, and Swagato Sanyal, Randomized versus Deterministic Decision Tree Size, STOC 2023, Definition 2.6
   - Also cited at Exact isomorphism-reduced dynamic program and independently replayed certificate in cdt6-artifact-isomorphism-dp-certificate, executed 2026-07-24
   - Also cited at C++17 source below, compiled and executed 2026-07-24
   - scholarly_publication; reference source; version of record; checked 2026-08-01
   - Source use: citation_only
   - For Leaf complexity of six-vertex graph connectivity, the reviewed source scope is Literature search completed 2026-07-24; Chattopadhyay et al. 2023, Definition 2.6 and Proposition 2.12; Rivest and Vuillemin 1976; Kahn, Saks, and Sturtevant 1984. The packet makes no inference beyond that cited scope.
   - Source named by the research packet.