Section 5 — Combinatorial core of the r > d truncation branch

Helper lemmas for the r > d branch of lem:projective-low-rank-sum (references/ldt-paper/orthonormalization.tex:559-658).

Given a finite family of overlap values f : α → ℝ (with α the pair index set {(a, i)} carrying r = |α| entries) and a chosen Large ⊂ α of size d < r such that every Small = Lᶜ entry has overlap ≤ every Large entry, the paper derives

• |Large| * ∑_{Small} f ≤ |Small| * ∑_{Large} f (pairwise double-counting),
• r * ∑_{Small} f ≤ |Small| * ∑_{α} f (partition bound).

We then combine this with the global R ≤ (1 + 2√ζ) I estimate to obtain ∑_{Small} f ≤ 4√ζ when ζ ≤ 1/4, which is the combinatorial heart of the paper's 4√ζ truncation error.

These lemmas do not depend on the matrix/spectral scaffolding in QXPLayer/Core.lean or QXPLayer/RankReduction/LowRank.lean; they are pure combinatorics over a chosen partition. The per-projector orthonormal range decomposition is available as MIPStarRE.Quantum.IsProj.rangeONB; the concrete Large/Small choice and truncated projectors are assembled in QXPLayer/RankReduction/LowRank.lean.

References

• references/ldt-paper/orthonormalization.tex lines 559–658 (proof of lem:projective-low-rank-sum, r > d branch).

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Truncation.exists_large_subset_ordered {α : Type u_1} [Fintype α] [DecidableEq α] (f : α → ℝ) {d : ℕ} (hd : d ≤ Fintype.card α) : ∃ (L : Finset α), L.card = d ∧ ∀ s ∈ Lᶜ, ∀ l ∈ L, f s ≤ f l

Choose d elements with the largest values of f, breaking ties arbitrarily. The resulting Large set has the paper's ordering property: every element outside Large has value at most every element of Large.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Truncation.card_mul_sum_small_le {α : Type u_1} {L S : Finset α} {f : α → ℝ} (hf : ∀ s ∈ S, ∀ l ∈ L, f s ≤ f l) : ↑L.card * ∑ s ∈ S, f s ≤ ↑S.card * ∑ l ∈ L, f l

Pairwise ordered double-counting.

If every element of S has value at most every element of L, the sum over S scaled by |L| is dominated by the sum over L scaled by |S|. Matches the paper's inequality ∑_{Small} o ≤ (|Small|/r) · ∑ o when L ∪ S exhausts the index set.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Truncation.card_univ_mul_sum_compl_le {α : Type u_1} [Fintype α] [DecidableEq α] (L : Finset α) {f : α → ℝ} (hf : ∀ s ∈ Lᶜ, ∀ l ∈ L, f s ≤ f l) : ↑(Fintype.card α) * ∑ s ∈ Lᶜ, f s ≤ ↑Lᶜ.card * ∑ x : α, f x

Partition-total form of the pairwise bound.

If S = Lᶜ, the paper's r · ∑_{Small} o ≤ |Small| · ∑ o follows from card_mul_sum_small_le after splitting ∑ x, f x = ∑_L f + ∑_{Lᶜ} f.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Truncation.sum_small_le_four_sqrt {α : Type u_1} [Fintype α] [DecidableEq α] (L : Finset α) {f : α → ℝ} {d : ℕ} {ζ : ℝ} (hL_card : L.card = d) (hcard_gt : d < Fintype.card α) (hr_bound : ↑(Fintype.card α) ≤ (1 + 2 * √ζ) * ↑d) (hf_ordering : ∀ s ∈ Lᶜ, ∀ l ∈ L, f s ≤ f l) (htotal : ∑ x : α, f x ≤ 1 + 2 * √ζ) (hζ_nonneg : 0 ≤ ζ) (hζ_le : ζ ≤ 1 / 4) : ∑ s ∈ Lᶜ, f s ≤ 4 * √ζ

Small-overlap sum bound.

Assuming the paper's inputs:

• L.card = d with d < |α|,
• |α| ≤ (1 + 2√ζ) · d,
• every Small = Lᶜ entry has value at most every Large = L entry,
• ∑ x, f x ≤ 1 + 2√ζ,
• 0 ≤ ζ ≤ 1/4,

this yields ∑_{Small} f ≤ 4√ζ, matching eq:small-overlaps in the paper. The Lean statement is slightly stronger than the paper's: it does not need f ≥ 0, since the ordering hypothesis and partition-total estimate already suffice. See docs/paper-gaps/truncation-combinatorics-f-nonneg.tex.