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.

For any monotone Boolean function, distinct minimal positive inputs must reach distinct positive leaves. If two reached the same leaf, that leaf's forced-present coordinates would lie in their intersection and would contain a positive input smaller than one of them. The dual statement holds for distinct maximal negative inputs.

The minimal connected graphs on six labeled vertices are the spanning trees. Cayley's formula gives \[ 6^{6-2}=1296. \] The maximal disconnected graphs are obtained by splitting the vertex set into two nonempty parts and including every edge within each part. Complementary parts define the same graph, so their number is \[ \frac{2^6-2}{2}=31. \] Positive and negative leaves are separate. Every correct tree therefore has at least \(1296+31=1327\) leaves. This gives a short independent check below the exact computer-certified value 1,693.

Rivest and Vuillemin study graph properties through adaptive adjacency queries and prove a quadratic worst-case query lower bound for every nontrivial monotone graph property. Kahn, Saks, and Sturtevant develop the topological evasiveness method and prove the prime-power vertex case of the evasiveness conjecture. Those results measure maximum root-to-leaf depth.

Chattopadhyay, Dahiya, Mande, Radhakrishnan, and Sanyal define deterministic decision-tree size as the minimum number of leaves and study it for general Boolean functions. Their subcube viewpoint matches the finite recurrence used here. A search of these sources and related graph-property literature found no tabulation of the six-vertex connectivity leaf minimum. The value 1,693 is therefore supported here by a complete finite certificate.

Edges use the order `01,02,03,04,05,12,13,14,15,23,24,25,34,35,45`. A canonical state key is `present_mask | (absent_mask << 15)`, minimized over all 720 vertex permutations. Each certificate row is ``` canonical_key,value,choice ``` where `choice` is an edge index in the canonical labeling and `-1` marks a terminal state.

The default run solves the recurrence and then verifies the certificate locally. At a nonterminal record, every unknown edge must have a certified child sum at least as large as the record's value. The stored choice must attain equality. A branch-and-bound shortcut may omit a present-edge child only when the already certified absent-edge child reaches the record value by itself, since the omitted child contributes at least one leaf. Terminal records are checked directly by connectivity of the present graph or disconnection of the maximal possible graph.

The program then follows the stored choices to replay an upper-bound policy with 1,693 leaves. Passing `--dump-certificate` emits all 23,352 sorted rows. That stream has SHA-256 digest `1229da5ce8044b6f3a7a1062182b46c433540fc82e452015c25d6bc24b0ffcdf`. This table is a matching lower certificate and a reconstructible optimal policy.