[RemyDegenne]

This PR adds LMLExplore/ReinforcementLearning/HardTree.lean, the combinatorics of the breadth-first A-ary tree on which the hard instances of the minimax lower bounds for episodic MDPs [DMKV21, Theorems 7 and 9] place all their states except three. The nodes are 0, …, n - 1, and the parent of j + 1 is j / A. The file adds depth A j, with the Galois connection ∑_{i<D} A^i ≤ j ↔ D ≤ depth A j (sum_pow_le_iff_le_depth). It adds height A n = ⌈log_A((A-1)n+1)⌉, with height A n ≤ D ↔ n ≤ ∑_{i<D} A^i (height_le_iff), depth_lt_height, and height_sum_pow: a full tree with (A^d - 1)/(A - 1) nodes has height d. It adds the transition child A n j k, which falls back to the first child when a child is missing, with child_lt and depth_child; the leaves, which make up at least half of the tree (le_two_mul_card_leaves); and walks from the root, with depth_walk and exists_walk: every node is reached in depth A j steps through internal nodes.

The targets are ReinforcementLearning Layer 19.3 (best policy identification lower bound [DMKV21, Theorem 7]) and Layer 18.4 (minimax regret lower bound [DMKV21, Theorem 9]). Both assume S = 3 + (A^d - 1)/(A - 1) and H ≥ 3d, and their hard MDPs are built on this tree. With n = S - 3 nodes, height_sum_pow turns the roadmap's d into height A (S - 3). exists_walk, depth_child and depth_lt_height give the paths of the hard MDP from the root to each leaf within d steps, and le_two_mul_card_leaves gives the count of the leaves that the change-of-measure argument sums over. After this PR, the hard MDPs and their lower bound statements remain.

The material is adapted from Essakine2026Tight/EV2026/HardTree.lean (treeDepth from EV2026/Constants.lean) of github.com/RemyDegenne/Essakine2026Tight, commit 9c77165d56f81c1db7a9835068356bb14886a3be, by Rémy Degenne, Apache-2.0, as the file states. The port makes these changes: the source's geomCount is replaced by Mathlib's partial geometric sums (geom_sum_succ, geom_sum_mul_add). treeDepth S A becomes height A n for the number n = S - 3 of tree nodes, characterized through Nat.clog_le_iff_le_pow. depth gets its converse bound and the characterization sum_pow_le_iff_le_depth. card_leafFinset (n + 3 ≤ 4 #L for n ≥ 3) becomes the sharper n ≤ 2 #L with no assumption on n. two_le_height needs n ≥ 2 instead of S ≥ 6, and exists_walk needs 0 < A instead of 2 ≤ A. The duplicated agreement argument in exists_walk is factored out as walk_update_of_le. The bodies are unexposed, with characteristic lemmas (depth_add_one, height_def, child_of_lt, child_of_not_lt, mem_leaves, walk_zero, walk_add_one). No public declaration is removed or renamed.

Roadmap: ReinforcementLearning

Paper: RemyDegenne/Essakine2026Tight
Item: R28

🤖 Prepared with Claude Code