# Agreement subtrees of balanced trees

Partial progress on an open problem. Vamshi Jandhyala.

> Two balanced trees on n leaves always agree on at least n^0.243 leaves, and some on only n^(5/11); Martin and Thatte conjectured n^(1/2).

Canonical: https://vamshij.com/research/balanced-tree-agreement-subtrees
Code and Lean proofs: https://github.com/jvvk/mathematics/tree/main/balanced-tree-agreement-subtrees
Paper (PDF): https://github.com/jvvk/mathematics/blob/main/balanced-tree-agreement-subtrees/paper/fig_grid.pdf

Two rooted binary trees on the same leaf labels agree on a set of labels when the subtrees they induce on
it are the same. Let `M(n)` be the least possible size of the largest such set over all pairs of
*balanced* trees on `n = 2^m` leaves. Martin and Thatte conjectured `M(n) ≥ √n`; Bordewich, Linz, Owen,
St. John, Semple and Wicke (SIAM J. Discrete Math. 2022) disproved it by a slowly vanishing factor and
proved `M(n) ≥ n^0.17`.

The paper proves:

- **The exponent exists.** A substitution lemma makes `M` submultiplicative, so by Fekete's lemma
  `β = lim log₂ M(2^m) / m` exists and equals the infimum. Any single pair of balanced trees therefore gives
  a bound for all `n`.
- **`β ≤ 5/11`.** The `k = 3` example of Bordewich et al. (2048 leaves, agreement 32) gives
  `M(n) ≤ 2^10 n^(5/11)`, polynomially below `√n`.
- **`β ≥ 0.243`.** Their inductive lower bound with optimised constants gives `n^0.235`; an induction
  that looks two levels down one tree and one level down the other gives `n^0.243`.

Preprint v1, 9 October 2026, not peer reviewed.

- **Formally verified in Lean 4** (`lean/`, standard axioms only):
  - the substitution lemma, submultiplicativity and the existence of the exponent;
  - Lemma 4.5 of Bordewich et al. and an explicit 2048-leaf pair with agreement at most 32, hence
    `β ≤ 5/11`;
  - `M(n) ≥ n^0.235`, including its computer-assisted inequality (Lean checks a certificate);
  - the two-level induction, giving `M(n) ≥ n^0.243` from the inequality of Lemma 5.3;
  - that agreement through triples is the usual definition (`S|Y ≅ T|Y`).
- **Not formalised:** the inequality of Lemma 5.3. Its certificate (1,418,968 simplices) is checked in
  exact arithmetic by `verify/certify_simplex_rig.py`. So `n^0.243` rests on that program, while `n^0.235`
  and `5/11` are fully machine-checked.

The author used an AI assistant (Claude, Anthropic) in this work, as described in the paper's
acknowledgement, and is responsible for its content.