`Carleson/Forest.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 981 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned Carleson blueprint

28 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)

Carleson.TileStructure

Imported by 2 files

structure TileStructure.Forest An n-forest line 21 source
Source documentation
An n-forest

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt
11 instances, coercions and auxiliary constants left out.
```
structure Forest (n : ℕ) where
…
```
instance TileStructure.Forest.(instance at line 39) line 39 source
instance TileStructure.Forest.(instance at line 40) line 40 source
instance TileStructure.Forest.(instance at line 41) line 41 source
lemma TileStructure.Forest.mem_mk line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, Membership.mem, Set.Nonempty, Set.OrdConnected, Ne and 25 more
Proof uses: Iff.rfl
108 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.mem_𝔘 line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Iff, Membership.mem, TileStructure.Forest.𝔘
Proof uses: Iff.rfl
27 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.mem_𝔗 line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Iff, Membership.mem, TileStructure.Forest.𝔗
Proof uses: Iff.rfl
26 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.nonempty line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, Set.Nonempty, TileStructure.Forest.𝔗
Proof uses: TileStructure.Forest.nonempty'
26 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.ordConnected line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, Set.OrdConnected, TileStructure.Forest.𝔗
Proof uses: TileStructure.Forest.ordConnected'
28 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.𝓘_ne_𝓘 line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, Ne and 2 more
Proof uses: TileStructure.Forest.𝓘_ne_𝓘'
29 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.smul_four_le line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LE.le and 3 more
Proof uses: TileStructure.Forest.smul_four_le'
38 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.stackSize_le line 53 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Forest, LE.le, stackSize, TileStructure.Forest.𝔘, HPow.hPow and 1 more
Proof uses: TileStructure.Forest.stackSize_le'
28 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.dens₁_𝔗_le line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, LE.le, ENNReal and 7 more
Proof uses: TileStructure.Forest.dens₁_𝔗_le'
43 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.lt_dist line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, Ne, TileStructure.Forest.𝔗 and 15 more
Proof uses: TileStructure.Forest.lt_dist'
57 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.ball_subset line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LE.le and 7 more
Proof uses: TileStructure.Forest.ball_subset'
42 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.ball_subset_of_mem_𝓘 line 62 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, Grid and 7 more
Proof uses: LE.le.trans, 𝔠, Metric.ball_subset_ball', le_of_not_gt, HAdd.hAdd, Dist.dist, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, inferInstance, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr and 45 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma TileStructure.Forest.𝓘_le_𝓘 line 67 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LE.le and 2 more
Proof uses: And.left, Prod.fst, OrderDual, FunctionDistances.Θ, smul, OfNat.ofNat, Prod.snd, TileStructure.Forest.smul_four_le
53 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.cball_subset_cball line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LE.le and 8 more
Proof uses: And.right, Grid, Prod.fst, OrderDual, FunctionDistances.Θ, smul, Prod.snd, TileStructure.Forest.smul_four_le
64 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.𝒬_mem_cball line 73 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, FunctionDistances.Θ and 8 more
Proof uses: TileStructure.Forest.cball_subset_cball, Metric.mem_ball_self, zero_lt_one
70 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.dist_lt_four line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LT.lt and 8 more
Proof uses: Iff.mp, Metric.ball, Metric.mem_ball', TileStructure.Forest.𝒬_mem_cball
56 instances, coercions and auxiliary constants left out.
lemma TileStructure.Forest.dist_lt_four' line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Forest, Membership.mem, TileStructure.Forest.𝔗, LT.lt and 8 more
Proof uses: Iff.mp, Metric.ball, Metric.mem_ball, TileStructure.Forest.𝒬_mem_cball
56 instances, coercions and auxiliary constants left out.
structure TileStructure.Row An n-row line 86 source
Source documentation
An n-row

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt
11 instances, coercions and auxiliary constants left out.
```
structure Row (n : ℕ) extends Forest X n where
…
```
Mentions: TileStructure.Forest
instance TileStructure.Row.(instance at line 93) line 93 source
instance TileStructure.Row.(instance at line 94) line 94 source
instance TileStructure.Row.(instance at line 95) line 95 source
lemma TileStructure.Row.mem_𝔘 line 97 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Row, Iff, Membership.mem, TileStructure.Forest.𝔘 and 1 more
Proof uses: Iff.rfl
27 instances, coercions and auxiliary constants left out.
lemma TileStructure.Row.mem_𝔗 line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, 𝔓, TileStructure.Row, Iff, Membership.mem, TileStructure.Forest.𝔗 and 1 more
Proof uses: Iff.rfl
26 instances, coercions and auxiliary constants left out.
lemma TileStructure.Row.pairwiseDisjoint line 100 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: PseudoMetricSpace, Nat, Real, Complex, Int, Set, ProofData, TileStructure, NNReal, defaultA, ProofData.Q, defaultD, defaultκ, defaultS, cancelPt, TileStructure.Row, Set.PairwiseDisjoint, 𝔓, TileStructure.Forest.𝔘, TileStructure.Row.toForest and 1 more
Proof uses: TileStructure.Row.pairwiseDisjoint'
34 instances, coercions and auxiliary constants left out.