Five orientations of a 32-leaf tree miss exactly one leaf pair

The Lean tree term is the tree of the source's Table 1: reading the vertex labels and edge indices off the rooted term and sorting by edge index reproduces, for each of the 61 lexicographic edges eᵢ = (u,v) with u < v, the child/parent pair the printed parent map assigns to it; 32 distinct leaves, 61 edges, root branches of 4, 13 and 15 leaves

oc(T) <= 6: the six hexadecimal masks of the source's Table 2, decoded under its stated bit convention, join all 496 leaf pairs of T by directed paths; and none of the six is redundant – for each of them there is a leaf pair the other five miss

oc(T) >= 6: no five orientations of the 61 edges of T join every pair of its 32 leaves by a directed path – a kernel-bound proof of the source's refutation, by structural induction over the rooted tree against a validated branch-state certificate, with the reasoning layer (branchₛound) free of native_decide

oc(T) = 6 exactly: 6 is the least m for which T has an orientation cover of size m, so D(32) >= 6 > 5 = ceil(log2 32) and the Brigham-Chartrand-Dutton-Zhang and Aksoy-Kilic-Kocak conjectures fail

The exact five-orientation coverage maximum of T is 495: five orientations join at most 495 of the 496 leaf pairs, and an explicit family attains 495, missing only the pair 3,4

Control: the balanced 32-leaf cubic tree (root branches of 10, 11 and 11 leaves) DOES have an orientation cover of size five, under exactly the definitions that make OC3 a statement about T

The leaf-record bound for every tree of the model at once: if m orientations join every pair of leaves of a rooted tree whose non-leaf vertices all have degree three, then it has at most 2 ^ m leaves; hence oc T > 4 for the source's tree with no branch-state certificate and no native_decide in the proof layer

A tree with t leaves admitting a K-robust m-cover – m orientations plus a set F x of at least K forbidden coordinates at each leaf, every pair still joined outside F x u F y – satisfies t * (K + m) <= m * 2 ^ m; and oc <= rc_K <= oc + K

No tree with exactly 2 ^ m leaves has a robust m-cover; in particular the balanced 32-leaf tree TB, which does have a five-orientation cover, has no robust one, while it does have a robust 6-cover

The common-alive bound: the coordinates in which every leaf of a branch reaches its attachment edge join no pair inside that branch, so the remaining coordinates already cover the branch internally, and |C| + ocᵢ(branch) <= m

6 <= rc T <= 7 and 6 <= rc₆ T <= 12 for the source's tree, where rc_K is the least m admitting a K-robust m-cover

At the smallest tree where the notions separate – two cherries on an edge, four leaves – oc = 2, rc = 3, and oc of the cherry-substituted 8-leaf tree is 3, all three exactly

6 <= oc (T[cherry]) <= 7 for the 64-leaf tree obtained by hanging a cherry at each of the 32 leaves of the source's tree – the cell whose value decides whether the substitution route can produce a second tree with oc > ceil(log2 t)

The converse transport: an m-cover of the cherry-substituted tree reads back down to a robust m-cover, so rc R = oc (R[cherry]) exactly for every tree of the model and every m; at the source's tree, oc (T[cherry]) = 6 iff T has a robust 6-cover, and = 7 iff it does not

A robust m-cover of any tree covers the cherry-substituted tree in the same m coordinates – no extra coordinate – and hence a tree with t leaves and a robust m-cover satisfies 2 t <= 2 ^ m

MEASUREMENT: the K-robust m-cover question for the source's tree as a SAT instance in the family's pivot model, with its positive control

MEASUREMENT: what the general layer cost to formalize

For every k: the k-fold cherry iterate of a tree with exactly 2 ^ m leaves and an m-cover has cover number exactly m + k; instantiated to two infinite families – oc (TB[cherryᵏ]) = 5 + k at 32 * 2ᵏ leaves, and oc (R4[cherryᵏ]) = 2 + k with no native_decide anywhere in its proof

The ladder cap for the source's tree: for every k, the k-fold cherry iterate of T has 32 * 2ᵏ leaves and 5 + k <= oc <= 6 + k = ceil(log2 (32 * 2ᵏ)) + 1, so the doubling ladder's defect stays at most one forever and provably cannot refute the source's Problem 5.1

The K-robust cover number is the orientation-cover number of the K-fold cherry tower: for every tree of the model, every m and every K, m orientations together with a set of at least K forbidden coordinates at each leaf (every pair still joined outside both sets) exist exactly when the tree obtained by grafting the perfect binary branch on 2 ^ K leaves at every leaf has an m-cover. Hence the sharp count 2 ^ K * t <= 2 ^ m, and rc_K R = oc R + K exactly for every tree whose cover number meets the leaf bound (2 ^ a < 2 t, the leaf count not necessarily a power of two)

At the source's tree: 5 + K <= rc_K T <= 6 + K for every K, so 11 <= rc₆ T <= 12 where the family's record was 6 <= rc₆ T <= 12; the (m, K) = (11, 6) design question this family ran as a SAT experiment is rung 6 of the doubling ladder, oc (T[cherry⁶]) = 11 at 2048 leaves; and the family's two open searches are ordered – a robust 6-cover of T implies a 6-robust 11-cover – so a refutation at (11, 6) settles the 64-leaf cell at oc (T[cherry]) = 7

Once a rung of the cherry tower meets the leaf-record bound, every later rung does; so every rung of the doubling ladder over the source's tree has cover number 5 + k or 6 + k, the value 5 + k propagates upwards, and the whole ladder is described by a single threshold

The ladder's infinitely many open cells collapse to one. In a K-robust m-cover each leaf has only m - K free coordinates and a pair can only be joined in a coordinate free at both ends, so if t (m - K) < m some coordinate is forbidden at every leaf and can be deleted at the cost of one coordinate and one unit of robustness; hence some rung of the doubling ladder over the source's tree meets the leaf-record bound if and only if rung 155 does

MEASUREMENT: the price of the m = 6 branch-state recurrence, run in its cheapest form (the ROBUST recurrence on the 32-leaf tree T itself rather than the plain one on the 64-leaf T[cherry]), with its positive control – and the answer is that it is not affordable in Python