LeanPool.AsymptoticTrianglePacking.Internal — T3 convergence core : geometric decay of the

uncovered set

Standalone, Mathlib-only. The mathematical heart of the iterated nibble (T3): if each round covers a definite fraction of the remaining vertices — so the uncovered count a k shrinks by a factor λ < 1 per round — then after T = O(log 1/β) rounds the uncovered count is ≤ β · a 0 = βq.

• geometric_decay — a (k+1) ≤ λ·a k (with a ≥ 0, λ ≥ 0) ⇒ a k ≤ λ^k · a 0.
• exists_round_count_below — for 0 ≤ λ < 1 and target β > 0, some round count T reaches a T ≤ β · a 0.

This is the deterministic convergence mechanism into which the per-round covering bound (exists_large_round_matching / E[covered] ≥ …) plugs to complete T3.

Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem LeanPool.AsymptoticTrianglePacking.Internal.geometric_decay {a : ℕ → ℝ} {lam : ℝ} (hlam : 0 ≤ lam) (hstep : ∀ (k : ℕ), a (k + 1) ≤ lam * a k) (k : ℕ) : a k ≤ lam ^ k * a 0

T3-conv(1) — geometric decay. If a (k+1) ≤ λ · a k for all k (with a nonnegative and λ ≥ 0), then a k ≤ λ^k · a 0.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_round_count_below {a : ℕ → ℝ} {lam β : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hβ : 0 < β) (ha : ∀ (k : ℕ), 0 ≤ a k) (hstep : ∀ (k : ℕ), a (k + 1) ≤ lam * a k) : ∃ (T : ℕ), a T ≤ β * a 0

T3-conv(2) — the uncovered count reaches β · a 0. For a per-round shrink factor 0 ≤ λ < 1 and any target fraction β > 0, some round count T brings the uncovered count down to a T ≤ β · a 0. (Take T with λ^T < β.)

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncovered_step {a b : ℕ → ℝ} {lam : ℝ} (hstep : ∀ (k : ℕ), a (k + 1) ≤ a k - b k) (hcov : ∀ (k : ℕ), (1 - lam) * a k ≤ b k) (k : ℕ) : a (k + 1) ≤ lam * a k

Per-round decrease bridge. If each round's uncovered count a drops by the covered amount b (a(k+1) ≤ a k - b k) and each round covers at least a (1-λ) fraction ((1-λ)·a k ≤ b k), then the uncovered sequence shrinks by factor λ: a(k+1) ≤ λ·a k.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_uncovered_below {a b : ℕ → ℝ} {lam β : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hβ : 0 < β) (ha : ∀ (k : ℕ), 0 ≤ a k) (hstep : ∀ (k : ℕ), a (k + 1) ≤ a k - b k) (hcov : ∀ (k : ℕ), (1 - lam) * a k ≤ b k) : ∃ (T : ℕ), a T ≤ β * a 0

T3 convergence chain. If each round covers at least a (1-λ) fraction of the remaining uncovered vertices (0 ≤ λ < 1), then for any target β > 0 some round count T brings the uncovered set down to ≤ β · a 0 — the nibble reaches (1-β)-coverage.

Bounded-rounds versions (only require the per-round bound for k < T)

The unbounded hcov : ∀ k, (1-λ)·a k ≤ b k is TOO STRONG for the nibble: the per-round covering fraction degrades (d_k → 0), so (1-λ) ≤ frac_k cannot hold for all k. These bounded variants require the decrease/covering only for k < T, and take T with λ^T ≤ β as data — matching the real nibble, where the covering holds while the residual is still near-regular (k < T).

theorem LeanPool.AsymptoticTrianglePacking.Internal.geometric_decay_lt {a : ℕ → ℝ} {lam : ℝ} (hlam : 0 ≤ lam) (T : ℕ) : (∀ k < T, a (k + 1) ≤ lam * a k) → a T ≤ lam ^ T * a 0

Bounded geometric decay. If a (k+1) ≤ λ·a k for k < T, then a T ≤ λ^T · a 0.

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncovered_step_lt {a b : ℕ → ℝ} {lam : ℝ} (T : ℕ) (hstep : ∀ k < T, a (k + 1) ≤ a k - b k) (hcov : ∀ k < T, (1 - lam) * a k ≤ b k) (k : ℕ) : k < T → a (k + 1) ≤ lam * a k

Bounded per-round decrease bridge. As uncovered_step, but only for k < T.

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncovered_below_lt {a b : ℕ → ℝ} {lam β : ℝ} (hlam0 : 0 ≤ lam) (ha : ∀ (k : ℕ), 0 ≤ a k) (T : ℕ) (hT : lam ^ T ≤ β) (hstep : ∀ k < T, a (k + 1) ≤ a k - b k) (hcov : ∀ k < T, (1 - lam) * a k ≤ b k) : a T ≤ β * a 0

Bounded convergence. For a fixed T with λ^T ≤ β, if each round k < T covers at least a (1-λ) fraction, then a T ≤ β · a 0.

LeanPool.AsymptoticTrianglePacking.Internal — discharge of the round-dependent iteration

Standalone, Mathlib-only. The sequence-indexed counterpart of LeanPool.AsymptoticTrianglePacking.Internal.Discharge: with a sequence of retention strategies (necessary by LeanPool.AsymptoticTrianglePacking.Internal.total_gain_le, which caps the total coverage of any single fixed strategy), each round k may cover a different fraction 1 - lam k of the remaining uncovered vertices, and the uncovered count after T rounds is controlled by the PRODUCT ∏_{k<T} lam k rather than by a power lam ^ T.

• geometric_decay_prod_lt, uncovered_below_prod_lt — convergence with round-dependent factors.
• nibble_matching_card_of_oracle_seq_lt — the covered-count bound from a bounded-rounds oracle.
• exists_matching_of_oracle_seq_lt — the NibbleTheorem per-instance conclusion.

Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem LeanPool.AsymptoticTrianglePacking.Internal.geometric_decay_prod_lt {a lam : ℕ → ℝ} (hlam : ∀ (k : ℕ), 0 ≤ lam k) (T : ℕ) : (∀ k < T, a (k + 1) ≤ lam k * a k) → a T ≤ (∏ k ∈ Finset.range T, lam k) * a 0

