The exact height at which a tree forces a ladder: T(2)=2 and T(3)=3 for non-uniform (k,δ)-ladders
Abstract
In arXiv:2607.21761v1, Conant and Terry introduced a notion of non-uniform ladder for a function f: X × Y → [0,1] and proved a real-valued analogue of the Shelah–Hodges tree/ladder correspondence: if f admits a (C(2k, k)-1, 2δ)-tree, then f admits a (k,δ)-ladder. They ask whether the height, which grows like 4ᵏ/√(π k), can be brought down to the order of 2ᵏ. Write T(k) for the least height that suffices. We determine it exactly for k ≤ 3: T(2)=2 and T(3)=3, against the values 5 and 19 supplied by their theorem, and we show T(k) ≥ k for every k. The upper bound at k=3 is a four-case analysis on the entries that the tree leaves unconstrained; the lower bounds come from the class of all Boolean concepts on d points. Separately, and as computations rather than as theorems, we record that the two-parameter induction used in the source cannot reach T(3)=3, and that eleven computed values of the auxiliary threshold of that induction all equal 2^(min(k,ℓ)-1); if that pattern persists it answers the question affirmatively, with t=2ᵏ⁻¹. Every theorem below is formalised in Lean 4 and checked by its kernel; the conjecture, and the measurements behind it, are not.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
d5f6fff06a94f1e1449388b5f746b93bad055c91d3f622b2b251cf5d054febbf
Claim ledger
Stated results
TL1candidate2026-09-02
Every f: X x Y -> [0,1] admitting a (2, 2 delta)-tree admits a (2, delta)-ladder, for every X, Y and every delta > 0: the least admissible height at k = 2 is at most 2, against Conant-Terry Theorem 1.11's binom(4,2) - 1 = 5
TL2routine2026-09-02
A (1, 2 delta)-tree need not force a (2, delta)-ladder: the full concept class on one point admits a (1, 1)-tree and omits (2, 1/2)-ladders, so the least admissible height at k = 2 is exactly 2
TL3candidate2026-09-02
Every f: X x Y -> [0,1] admitting a (3, 2 delta)-tree admits a (3, delta)-ladder, for every X, Y and every delta > 0: the least admissible height at k = 3 is at most 3, against Conant-Terry Theorem 1.11's binom(6,3) - 1 = 19
TL4routine2026-09-02
A (2, 2 delta)-tree need not force a (3, delta)-ladder: the full concept class on two points admits a (2, 1)-tree and omits (3, 1/2)-ladders, so the least admissible height at k = 3 is exactly 3
TL5routine2026-09-02
The row-count obstruction: if no row of f is >= delta at k pairwise distinct points then f admits no (k, delta)-ladder – the leaves of a ladder are pairwise distinct (delta > 0) and the first row is uniformly >= delta (r₁ >= 0, the lower half of the source's r in [0,1])
TL6routine2026-09-02
The least admissible height is at least k, for every k: for 0,1-valued f the rows of a (k, delta)-ladder are pairwise distinct, so the full concept class on d points – which admits a (d, 1)-tree – omits (d+1, delta)-ladders for every delta > 0
TL7known2026-09-02
Conant-Terry Proposition 3.4 at height 2, for all admissible parameters at once: for 0 < alpha <= 1, delta > 0 and alpha < 2 delta, the three-valued function that is alpha on sigma¹ <= eta, 0 on sigma⁰ <= eta and alpha/2 elsewhere admits a (2, alpha)-tree with uniform value 0 and omits (3, delta)-ladders – so the change of scale from delta to 2 delta in Theorem 1.11 cannot be dropped
TL8routine2026-09-02
Monotonicity in both parameters: a (t, s)-tree contains a (t', s)-tree for t' <= t (truncate the nodes, pad the leaves) and a (k, delta)-ladder contains a (k', delta)-ladder for k' <= k, so 'the least admissible height' is a genuine threshold
TL9measurement2026-09-02
The search route and its measured cost: the ladder-existence condition separates over rows (f admits a (k,delta)-ladder iff there are leaves y₁..yₖ such that for each i some x satisfies max(0, max_(j<i) f(x,yⱼ)) + delta <= min_(j>=i) f(x,yⱼ)), only pairwise-distinct leaf tuples matter, and after normalising delta = 1 and replacing [0,1] by [0,infinity) the whole question is quantifier-free difference logic – z3 decides height 3 in 2.4 s. Measured: T(2)=2, T(3)=3, T(4)>=4; free-ladder auxiliary T_f(2)=1, T_f(3)=2, T_f(4)>=4; the source's own auxiliary T(k,1)=T(1,l)=1 (its Claim 1(a), reproduced), T(2,2)=T(2,3)=T(2,4)=T(3,2)=2, T(3,3)=4, T(3,4)>=4, against its bound B(k,l)=2C(k+l-2,k-1)-1; discrete D(2)=2, D(3)=3, D(4)>=4
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- From Conant–Terry, *Encoding orders and trees in real-valued functions*, arXiv:2607.21761v1 (math.CO; cs.LG, math.LO), transcribed verbatim. Binary strings: 2ᵗ is the set of strings of length t ("leaves"), 2^(<t) the set of strings of length < t ("nodes"), ⊑ is "is an initial segment of". Fix f: X × Y → [0,1] and δ > 0.
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7