Theorem thm:max_string: the maximal complete non-fringe r-ary height

Source lines 475–521 (statement), 2800–2897 (proof, inventory P20). The target is the reviewed statement PoissonDeclumping.MaxStringStatement of Statements/Main.lean. The final theorem maxString_of takes Theorems thm:PoissonApproximation and thm:PoissonApproximation2 as hypotheses of exactly their reviewed statement types (PoissonApproximationStatement, PoissonApproximation2Statement); everything else is proved from the hypothesis InStableDomain μ (through Stable.stableToolkit).

All marks are G_k = 1{H_{r,k} ≺ ·} (Embeds (completeTree r k)), with π_k = μ_1^k (r = 1) or μ_r^{(r^k-1)/(r-1)} (r ≥ 2), and the cutoff is M_n = max 1 ⌊n^{1-η}⌋₊ with η = (1 - 1/α)/2 (correction F11). All limits run along admissible sizes.

• (i) maxString_unary_of (μ_1 > 0): level k_n = (⌊t_n^* + t⌋ + 1).toNat (the level may be nonpositive for finitely many n; {H_1 ≤ ⌊t_n^* + t⌋} = {N_{k_n} = 0} holds for every n, setOf_natCast_le_eq). Raw (S) by Lemma lem:S_rary(i) (k_n = O(log n)), declumped (C) by Lemma lem:C_rary with B = {d | d ≠ 1}, c_B = 1 - μ_1 (cB_ne_one), propagation (propagatesOutside_completeTree_one), n π_{k_n} bounded; Theorem thm:PoissonApproximation2(i) gives the declumped Poisson approximation, Corollary cor:SM(iii) the vanishing root mark (π_{k_n} = O(1/n)), Lemma lem:declump_to_raw the raw zero event (this is the paper's Corollary cor:declump_zero), and the exact lattice identity n (1 - μ_1) μ_1^{⌊t_n^*+t⌋+1} = μ_1^{t+1-{t_n^*+t}} the limit.
• (ii) maxString_rary_of (r ≥ 2, μ_r > 0): the thresholds eq:threshold_rary. Upper (tendsto_le_maxCompleteHeight_zero): Markov (Lemma lem:ineqs) with E[N_{k_n}(𝒯^n)] ∼ n π_{k_n} (Corollary cor:SM(ii)). Lower (tendsto_le_maxCompleteHeight_one): Theorem thm:PoissonApproximation(ii) with (M) from Corollary cor:SM(i) and (C) from Lemma lem:S_rary(ii) — correction F8: the source cites Corollary cor:Non-fringe Poisson(ii), whose uniform pair hypothesis is not established; the summed pair bound of Lemma lem:S_rary(ii) is exactly Assumption (C) of Theorem thm:PoissonApproximation. The two-point set is handled without the paper's split at θ_n = 1/2: J_n = {a_n, a_n + 1} with a_n = twoPointLow t_n^{**}, n π_{a_n} → ∞, n π_{a_n+2} → 0 (ExtremesAnalysis.rary_twoPoint_thresholds), and P(H_r ∈ J_n) ≥ P(H_r ≥ a_n) - P(H_r ≥ a_n + 2); the interior phase uses the levels m_n, m_n + 1.

theorem PoissonDeclumping.Extremes.cB_ne_one {μ : PMF ℕ} (hc : IsCritical μ) : cB μ {d : ℕ | d ≠ 1} = 1 - μ 1

c_B = 1 - μ_1 for B = {d | d ≠ 1} (criticality: ∑ j μ_j = 1).

theorem PoissonDeclumping.Extremes.pmf_toReal_mem_Ioo {μ : PMF ℕ} {r : ℕ} (h0 : 0 < μ r) (h1 : μ r ≠ 1) : 0 < (μ r).toReal ∧ (μ r).toReal < 1

0 < μ_r < 1 in real form, for μ_r > 0 and μ_r ≠ 1.

theorem PoissonDeclumping.Extremes.propagatesOutside_completeTree_one (k : ℕ) : PlaneTree.PropagatesOutside {d : ℕ | d ≠ 1} (PlaneTree.completeTree 1 k).Embeds

Propagation for the unary marks: if a child of a vertex of outdegree 1 carries a unary chain of height k, so does the vertex.

theorem PoissonDeclumping.Extremes.cutoff_exponent {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) : (0 < (1 - 1 / α) / 2 ∧ (1 - 1 / α) / 2 < 1 - 1 / α) ∧ (1 - 1 / α) / 2 < 1

The cutoff exponent η = (1 - 1/α)/2 ∈ (0, 1 - 1/α).

theorem PoissonDeclumping.Extremes.setOf_natCast_le_eq {r : ℕ} (hr : 1 ≤ r) (m : ℤ) : {T : PlaneTree | ↑(PlaneTree.maxCompleteHeight r T) ≤ m} = {T : PlaneTree | PlaneTree.markCount (PlaneTree.completeTree r (m + 1).toNat).Embeds T = 0}

{H_r(T) ≤ m} = {N_{(m+1).toNat}(T) = 0} for every integer m (r ≥ 1).

theorem PoissonDeclumping.Extremes.maxString_unary_of (h2 : PoissonApproximation2Statement) (μ : PMF ℕ) (hμ : InStableDomain μ) (hμ1 : 0 < μ 1) : LatticeGumbel μ (PlaneTree.maxCompleteHeight 1) (μ 1).toReal (tStar (μ 1).toReal)

Theorem thm:max_string(i) (source lines 477–485, proof 2808–2850), conditional on Theorem thm:PoissonApproximation2 (PoissonApproximation2Statement, its part (i)).

Theorem thm:max_string(ii): thresholds

theorem PoissonDeclumping.Extremes.le_maxCompleteHeight_iff_one_le {r : ℕ} (hr : 1 ≤ r) (T : PlaneTree) (k : ℕ) : ↑k ≤ ↑(PlaneTree.maxCompleteHeight r T) ↔ 1 ≤ ↑(PlaneTree.markCount (PlaneTree.completeTree r k).Embeds T)

{H_r(T) ≥ k} = {N_k(T) ≥ 1} (r ≥ 1), in the real form used by Lemma lem:ineqs.

theorem PoissonDeclumping.Extremes.lintegral_markCount_eq_ofReal {μ : PMF ℕ} {n : ℕ} (hn : PlaneTree.Admissible μ n) (G : PlaneTree → Prop) : ∫⁻ (T : PlaneTree), ENNReal.ofReal ↑(PlaneTree.markCount G T) ∂PlaneTree.conditioned μ n = ENNReal.ofReal (∫ (T : PlaneTree), ↑(PlaneTree.markCount G T) ∂PlaneTree.conditioned μ n)

At an admissible size, ∫⁻ N(𝒯^n) = ENNReal.ofReal (E[N(𝒯^n)]).

theorem PoissonDeclumping.Extremes.tendsto_le_maxCompleteHeight_zero {μ : PMF ℕ} {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {r : ℕ} (hr : 2 ≤ r) {k : ℕ → ℕ} (hk : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑r ^ k n ≤ ↑n ^ δ) (hπ : Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ (fun (j : ℕ) => (PlaneTree.completeTree r j).Embeds) k n) (admissibleSizes μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | k n ≤ PlaneTree.maxCompleteHeight r T}) (admissibleSizes μ) (nhds 0)

Upper threshold (first implication of eq:threshold_rary, source lines 2860–2872): if r^{k_n} = n^{o(1)} and n π_{k_n} → 0 along admissible sizes, then P(H_r(𝒯^n) ≥ k_n) → 0. Lemma lem:ineqs (first half, Markov) with E[N_{k_n}(𝒯^n)] ∼ n π_{k_n} (Lemma lem:S_rary(i) and Corollary cor:SM(ii)).

theorem PoissonDeclumping.Extremes.tendsto_le_maxCompleteHeight_one (h1 : PoissonApproximationStatement) {μ : PMF ℕ} (hμ : InStableDomain μ) {α : ℝ} {a : ℕ → ℝ} (hT : StableToolkit μ α a) {r : ℕ} (hr : 2 ≤ r) (hμr : 0 < μ r) {k : ℕ → ℕ} (hk : ∀ (δ : ℝ), 0 < δ → ∀ᶠ (n : ℕ) in admissibleSizes μ, ↑r ^ k n ≤ ↑n ^ δ) (hπ : Filter.Tendsto (fun (n : ℕ) => ↑n * markProb μ (fun (j : ℕ) => (PlaneTree.completeTree r j).Embeds) k n) (admissibleSizes μ) Filter.atTop) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real {T : PlaneTree | k n ≤ PlaneTree.maxCompleteHeight r T}) (admissibleSizes μ) (nhds 1)