Convergence with round-dependent factors. If a (k+1) ≤ lam k · a k for every k < T, then a T ≤ (∏_{k<T} lam k) · a 0.

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncovered_below_prod_lt {a b lam : ℕ → ℝ} {β : ℝ} (hlam0 : ∀ (k : ℕ), 0 ≤ lam k) (ha : ∀ (k : ℕ), 0 ≤ a k) (T : ℕ) (hT : ∏ k ∈ Finset.range T, lam k ≤ β) (hstep : ∀ k < T, a (k + 1) ≤ a k - b k) (hcov : ∀ k < T, (1 - lam k) * a k ≤ b k) : a T ≤ β * a 0

Bounded convergence with round-dependent factors. If round k < T decreases the uncovered count by at least a (1 - lam k)-fraction, then a T ≤ (∏_{k<T} lam k) · a 0 ≤ β · a 0.

theorem Hypergraph.nibble_matching_card_of_oracle_seq_lt {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') {H : Finset (Finset V)} {r : ℕ} (hr : IsUniform H r) (hr1 : 1 ≤ r) {lam : ℕ → ℝ} {β : ℝ} (hlam0 : ∀ (k : ℕ), 0 ≤ lam k) (T : ℕ) (hTβ : ∏ k ∈ Finset.range T, lam k ≤ β) (horacle : ∀ k < T, (1 - lam k) * (↑(Fintype.card V) - ↑(support (nibbleMatchingSeq R H k)).card) ≤ ↑(support (roundMatching (R k (nibbleResidualSeq R H k)))).card) : (1 - β) * (↑(Fintype.card V) / ↑r) ≤ ↑(nibbleMatchingSeq R H T).card

Round-dependent discharge. With a sequence of retention strategies and a bounded-rounds oracle — round k < T covers at least a (1 - lam k)-fraction of the vertices still uncovered — the accumulated matching after T rounds covers at least (1-β)·|V|, hence has size at least (1-β)·(|V|/r), provided ∏_{k<T} lam k ≤ β.

theorem Hypergraph.exists_matching_of_oracle_seq_lt {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') {H : Finset (Finset V)} {r : ℕ} (hr : IsUniform H r) (hr1 : 1 ≤ r) {lam : ℕ → ℝ} {β : ℝ} (hlam0 : ∀ (k : ℕ), 0 ≤ lam k) (T : ℕ) (hTβ : ∏ k ∈ Finset.range T, lam k ≤ β) (horacle : ∀ k < T, (1 - lam k) * (↑(Fintype.card V) - ↑(support (nibbleMatchingSeq R H k)).card) ≤ ↑(support (roundMatching (R k (nibbleResidualSeq R H k)))).card) : ∃ (M : Finset (Finset V)), IsMatching H M ∧ (1 - β) * (↑(Fintype.card V) / ↑r) ≤ ↑M.card

Round-dependent oracle ⇒ the NibbleTheorem per-instance conclusion.

LeanPool.AsymptoticTrianglePacking.Internal — from a per-round covering oracle to the adaptive

strategy sequence

Standalone (imports only LeanPool.AsymptoticTrianglePacking.Internal.IterationSeq / LeanPool.AsymptoticTrianglePacking.Internal.DischargeSeq and Mathlib).

The corrected outer interface of the nibble (LeanPool.AsymptoticTrianglePacking.Internal.AdaptiveOracleExistsCeil) asks for a strategy sequence R : ℕ → Finset (Finset V) → Finset (Finset V), per-round rates lam : ℕ → ℝ with ∏_{k<T} lam k ≤ β, and the per-round covering demand

(1 - lam k) · (#uncovered after k rounds) ≤ #(vertices covered in round k).

This file performs the two architectural reductions of that demand, both placeholder-free:

• exists_adaptive_rates_of_uncovered_le — the rate sequence lam is never an obstruction: for ANY strategy sequence R, the rates lam k := u (k+1) / u k (with u k the uncovered count after k rounds) satisfy the per-round demand with equality, and their product telescopes to u T / u 0. Hence the whole outer demand is EQUIVALENT to the single scalar statement u T ≤ β · |V| — "after T rounds at most a β-fraction of the vertices is still uncovered".

• exists_uncovered_le_of_roundOracle — that scalar statement follows from a purely one-round oracle HasRoundOracle H c β: an invariant Inv on (residual hypergraph, covered set) pairs which holds initially and, as long as more than a β-fraction of the vertices is uncovered, can be advanced by one round that covers at least a c-fraction of the still-uncovered vertices. The strategy sequence is built explicitly (oracleStrategy, oracleStateSeq) so that no well-founded recursion or dependent choice over the history is needed.

Combining the two gives exists_adaptive_strategy_of_roundOracle, which is exactly the per-instance conclusion of AdaptiveOracleExistsCeil. The converse hasRoundOracle_of_matching shows the one-round oracle is not a strengthening: it already follows from the existence of one large matching.

Must be placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem LeanPool.AsymptoticTrianglePacking.Internal.roundMatching_eq_of_isMatching {V : Type u_1} [DecidableEq V] {H M : Finset (Finset V)} (hM : Hypergraph.IsMatching H M) : Hypergraph.roundMatching M = M

A matching is its own round matching: every retained edge is isolated.

The uncovered count

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount {V : Type u_1} [DecidableEq V] [Fintype V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : ℝ

The number of vertices still uncovered after k rounds of the strategy sequence R.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount R H k = ↑(Fintype.card V) - ↑(Hypergraph.support (Hypergraph.nibbleMatchingSeq R H k)).card

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount_nonneg {V : Type u_1} [DecidableEq V] [Fintype V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : 0 ≤ uncoveredCount R H k

@[simp]

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount_zero {V : Type u_1} [DecidableEq V] [Fintype V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) : uncoveredCount R H 0 = ↑(Fintype.card V)

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount_succ {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : uncoveredCount R H (k + 1) = uncoveredCount R H k - ↑(Hypergraph.support (Hypergraph.roundMatching (R k (Hypergraph.nibbleResidualSeq R H k)))).card

One round decreases the uncovered count by exactly the number of vertices it covers.

theorem LeanPool.AsymptoticTrianglePacking.Internal.uncoveredCount_antitone {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : uncoveredCount R H (k + 1) ≤ uncoveredCount R H k

The rate sequence is never an obstruction

For ANY strategy sequence, the canonical rates lam k = u (k+1) / u k meet the per-round covering demand with equality and telescope. So the entire outer-loop demand of AdaptiveOracleExistsCeil reduces to the single scalar statement u T ≤ β · |V|.

noncomputable def LeanPool.AsymptoticTrianglePacking.Internal.canonicalRate {V : Type u_1} [DecidableEq V] [Fintype V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : ℝ

The canonical per-round rate of a strategy sequence: the ratio of consecutive uncovered counts (with the convention 0 once everything is covered).

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.canonicalRate_nonneg {V : Type u_1} [DecidableEq V] [Fintype V] (R : ℕ → Finset (Finset V) → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : 0 ≤ canonicalRate R H k

theorem LeanPool.AsymptoticTrianglePacking.Internal.prod_canonicalRate {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (n : ℕ) : (∏ k ∈ Finset.range n, canonicalRate R H k) * uncoveredCount R H 0 = uncoveredCount R H n

The canonical rates telescope exactly.

theorem LeanPool.AsymptoticTrianglePacking.Internal.canonicalRate_cover {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) (k : ℕ) : (1 - canonicalRate R H k) * uncoveredCount R H k ≤ ↑(Hypergraph.support (Hypergraph.roundMatching (R k (Hypergraph.nibbleResidualSeq R H k)))).card

The canonical rates satisfy the per-round covering demand — with equality when some vertex is still uncovered.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_adaptive_rates_of_uncovered_le {V : Type u_1} [DecidableEq V] [Fintype V] {R : ℕ → Finset (Finset V) → Finset (Finset V)} (hR : ∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') (H : Finset (Finset V)) {β : ℝ} (hβ : 0 ≤ β) (T : ℕ) (hT : uncoveredCount R H T ≤ β * ↑(Fintype.card V)) : ∃ (lam : ℕ → ℝ) (T' : ℕ), (∀ (k : ℕ), 0 ≤ lam k) ∧ ∏ k ∈ Finset.range T', lam k ≤ β ∧ ∀ k < T', (1 - lam k) * (↑(Fintype.card V) - ↑(Hypergraph.support (Hypergraph.nibbleMatchingSeq R H k)).card) ≤ ↑(Hypergraph.support (Hypergraph.roundMatching (R k (Hypergraph.nibbleResidualSeq R H k)))).card

The rate sequence is never an obstruction. If after T rounds at most a β-fraction of the vertices is uncovered, then the canonical rates witness the full per-round demand of AdaptiveOracleExistsCeil.

The explicit strategy sequence built from a one-round oracle

def LeanPool.AsymptoticTrianglePacking.Internal.oracleStateSeq {V : Type u_1} [DecidableEq V] (G : Finset (Finset V) → Finset V → Finset (Finset V)) (H : Finset (Finset V)) : ℕ → Finset (Finset V) × Finset (Finset V)

The state (accumulated matching, current residual) after k rounds of the state-indexed oracle G, which chooses the retained set from the current residual and the current covered set.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.AsymptoticTrianglePacking.Internal.oracleStateSeq G H 0 = (∅, H)

def LeanPool.AsymptoticTrianglePacking.Internal.oracleStrategy {V : Type u_1} [DecidableEq V] (G : Finset (Finset V) → Finset V → Finset (Finset V)) (H : Finset (Finset V)) : ℕ → Finset (Finset V) → Finset (Finset V)

The strategy sequence induced by a state-indexed oracle: in round k it feeds the oracle the covered set reached after k rounds. This is a bona fide ℕ → Finset (Finset V) → Finset (Finset V) — no dependence on the run-time history is needed, because the history is a function of G and H alone.

Equations

• LeanPool.AsymptoticTrianglePacking.Internal.oracleStrategy G H k H' = G H' (Hypergraph.support (LeanPool.AsymptoticTrianglePacking.Internal.oracleStateSeq G H k).1)

theorem LeanPool.AsymptoticTrianglePacking.Internal.oracleStrategy_subset {V : Type u_1} [DecidableEq V] {G : Finset (Finset V) → Finset V → Finset (Finset V)} (hG : ∀ (H' : Finset (Finset V)) (S : Finset V), G H' S ⊆ H') (H : Finset (Finset V)) (k : ℕ) (H' : Finset (Finset V)) : oracleStrategy G H k H' ⊆ H'

theorem LeanPool.AsymptoticTrianglePacking.Internal.nibbleIterSeq_oracleStrategy {V : Type u_1} [DecidableEq V] (G : Finset (Finset V) → Finset V → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : Hypergraph.nibbleIterSeq (oracleStrategy G H) H k = oracleStateSeq G H k

The nibble iteration of oracleStrategy G H is exactly the oracle state sequence.

theorem LeanPool.AsymptoticTrianglePacking.Internal.nibbleMatchingSeq_oracleStrategy {V : Type u_1} [DecidableEq V] (G : Finset (Finset V) → Finset V → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : Hypergraph.nibbleMatchingSeq (oracleStrategy G H) H k = (oracleStateSeq G H k).1

theorem LeanPool.AsymptoticTrianglePacking.Internal.nibbleResidualSeq_oracleStrategy {V : Type u_1} [DecidableEq V] (G : Finset (Finset V) → Finset V → Finset (Finset V)) (H : Finset (Finset V)) (k : ℕ) : Hypergraph.nibbleResidualSeq (oracleStrategy G H) H k = (oracleStateSeq G H k).2

The one-round oracle

def LeanPool.AsymptoticTrianglePacking.Internal.HasRoundOracle {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) (c β : ℝ) : Prop

The one-round covering oracle. An invariant Inv on pairs (current residual hypergraph, currently covered set) which

• holds at the start, and
• as long as more than a β-fraction of the vertices is still uncovered, can be advanced by ONE round: a retained set R' ⊆ H' whose round matching covers at least a c-fraction of the still-uncovered vertices and re-establishes the invariant.

This is the per-round (non-iterated) content of the nibble outer loop.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_uncovered_le_of_roundOracle {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {c β : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hβ0 : 0 < β) (hO : HasRoundOracle H c β) : ∃ (R : ℕ → Finset (Finset V) → Finset (Finset V)) (T : ℕ), (∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') ∧ uncoveredCount R H T ≤ β * ↑(Fintype.card V)

Iterating the one-round oracle. A per-round oracle covering a c-fraction of the uncovered set drives the uncovered count below β·|V| in a bounded number of rounds.

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_adaptive_strategy_of_roundOracle {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {c β : ℝ} (hc0 : 0 < c) (hc1 : c ≤ 1) (hβ0 : 0 < β) (hO : HasRoundOracle H c β) : ∃ (R : ℕ → Finset (Finset V) → Finset (Finset V)) (lam : ℕ → ℝ) (T : ℕ), (∀ (k : ℕ) (H' : Finset (Finset V)), R k H' ⊆ H') ∧ (∀ (k : ℕ), 0 ≤ lam k) ∧ ∏ k ∈ Finset.range T, lam k ≤ β ∧ ∀ k < T, (1 - lam k) * (↑(Fintype.card V) - ↑(Hypergraph.support (Hypergraph.nibbleMatchingSeq R H k)).card) ≤ ↑(Hypergraph.support (Hypergraph.roundMatching (R k (Hypergraph.nibbleResidualSeq R H k)))).card

The per-round oracle produces the full adaptive strategy sequence. This is exactly the per-instance conclusion demanded by LeanPool.AsymptoticTrianglePacking.Internal.AdaptiveOracleExistsCeil.

theorem LeanPool.AsymptoticTrianglePacking.Internal.hasRoundOracle_of_scheduled_invariant {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {c β : ℝ} (hc0 : 0 ≤ c) (hc1 : c ≤ 1) (T : ℕ) (hT : (1 - c) ^ T ≤ β) (P : ℕ → Finset (Finset V) → Finset V → Prop) (hP0 : P 0 H ∅) (hdisj : ∀ (j : ℕ) (H' : Finset (Finset V)) (S : Finset V), P j H' S → ∀ e ∈ H', Disjoint e S) (hstep : ∀ j < T, ∀ (H' : Finset (Finset V)) (S : Finset V), P j H' S → β * ↑(Fintype.card V) < ↑(Fintype.card V) - ↑S.card → ∃ R' ⊆ H', P (j + 1) (Hypergraph.residual H' R') (S ∪ Hypergraph.support (Hypergraph.roundMatching R')) ∧ c * (↑(Fintype.card V) - ↑S.card) ≤ ↑(Hypergraph.support (Hypergraph.roundMatching R')).card) : HasRoundOracle H c β

Round oracle from a scheduled invariant. In practice the nibble invariant is not preserved by an unbounded number of rounds: the degree scale, the regularity slack and the exceptional set all degrade from round to round, and the schedule is only good for T rounds. This lemma performs the bookkeeping: an invariant indexed by the round counter, preserved for T rounds, each round covering a c-fraction of the uncovered set, already yields a HasRoundOracle — because after T rounds fewer than a β-fraction of the vertices is left, so the oracle is never asked to step again. The hypothesis hdisj (edges of the current residual avoid the covered set) is the standing invariant of the nibble iteration (nibbleResidualSeq_disjoint_support).

Bridges to the hypergraph bricks

The two elementary conversions a concrete round oracle has to perform: from a lower bound on the round matching's cardinality to the covering demand (via r-uniformity), and from a set of high-degree vertices to a lower bound on the number of edges (handshake).

theorem LeanPool.AsymptoticTrianglePacking.Internal.round_cover_of_matching_card {V : Type u_1} [DecidableEq V] {H' R' : Finset (Finset V)} {r : ℕ} {c U : ℝ} (huni : Hypergraph.IsUniform H' r) (hR' : R' ⊆ H') (h : c * U ≤ ↑r * ↑(Hypergraph.roundMatching R').card) : c * U ≤ ↑(Hypergraph.support (Hypergraph.roundMatching R')).card

Covering demand from the round matching's cardinality. In an r-uniform hypergraph the round matching covers exactly r times its cardinality, so a cardinality bound is a covering bound.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_mul_le_of_degree_ge {V : Type u_1} [DecidableEq V] [Finite V] {H : Finset (Finset V)} {r : ℕ} (huni : Hypergraph.IsUniform H r) (A : Finset V) {δ : ℝ} (hA : ∀ v ∈ A, δ ≤ ↑(Hypergraph.degree H v)) : δ * ↑A.card ≤ ↑r * ↑H.card

Handshake lower bound on the edge count. Any set A of vertices of degree at least δ forces δ · |A| ≤ r · |H|.

theorem LeanPool.AsymptoticTrianglePacking.Internal.round_cover_demand_of_gain {V : Type u_1} [DecidableEq V] [Finite V] {H' R' : Finset (Finset V)} {r : ℕ} {γ δ U m : ℝ} (huni : Hypergraph.IsUniform H' r) (hR' : R' ⊆ H') (A : Finset V) (hA : ∀ v ∈ A, δ ≤ ↑(Hypergraph.degree H' v)) (hδ : 0 ≤ δ) (hγ : 0 ≤ γ) (hgain : γ * ↑H'.card ≤ ↑(Hypergraph.roundMatching R').card) (hAU : U - m ≤ ↑A.card) : γ * δ * (U - m) ≤ ↑(Hypergraph.support (Hypergraph.roundMatching R')).card

The covering demand of HasRoundOracle, from the standard one-round output. This is the last bridge a concrete round oracle has to cross. The nibble bricks deliver a round matching of cardinality at least γ·|H'| (with γ = p·(1-p)^{rΔ} minus the bad-event penalty); the residual near-regularity delivers a set A of vertices of degree at least δ in H'; and the exceptional (dead) vertices are at most m. Then the round covers at least γ·δ·(U - m) vertices, where U is the number of still-uncovered vertices. Handshake plus r-uniformity, nothing else.

theorem LeanPool.AsymptoticTrianglePacking.Internal.hasRoundOracle_of_matching {V : Type u_1} [DecidableEq V] [Fintype V] (H : Finset (Finset V)) {β : ℝ} {M : Finset (Finset V)} (hM : Hypergraph.IsMatching H M) (hcard : (1 - β) * ↑(Fintype.card V) ≤ ↑(Hypergraph.support M).card) : HasRoundOracle H (1 - β) β

The one-round oracle is not a strengthening. A single matching covering a (1-β)-fraction of the vertices already realises a one-round oracle with c = 1 - β.

Ceiling-carrying oracle interface

This module contains the interface and deterministic assembly shared by the tight-band nibble proof. It deliberately contains no historical majority-only or round-oracle development: the global degree ceiling is part of every input.

def LeanPool.AsymptoticTrianglePacking.Internal.AdaptiveOracleExistsCeil : Prop

The adaptive ceiling oracle obtained by iterating a one-round oracle.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.nibbleTheoremMostCeil_of_adaptiveOracleCeil (h : AdaptiveOracleExistsCeil) : NibbleTheoremMostCeil

The ceiling interface follows from its adaptive oracle.

def LeanPool.AsymptoticTrianglePacking.Internal.RoundOracleExistsCeil : Prop

A one-round ceiling oracle which can be iterated into the adaptive oracle.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.AsymptoticTrianglePacking.Internal.adaptiveOracleExistsCeil_of_roundOracleCeil (h : RoundOracleExistsCeil) : AdaptiveOracleExistsCeil

Iterating the one-round ceiling oracle yields the adaptive ceiling oracle.

theorem LeanPool.AsymptoticTrianglePacking.Internal.NibbleTheoremMostCeil.nibbleTheorem (h : NibbleTheoremMostCeil) : NibbleTheorem

The ceiling-carrying theorem entails the strict near-regular theorem.

LeanPool.AsymptoticTrianglePacking.Internal — the tight-band assembly: from one sharp round to the

LeanPool.AsymptoticTrianglePacking.Internal theorem

This file performs the ASSEMBLY of the LeanPool.AsymptoticTrianglePacking.Internal out of the iterable single round LeanPool.AsymptoticTrianglePacking.Internal.SharpRoundHyp (LeanPool.AsymptoticTrianglePacking.Internal.Tight.SharpRound):

• LeanPool.AsymptoticTrianglePacking.Internal.TightParams — the schedule: the round rate γ, the relative tolerance ε, the per-round exceptional fraction θ, the initial exceptional fraction η, the number of rounds T, the degree band [d·lo k, d·hi k] after k rounds and the exceptional budget sig k, together with every inequality the iteration consumes.
• LeanPool.AsymptoticTrianglePacking.Internal.roundOracle_of_sharpRound_params — one round of the schedule: the tight-band invariant is re-established (band, global ceiling, codegree, exceptional budget) and a γ/(16r) fraction of the uncovered vertices is covered; iterated by LeanPool.AsymptoticTrianglePacking.Internal.hasRoundOracle_of_scheduled_invariant.
• LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams — the schedule exists for every r ≥ 2 and β ∈ (0,1).
• LeanPool.AsymptoticTrianglePacking.Internal.roundOracleExistsCeil_of_sharpRound, LeanPool.AsymptoticTrianglePacking.Internal.nibbleTheoremMostCeil_of_sharpRound, LeanPool.AsymptoticTrianglePacking.Internal.nibbleTheoremMostCeilSized_of_sharpRound, LeanPool.AsymptoticTrianglePacking.Internal.nibbleTheorem_of_sharpRound — the packaged conclusions.

The three mechanisms of the assembly are:

• the band step — the floor falls by at most ((r−1)/r)γΔ + εγΔ and the ceiling by at least ((r−1)/r)γ(δ−lost)δ(1−γ)/Δ − εγΔ, so a band of relative width n widens to n(1 + 8((r−1)/r)γ) while both ends fall by the factor 1 − ((r−1)/r)γ;
• the exceptional bookkeeping — the vertices that leave the band (B), the vertices with too many edges into the exceptional set (heavy), the vertices that break the new ceiling (Hi, contained in E ∪ B ∪ heavy) and the vertices damaged by pruning Hi (Dam) are all counted by the deterministic estimate LeanPool.AsymptoticTrianglePacking.Internal.card_heavyLoss_le; the exceptional set therefore grows by a bounded factor (2 + r/(εγ))² per round, which the choice of θ absorbs;
• the covering count — the round covers a γ/(8r) fraction of the live set, which is at least half of the uncovered set as long as the exceptional set stays below β|V|/2.

Must be sorry-free and axiom-clean [propext, Classical.choice, Quot.sound].

The schedule

structure LeanPool.AsymptoticTrianglePacking.Internal.TightParams (r : ℕ) (β : ℝ) : Type

The tight-band schedule. All parameters of the T-round LeanPool.AsymptoticTrianglePacking.Internal at uniformity r and target β, with the inequalities the iteration consumes. lo k, hi k are the degree band after k rounds RELATIVE to the regular degree d, and sig k is the exceptional budget as a fraction of |V|.

• gam : ℝ

  round rate

• eps : ℝ

  relative band tolerance

• exc : ℝ

  per-round exceptional fraction

• eta : ℝ

  initial exceptional fraction

• wid : ℝ

  initial relative band width

• lomin : ℝ

  a positive lower bound for the relative band floor

• T : ℕ

  the number of rounds

• lo : ℕ → ℝ

  relative degree floor after k rounds

• hi : ℕ → ℝ

  relative degree ceiling after k rounds

• sig : ℕ → ℝ

  exceptional budget after k rounds

• gam_pos : 0 < self.gam
• gam_le : self.gam ≤ 1 / 2
• eps_pos : 0 < self.eps
• eps_le : self.eps ≤ 1
• two_gam_le_eps : 2 * self.gam ≤ self.eps

  the tolerance is at least twice the round rate; this is the regime in which the sharp round LeanPool.AsymptoticTrianglePacking.Internal.sharpRoundFor_of_two_gamma_le_eps is proved

• exc_pos : 0 < self.exc
• exc_le : self.exc ≤ 1
• eta_pos : 0 < self.eta
• wid_pos : 0 < self.wid
• lomin_pos : 0 < self.lomin
• lomin_le (k : ℕ) : k ≤ self.T → self.lomin ≤ self.lo k
• hi_le_two_lo (k : ℕ) : k ≤ self.T → self.hi k ≤ 2 * self.lo k
• lo_le_hi (k : ℕ) : k ≤ self.T → self.lo k ≤ self.hi k
• init_lo : self.lo 0 ≤ 1 - self.wid
• init_hi : 1 + self.wid ≤ self.hi 0
• step_lo (k : ℕ) : k < self.T → self.lo (k + 1) ≤ self.lo k - (↑r - 1) / ↑r * self.gam * self.hi k - 2 * self.eps * self.gam * self.hi k
• step_hi (k : ℕ) : k < self.T → self.hi k - (↑r - 1) / ↑r * self.gam * (self.lo k - self.eps * self.gam * self.hi k) * self.lo k * (1 - self.gam) / self.hi k + self.eps * self.gam * self.hi k ≤ self.hi (k + 1)
• sig_init : self.eta ≤ self.sig 0
• sig_step (k : ℕ) : k < self.T → (2 + ↑r / (self.eps * self.gam)) ^ 2 * (self.sig k + self.exc) ≤ self.sig (k + 1)
• sig_le (k : ℕ) : k ≤ self.T → self.sig k ≤ β / 2
• decay : (1 - self.gam / (16 * ↑r)) ^ self.T ≤ β

Elementary hypergraph bricks used by the step

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_prune_eq_zero {V : Type u_1} [DecidableEq V] {K : Finset (Finset V)} {B : Finset V} {v : V} (hv : v ∈ B) : Hypergraph.degree (prune K B) v = 0

Pruning kills the degree of the pruned vertices.

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_mono {V : Type u_1} [DecidableEq V] {K K' : Finset (Finset V)} (h : K' ⊆ K) (v : V) : Hypergraph.degree K' v ≤ Hypergraph.degree K v

Degrees are monotone in the hypergraph.

theorem LeanPool.AsymptoticTrianglePacking.Internal.codegree_mono {V : Type u_1} [DecidableEq V] {K K' : Finset (Finset V)} (h : K' ⊆ K) (x y : V) : Hypergraph.codegree K' x y ≤ Hypergraph.codegree K x y

Codegrees are monotone in the hypergraph.

theorem LeanPool.AsymptoticTrianglePacking.Internal.lostDegree_union_of_disjoint {V : Type u_1} [DecidableEq V] {K : Finset (Finset V)} {S E : Finset V} (hS : ∀ e ∈ K, Disjoint e S) (v : V) : lostDegree K (S ∪ E) v = lostDegree K E v

Only the part of the deleted set that the edges actually meet matters.

theorem LeanPool.AsymptoticTrianglePacking.Internal.degree_eq_zero_of_disjoint {V : Type u_1} [DecidableEq V] {K : Finset (Finset V)} {S : Finset V} (hS : ∀ e ∈ K, Disjoint e S) {v : V} (hv : v ∈ S) : Hypergraph.degree K v = 0

A vertex in an edge-avoided set has degree zero.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_edges_meeting_le_sum {V : Type u_1} [DecidableEq V] {K : Finset (Finset V)} (B : Finset V) : {e ∈ K | ¬Disjoint e B}.card ≤ ∑ x ∈ B, Hypergraph.degree K x

The number of edges meeting B, bounded by the degree sum over B.

theorem LeanPool.AsymptoticTrianglePacking.Internal.sum_lostDegree_eq {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} (B : Finset V) : ∑ v : V, lostDegree K B v = ∑ e ∈ K with ¬Disjoint e B, e.card

The total loss equals the size of the edges meeting B.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_heavyLoss_le_real {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform K r) {Δ : ℝ} (hΔ : ∀ (x : V), ↑(Hypergraph.degree K x) ≤ Δ) (B : Finset V) (ζ : ℝ) : ↑{v : V | ζ < ↑(lostDegree K B v)}.card * ζ ≤ ↑r * (↑B.card * Δ)

Few vertices lose many edges (real form). At most r·|B|·Δ/ζ vertices lose more than ζ edges when the edges meeting B are deleted.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_heavyLoss_le_ratio {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform K r) {Δ ζ psi : ℝ} (hΔ : ∀ (x : V), ↑(Hypergraph.degree K x) ≤ Δ) (hζ : 0 < ζ) (hratio : ↑r * Δ = psi * ζ) (B : Finset V) : ↑{v : V | ζ < ↑(lostDegree K B v)}.card ≤ psi * ↑B.card

Few vertices lose many edges (ratio form). If r·Δ = psi·ζ then at most psi·|B| vertices lose more than ζ edges when the edges meeting B are deleted.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_union_five_le {V : Type u_1} [DecidableEq V] (A B C D E : Finset V) : ↑(A ∪ B ∪ C ∪ D ∪ E).card ≤ ↑A.card + ↑B.card + ↑C.card + ↑D.card + ↑E.card

The cardinality of a five-fold union, in real form.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_compl_union_ge {V : Type u_1} [Fintype V] [DecidableEq V] (S E : Finset V) : ↑(Fintype.card V) - ↑S.card - ↑E.card ≤ ↑(S ∪ E)ᶜ.card

The complement of S ∪ E is at least as large as |V| − |S| − |E|.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_ceiling_step_bound {a gam eps lo hi hi1 d l : ℝ} (hd : 0 < d) (hhi0 : 0 < hi) (ha0 : 0 ≤ a) (hgam0 : 0 ≤ gam) (hg1 : 0 ≤ 1 - gam) (hlo0 : 0 ≤ lo) (hl : l ≤ eps * gam * (d * hi)) (hstep : hi - a * gam * (lo - eps * gam * hi) * lo * (1 - gam) / hi + eps * gam * hi ≤ hi1) : d * hi - a * gam * (d * lo - l) * (d * lo) * (1 - gam) / (d * hi) + eps * gam * (d * hi) ≤ d * hi1

The ceiling of the next round. The drop requested by LeanPool.AsymptoticTrianglePacking.Internal.TightParams.step_hi, at the absolute scale d and with an actual loss l below the tolerance εγ·d·hi, still lands below d·hi₁.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_ge_of_codegree {V : Type u_1} [Fintype V] [DecidableEq V] {K : Finset (Finset V)} {r : ℕ} (hr : Hypergraph.IsUniform K r) (hr1 : 1 ≤ r) {κ : ℝ} (hκ : ∀ (x y : V), x ≠ y → ↑(Hypergraph.codegree K x y) ≤ κ) (v : V) : (↑r - 1) * ↑(Hypergraph.degree K v) ≤ (↑(Fintype.card V) - 1) * κ

Vertex count from the codegree bound. A vertex of degree D forces (r−1)·D ≤ (|V| − 1)·κ.

theorem LeanPool.AsymptoticTrianglePacking.Internal.budget_arith {e b h hh dm tot psi sigj exc sig1 N : ℝ} (hpsi0 : 0 ≤ psi) (he : 0 ≤ e) (hb : 0 ≤ b) (htot : tot ≤ e + b + h + hh + dm) (h1 : h ≤ psi * e) (h2 : hh ≤ e + b + h) (h3 : dm ≤ psi * hh) (hEB : e + b ≤ (sigj + exc) * N) (hN : 0 ≤ N) (hstep : (2 + psi) ^ 2 * (sigj + exc) ≤ sig1) : tot ≤ sig1 * N

The arithmetic of the exceptional budget: the new exceptional set is the old one (e) plus the vertices that left the band (b), plus those heavily damaged by the old exceptional set (h), plus those breaking the new ceiling (hh ≤ e + b + h), plus those damaged by pruning the latter (dm ≤ psi·hh); the total is at most (2 + psi)²(e + b).

One round of the schedule

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_round_step {r : ℕ} (hr : 2 ≤ r) {β : ℝ} (Pm : TightParams r β) {D₀ c₀ : ℝ} (hc₀ : 0 ≤ c₀) (hround : SharpRoundFor r Pm.gam Pm.eps Pm.exc (β / 2) D₀ c₀) {W : Type} [Fintype W] [DecidableEq W] {d κ : ℝ} (hd : 0 < d) (hκ0 : 0 ≤ κ) (hDlo : D₀ ≤ d * Pm.lomin) (hcodsmall : κ ≤ c₀ * (d * Pm.lomin)) (hNbig : D₀ ≤ ↑(Fintype.card W)) {j : ℕ} (hj : j < Pm.T) {K : Finset (Finset W)} {S E : Finset W} (huni : Hypergraph.IsUniform K r) (hSdisj : ∀ e ∈ K, Disjoint e S) (hhi : ∀ (v : W), ↑(Hypergraph.degree K v) ≤ d * Pm.hi j) (hlo : ∀ v ∉ S, v ∉ E → d * Pm.lo j ≤ ↑(Hypergraph.degree K v)) (hcodeg : ∀ (x y : W), x ≠ y → ↑(Hypergraph.codegree K x y) ≤ κ) (hE : ↑E.card ≤ Pm.sig j * ↑(Fintype.card W)) (huncov : β * ↑(Fintype.card W) < ↑(Fintype.card W) - ↑S.card) : ∃ R' ⊆ K, Pm.gam / (16 * ↑r) * (↑(Fintype.card W) - ↑S.card) ≤ ↑(Hypergraph.covered R').card ∧ ∃ (K' : Finset (Finset W)) (E' : Finset W), K' ⊆ Hypergraph.residual K R' ∧ Hypergraph.IsUniform K' r ∧ (∀ e ∈ K', Disjoint e (S ∪ Hypergraph.covered R')) ∧ (∀ (v : W), ↑(Hypergraph.degree K' v) ≤ d * Pm.hi (j + 1)) ∧ (∀ v ∉ S ∪ Hypergraph.covered R', v ∉ E' → d * Pm.lo (j + 1) ≤ ↑(Hypergraph.degree K' v)) ∧ (∀ (x y : W), x ≠ y → ↑(Hypergraph.codegree K' x y) ≤ κ) ∧ ↑E'.card ≤ Pm.sig (j + 1) * ↑(Fintype.card W)

One round of the tight-band schedule. From the invariant at stage j — an r-uniform sub-hypergraph K avoiding the covered set S, with global degree ceiling d·hi j, degree floor d·lo j off the exceptional set E, codegrees ≤ κ and |E| ≤ sig j·|V| — one sharp round produces a retained set covering a γ/(16r) fraction of the uncovered vertices and re-establishes the invariant at stage j+1.

LeanPool.AsymptoticTrianglePacking.Internal — existence of the tight-band schedule

LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams: for every uniformity r ≥ 2 and every target β ∈ (0,1) there is a LeanPool.AsymptoticTrianglePacking.Internal.TightParams r β, i.e. a complete choice of

• the round rate γ, the relative tolerance ε, the exceptional fractions θ (per round) and η (initial), the number of rounds T,
• the relative degree band [lo k, hi k] after k rounds and the exceptional budget sig k,

satisfying every inequality that LeanPool.AsymptoticTrianglePacking.Internal.tight_round_step and LeanPool.AsymptoticTrianglePacking.Internal.hasRoundOracle_of_scheduled_invariant consume.

The schedule is the classical one. With a = (r−1)/r ∈ [1/2, 1):

• γ = min (1/8) (exp(−8M−1)/32) where M = 16rL + 1 and L = log(1/β), n₀ = 8γ, ε = 4aγ;
• q = 1 − aγ, n k = n₀(1 + 8aγ)^k, lo k = q^k(1 − n k), hi k = q^k(1 + n k);
• T = ⌈M/γ⌉, so γT ∈ [M, M + γ]. Then (1 − γ/(16r))^T ≤ exp(−M/(16r)) ≤ exp(−L) = β, while n T ≤ n₀ exp(8γT) ≤ 8γ·exp(8M+1) ≤ 1/4 — the point being that γT ≈ M is INDEPENDENT of γ, so making γ small really does shrink the total band widening.
• sig k = 2θ(2G)^k with G = (2 + r/(εγ))² the per-round exceptional growth factor and η = θ = β/(8(2G)^T), so sig k ≤ β/4.

The two per-round band inequalities reduce to the polynomial cores LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_lo_core and LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_hi_core.

Must be sorry-free and axiom-clean [propext, Classical.choice, Quot.sound].

The two polynomial cores of the band step

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_lo_core {a gam n : ℝ} (ha2 : a ≤ 1) (hgam : 0 < gam) (_hgam8 : gam ≤ 1 / 8) (hn : 8 * gam ≤ n) (hn4 : n ≤ 1 / 4) : 0 ≤ 6 * n - 8 * gam - 8 * gam * n - 8 * a * gam * n

Floor step (polynomial core). With ε = 4aγ and 8γ ≤ n ≤ 1/4, the quantity by which the new floor q(1 − n(1+8aγ)) falls short of the guaranteed drop is aγ(6n − 8γ − 8γn − 8aγn) ≥ 0.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_hi_core {a gam n : ℝ} (ha1 : 1 / 2 ≤ a) (ha2 : a ≤ 1) (hgam : 0 < gam) (_hgam8 : gam ≤ 1 / 8) (hn : 8 * gam ≤ n) (hn4 : n ≤ 1 / 4) : 0 ≤ 4 * a * n + 8 * a * n ^ 2 - a * gam * (1 - n) ^ 2 - 8 * a ^ 2 * gam * n * (1 + n) - 4 * a * gam * (1 + n) ^ 2 - a * (4 * a * gam) * gam * (1 + n) * (1 - n) * (1 - gam)

Ceiling step (polynomial core). With ε = 4aγ and 8γ ≤ n ≤ 1/4, the first-order gain 4an + 8an² of the ceiling dominates all the correction terms.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_lo_scaled {a gam eps q qk n : ℝ} (ha0 : 0 ≤ a) (ha2 : a ≤ 1) (hgam : 0 < gam) (hgam8 : gam ≤ 1 / 8) (hn : 8 * gam ≤ n) (hn4 : n ≤ 1 / 4) (hqk : 0 < qk) (heps : eps = 4 * a * gam) (hq : q = 1 - a * gam) : qk * q * (1 - n * (1 + 8 * a * gam)) ≤ qk * (1 - n) - a * gam * (qk * (1 + n)) - 2 * eps * gam * (qk * (1 + n))

Floor step (scaled). The polynomial core LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_lo_core, multiplied by the common factor q^k carried by both ends of the band.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_hi_scaled {a gam eps q qk n : ℝ} (ha1 : 1 / 2 ≤ a) (ha2 : a ≤ 1) (hgam : 0 < gam) (hgam8 : gam ≤ 1 / 8) (hn : 8 * gam ≤ n) (hn4 : n ≤ 1 / 4) (hqk : 0 < qk) (heps : eps = 4 * a * gam) (hq : q = 1 - a * gam) : qk * (1 + n) - a * gam * (qk * (1 - n) - eps * gam * (qk * (1 + n))) * (qk * (1 - n)) * (1 - gam) / (qk * (1 + n)) + eps * gam * (qk * (1 + n)) ≤ qk * q * (1 + n * (1 + 8 * a * gam))

Ceiling step (scaled). The polynomial core LeanPool.AsymptoticTrianglePacking.Internal.tight_band_step_hi_core, after clearing the denominator 1 + n and multiplying by the common factor q^k carried by both ends of the band.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_band_width_le_quarter {a gam M : ℝ} {T k : ℕ} (ha0 : 0 ≤ a) (ha2 : a ≤ 1) (hgam : 0 < gam) (hgam8 : gam ≤ 1 / 8) (hgamE : gam ≤ Real.exp (-(8 * M) - 1) / 32) (hM0 : 0 < M) (hgamT_ub : gam * ↑T ≤ M + gam) (hk : k ≤ T) : 8 * gam * (1 + 8 * a * gam) ^ k ≤ 1 / 4

The band width stays below 1/4. With γ ≤ exp(−8M−1)/32 and γT ≤ M + γ, the relative width n k = 8γ(1 + 8aγ)^k never exceeds 1/4 before the last round.

theorem LeanPool.AsymptoticTrianglePacking.Internal.tight_schedule_decay_le {gam L M β : ℝ} {r T : ℕ} (hrR : 2 ≤ ↑r) (hgam : 0 < gam) (hgam8 : gam ≤ 1 / 8) (hβ0 : 0 < β) (hLdef : L = -Real.log β) (hMdef : M = 16 * ↑r * L + 1) (hgamT_lb : M ≤ gam * ↑T) : (1 - gam / (16 * ↑r)) ^ T ≤ β

The total decay of the schedule. γT ≥ M = 16rL + 1 with L = log(1/β) gives (1 − γ/(16r))^T ≤ exp(−L) = β.

The schedule

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_tightParams (r : ℕ) (hr : 2 ≤ r) {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1) : Nonempty (TightParams r β)

The tight-band schedule exists.