8.2. Selecting a sparse subgraph
Fix a twist-equality partition with t \ge 2 blocks. Contracting each
block to a vertex leaves the simple support graph J, one edge per pair of
blocks joined by at least one pin, with m_e pins on the edge e; when
some pair carries three or more pins, the pin-fibre
lemma forces those pins collinear, which is the first case of
Proposition 6.5 below, so this section assumes m_e \in \{1, 2\} and sets
M = \sum_e m_e and R = \max\{0,\ 6(t-1) - 2M\}. The paper selects the
subgraph with the matroid-union theorem, in the union of two copies of the
graphic matroid of J: independence there means a partition into two
forests, which the forest-decomposition theorem of
Nash-Williams (1964) identifies with the (2,2)-sparsity
counts, and the matroid-union rank formula of
Edmonds (1965) evaluates the maximum size of an
independent set as a minimum over vertex partitions.
Suppose m_e \in \{1, 2\} for every edge of the support graph J and
that H satisfies the partition inequality (1.2). Then J contains a
spanning (2,2)-sparse subgraph F with exactly R edges.
(Zheng, 2026, Lemma 6.3)
Lean code for Lemma8.2.1●2 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/Sparse22/OptimalPartition.leancomplete
theorem RB31E2E.exists_sparse22_of_all_partition_terms.{u_1} {V : Type u_1} [DecidableEq V] [Fintype V] (J : RB31E2E.SimpleEdgeSet V) (R : ℕ) (hR : ∀ (P : Finpartition Finset.univ), R ≤ RB31E2E.sparsePartitionTerm J P) : ∃ F ⊆ J, RB31E2E.Sparse22 F ∧ Finset.card F = R
theorem RB31E2E.exists_sparse22_of_all_partition_terms.{u_1} {V : Type u_1} [DecidableEq V] [Fintype V] (J : RB31E2E.SimpleEdgeSet V) (R : ℕ) (hR : ∀ (P : Finpartition Finset.univ), R ≤ RB31E2E.sparsePartitionTerm J P) : ∃ F ⊆ J, RB31E2E.Sparse22 F ∧ Finset.card F = R
If every partition term is at least `R`, then `J` has an `R`-edge `(2,2)`-sparse subset. This is the extraction statement needed by the body--pin bridge and does not invoke a graphic-matroid-union API.
-
theoremdefined in RB31EndToEnd/Combinatorics/BodyPinSparseSkeleton.leancomplete
theorem RB31E2E.BodyPinIncidence.exists_sparse_nullSkeleton (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (hπ : Function.Surjective π) (ht : 2 ≤ t) (hpartition : H.PartitionCondition) (hsmall : ∀ e ∈ H.fineSupportOn π, H.fineMultiplicityOn π e ≤ 2) : ∃ F ⊆ H.fineSupportOn π, RB31E2E.Sparse22 F ∧ Finset.card F = H.sparseSkeletonTarget π
theorem RB31E2E.BodyPinIncidence.exists_sparse_nullSkeleton (H : RB31E2E.BodyPinIncidence) {t : ℕ} (π : H.Body → Fin t) (hπ : Function.Surjective π) (ht : 2 ≤ t) (hpartition : H.PartitionCondition) (hsmall : ∀ e ∈ H.fineSupportOn π, H.fineMultiplicityOn π e ≤ 2) : ∃ F ⊆ H.fineSupportOn π, RB31E2E.Sparse22 F ∧ Finset.card F = H.sparseSkeletonTarget π
The body--pin partition condition extracts a simple `(2,2)`-sparse null skeleton whenever every nonempty fine bundle contains at most two pins. The explicit hypothesis `2 ≤ t` is the weakest case needed by the nontrivial equality-cellule argument. The zero- and one-label cases have target zero and are intentionally left out of this interface.
If 6(t-1) - 2M \le 0 take F empty, so assume it positive. It is enough
that every term of the rank formula (6.5) is at least 6(t-1) - 2M; for a
partition Q with r blocks this is the inequality
2M + s_{\mathrm{cross}} \ge 4t + 2r - 6. The capacity of the block pair
carrying m_e \in \{1,2\} pins is 2m_e + 1, so the partition condition
at the twist-equality partition itself gives 2M + |E(J)| \ge 6(t-1). If
s_{\mathrm{int}} \le 2(t - r), subtracting it gives the inequality. If
s_{\mathrm{int}} \ge 2(t - r), then 2M_{\mathrm{int}} \ge
2 s_{\mathrm{int}} \ge 4(t - r); lifting Q to a partition of the bodies
with r blocks, each coarse capacity is at most the sum of the fine
capacities it contains, so the partition condition gives
2M_{\mathrm{cross}} + s_{\mathrm{cross}} \ge 6(r-1), and adding the two
inequalities gives the claim. Hence r_2(J) \ge R, and an independent
R-element set is the required subgraph.
The formalization uses no matroid at all — no Nash–Williams, no Edmonds, no
matroid API in the import closure — and proves the same minimum only in the
direction it needs, by constructing the optimal partition explicitly. Take a
maximum-cardinality (2,2)-sparse subset F \subseteq J. Every omitted
edge, if added, would violate sparsity, so by
the addable-edge criterion some tight set
contains its endpoints. Singletons are tight, and by
uncrossing the union of the tight sets through a
vertex is tight, so the tight hulls partition the vertices into maximal
tight blocks with every omitted edge internal to a block. Summing tightness
over the blocks counts the internal edges exactly, and so
/-- The partition expression associated with a simple support. -/
noncomputable def sparsePartitionTerm (J : SimpleEdgeSet V)
(P : Finpartition (Finset.univ : Finset V)) : ℕ :=
2 * (Fintype.card V - P.parts.card) + (crossEdges J P).card
is attained by F at that one partition:
card_eq_sparsePartitionTerm
gives |F| = 2(|V(J)| - |Q|) + s_{\mathrm{cross}}(Q) for the tight-hull
partition Q. Consequently, if every partition term is at least R, a
maximum sparse subset has at least R edges, and any R of them form the
required subgraph; that is
exists_sparse22_of_all_partition_terms,
whose source carries the comment that no graphic-matroid-union interface is
invoked. The paper needs the hard direction of the rank formula, that the
minimum is attained; the formalization needs only this constructive half,
and the converse bound, that every sparse subset is at most every partition
term, is proved in the same module and is not reachable from the root
theorem; the register has the entry.
The body–pin side is
exists_sparse_nullSkeleton:
under the partition condition, with every nonzero cross-block multiplicity
at most two, the support of the cross-block pins contains a sparse subgraph
of exactly the deficit cardinality
/-- The deficit which must be paid by a sparse null skeleton. -/
noncomputable def sparseSkeletonTarget (H : BodyPinIncidence)
{t : ℕ} (π : H.Body → Fin t) : ℕ :=
6 * (t - 1) - 2 * H.fineMassOn π
where truncated subtraction over \N gives the paper's
\max\{0, \cdot\}. Its partition-term hypothesis is proved from the
partition condition without contracting to J: the capacity of a one- or
two-pin bundle is exactly 2m_e + 1, so the fine partition condition reads
6(t-1) \le 2M + |E(J)|, and an aggregation inequality —
capacityOn_comp_le_two_mul_crossingFineMass_add_card,
that coarsening the labels never increases capped capacity beyond
2M + s of the fine crossing data — turns the partition condition at each
coarsening into the corresponding Edmonds term.