Lower threshold (second implication of eq:threshold_rary, source lines 2860–2872, with correction F8): if μ_r > 0, r^{k_n} = n^{o(1)} and n π_{k_n} → ∞ along admissible sizes, then P(H_r(𝒯^n) ≥ k_n) → 1. Assumption (M) comes from (S) (Lemma lem:S_rary(i) and Corollary cor:SM(i)), Assumption (C) from the summed pair bound (Lemma lem:S_rary(ii)), and N_{k_n}(𝒯^n) → ∞ in probability from Theorem thm:PoissonApproximation(ii).

theorem PoissonDeclumping.Extremes.tendsto_diff_one {μ : PMF ℕ} {E F : ℕ → Set PlaneTree} (hE : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real (E n)) (admissibleSizes μ) (nhds 1)) (hF : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real (F n)) (admissibleSizes μ) (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => (PlaneTree.conditioned μ n).real (E n \ F n)) (admissibleSizes μ) (nhds 1)

Localization from two thresholds: if P(E_n) → 1 and P(F_n) → 0 along admissible sizes, then P(E_n \ F_n) → 1.

theorem PoissonDeclumping.Extremes.maxString_rary_of (h1 : PoissonApproximationStatement) (μ : PMF ℕ) (hμ : InStableDomain μ) (r : ℕ) (hr : 2 ≤ r) (hμr : 0 < μ r) : TwoPointLocalization μ (PlaneTree.maxCompleteHeight r) (tStarStar r (μ r).toReal)

Theorem thm:max_string(ii) (source lines 486–501, proof 2851–2897), conditional on Theorem thm:PoissonApproximation (PoissonApproximationStatement, its part (ii)), which replaces the paper's citation of Corollary cor:Non-fringe Poisson(ii) (correction F8).

theorem PoissonDeclumping.Extremes.maxString_of (h1 : PoissonApproximationStatement) (h2 : PoissonApproximation2Statement) : MaxStringStatement

Theorem thm:max_string (source lines 475–501), conditional on Theorems thm:PoissonApproximation and thm:PoissonApproximation2 (the reviewed statements PoissonApproximationStatement and PoissonApproximation2Statement).