Multiplicity ledgers for the collapse induction

This module records the three elementary mass facts used in the final assembly of Proposition 5.9: a branching subtree carries at least four copies, the original mass splits into its inside and outside parts, and a skipped branch set in the contracted tree is paid for by the multiplicity away from the new marker leaf.

theorem Anderson4D.four_le_totalMultiplicity_of_root_mem_BranchNodes {t : PlaneTree} (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) : 4 ≤ totalMultiplicity mu

A tree whose root branches carries at least four copies: it has at least two leaves and every leaf multiplicity is at least two.

theorem Anderson4D.four_le_totalMultiplicity_restrict {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr : r ∈ t.BranchNodes) : 4 ≤ totalMultiplicity (restrictMultiplicities mu r)

The inside mass of a selected branch is at least four.

theorem Anderson4D.totalMultiplicity_eq_restrict_add_outside {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : totalMultiplicity mu = totalMultiplicity (restrictMultiplicities mu r) + outsideMultiplicityTotal mu r

Original mass is the restricted mass plus the unchanged outside mass.

theorem Anderson4D.sum_contractMultiplicity_erase_marker {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) : ∑ l ∈ Finset.univ.erase (contractMarkerLeaf r), leafMultiplicity (contractMultiplicities mu r s hs) l = outsideMultiplicityTotal mu r

The sum of contracted multiplicities away from the marker is exactly the original outside mass.

theorem Anderson4D.two_mul_card_contractW_le_outsideMultiplicityTotal {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) (hs : 1 ≤ s) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : 2 * W.card ≤ outsideMultiplicityTotal mu r

Every skipped set in the contracted tree satisfies the off-marker cardinality hypothesis used in the factorial comparison (5.47).