feat(IndexedBinaryTree): add Skeleton depth/leafCount and index depth bounds

[BoltonBailey]

This PR adds Skeleton.depth and Skeleton.leafCount to ToMathlib/Data/IndexedBinaryTree/Basic.lean, which are another part of what's needed for the upstreaming of Verified-zkEVM/ArkLib#144.

I have also added a bit of API that seems like it will be useful, using numina-lean-agent tool.

🤖 Generated with Claude Code

[github-actions]

🤖 PR Summary

Mathematical Formalization

• Defines Skeleton.depth and Skeleton.leafCount for measuring binary tree skeletons.
• Establishes a foundational API including simp lemmas and the structural invariant that every skeleton contains at least one leaf.
• Implements bounding theorems relating the depth of leaf and node indices to the overall depth of the tree skeleton.

---

Statistics

Metric	Count
📝 Files Changed	2
✅ Lines Added	69
❌ Lines Removed	0

---

Lean Declarations

✏️ **Added:** 9 declaration(s)

• def Skeleton.leafCount : Skeleton → Nat in ToMathlib/Data/IndexedBinaryTree/Basic.lean
• theorem Skeleton.leafCount_internal (left right : Skeleton) : in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• theorem SkeletonLeafIndex.depth_le_skeleton_depth : in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• theorem Skeleton.leafCount_leaf : Skeleton.leaf.leafCount = 1 in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• def Skeleton.depth : Skeleton → Nat in ToMathlib/Data/IndexedBinaryTree/Basic.lean
• theorem Skeleton.leafCount_pos : ∀ s : Skeleton, 0 < s.leafCount in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• theorem Skeleton.depth_leaf : Skeleton.leaf.depth = 0 in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• theorem SkeletonNodeIndex.depth_le_skeleton_depth : in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean
• theorem Skeleton.depth_internal (left right : Skeleton) : in ToMathlib/Data/IndexedBinaryTree/Lemmas.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

All changes adhere to the style guide.

---

📄 **Per-File Summaries**

• ToMathlib/Data/IndexedBinaryTree/Basic.lean: This change introduces the Skeleton.depth and Skeleton.leafCount definitions to calculate the maximum depth and total number of leaves in a binary tree skeleton. No new theorems or proofs were modified, and the file contains no sorry placeholders.
• ToMathlib/Data/IndexedBinaryTree/Lemmas.lean: This update introduces several new theorems and simp lemmas characterizing the depth and leaf count of Skeleton structures. Key additions include proofs that every skeleton has at least one leaf and that the depth of any leaf or node index is bounded by the tree's overall depth.

---

Last updated: 2026-05-02 15:08 UTC.