feat(SetTheory/Descriptive/Tree): add infinite branches and bodies

[Hilbert-beinghappy]

Motivation

The existing tree A API models trees as prefix-closed sets of finite
lists, together with some basic node operations (take, subAt,
pullSub). It had no notion of an infinite branch through such a
tree. Infinite branches and their collection, the body of a tree, are
basic vocabulary in descriptive set theory (e.g. to state that a tree
is well-founded iff its body is empty, or to talk about closed subsets
of Baire space as bodies of trees), so this is a natural extension of
the file.

Changes

• initialSegment x n is the list of the first n values of an
  infinite sequence x : ℕ → A, with lemmas relating its length and
  its behaviour when passing from n to n + 1.
• IsBranch T x says that x : ℕ → A is an infinite branch of T:
  every finite initial segment of x lies in T.
• body T is the set of infinite branches of T, defined via
  IsBranch.
• The auxiliary lemmas nil_mem_of_isBranch (a branch forces the root
  [] to lie in T) and body_mono (body is monotone in the tree,
  tagged @[gcongr]) round out the basic API.

Scope

This PR intentionally does not add closedness of body T (which
would require A to carry the discrete topology, so that body T is
closed in the product topology on ℕ → A), well-foundedness of trees
(which needs well-founded relations and descending chains), or rank
(which needs ordinal-valued rank API). These are left for follow-up
PRs, since each pulls in its own dependencies and deserves separate
review.

Verification

• lake build Mathlib.SetTheory.Descriptive.Tree
• lake exe lint-style Mathlib.SetTheory.Descriptive.Tree
• lake build Mathlib

AI use

I used Codex to help select this item from the
backlog, adapt the definitions to the existing tree A API and to the
Descriptive.Tree namespace and current module system (e.g. adding
the public import for Mathlib.Data.List.OfFn), draft the
implementation, and run the three verification commands above. I
checked every definition and lemma statement against its intended
mathematical meaning, and went through each proof term individually,
unfolding initialSegment, IsBranch, and body to confirm the
simp/simpa calls actually close the resulting goals rather than
just trusting that they compiled.

[github-actions]

PR summary 7446aca08f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IsBranch
+ body
+ body_mono
+ initialSegment
+ initialSegment_succ
+ initialSegment_zero
+ length_initialSegment
+ mem_body
+ nil_mem_of_isBranch

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 7446aca).

• +9 new declarations
• −0 removed declarations

+Descriptive.Tree.IsBranch
+Descriptive.Tree.body
+Descriptive.Tree.body_mono
+Descriptive.Tree.initialSegment
+Descriptive.Tree.initialSegment_succ
+Descriptive.Tree.initialSegment_zero
+Descriptive.Tree.length_initialSegment
+Descriptive.Tree.mem_body
+Descriptive.Tree.nil_mem_of_isBranch

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7446aca08f
Reference commit d0060d7bbb

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).