Proof of `Depth and approximation loss of balanced recursion` (2nd statement)
groundedproofs/Lax263307Proofs/RecursionDepth.lean · lax-263307
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Monotonicity of the integer depth function and its defining recurrence give one fewer available level for every balanced child.