Gamma and accumulated-scale transport through subtree collapse

This file records the exact contraction ledgers used in paper §5.4.1. Restriction and geometric transport live in CollapseEmbedding; here the marker contribution is isolated from the unchanged retained branches.

Children at a contracted branch

def Anderson4D.collapseContractVertexEmbedding {t : PlaneTree} (r : t.VPos) : (t.contractAt ↑r).VPos ↪ t.VPos

Inclusion of all vertices retained by contraction.

Equations

• Anderson4D.collapseContractVertexEmbedding r = { toFun := Anderson4D.PlaneTree.contractVertex ⋯, inj' := ⋯ }

theorem Anderson4D.map_childrenOf_contractVertex_of_ne {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) : Finset.map (collapseContractVertexEmbedding r) (childrenOf v) = childrenOf (PlaneTree.contractVertex ⋯ v)

At a retained vertex distinct from the marker, the child finset maps exactly to the original child finset. The proof uses preservation of child counts to obtain surjectivity from the evident inclusion.

def Anderson4D.contractParentVertex {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) : (t.contractAt ↑r).VPos

A canonical retained copy of the original parent of a non-root contraction vertex.

Equations

• Anderson4D.contractParentVertex r hr0 = ⟨↑(Anderson4D.PlaneTree.parentV r), ⋯⟩

@[simp]

theorem Anderson4D.contractVertex_contractParentVertex {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) : PlaneTree.contractVertex ⋯ (contractParentVertex r hr0) = PlaneTree.parentV r

theorem Anderson4D.contractParentVertex_ne_marker {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) : ↑(contractParentVertex r hr0) ≠ ↑r

The contracted parent is not the marker.

theorem Anderson4D.contractMarker_mem_childrenOf_parent {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) : t.contractMarker ↑r ⋯ ∈ childrenOf (contractParentVertex r hr0)

The marker leaf is a child of the canonical contracted parent.

theorem Anderson4D.self_mem_childrenOf_parent {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) : r ∈ childrenOf (PlaneTree.parentV r)

The original subtree root is a child of its original parent.

theorem Anderson4D.map_leafChildren_contractParent {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) : Finset.map (collapseContractVertexEmbedding r) (leafChildren (contractParentVertex r hr0)) = insert r (leafChildren (PlaneTree.parentV r))

At the parent of the collapsed subtree, the contracted leaf children are the old leaf children together with the new marker (viewed at the original subtree-root position).

theorem Anderson4D.map_simpleChildren_contractParent {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (compound : Finset t.VPos) : Finset.map (collapseContractVertexEmbedding r) (childrenOf (contractParentVertex r hr0) ∩ simpleLeaves (t.contractAt ↑r) (contractCompound r compound)) = childrenOf (PlaneTree.parentV r) ∩ simpleLeaves t compound

At the contracted parent, simple leaf children are precisely the unchanged original simple leaf children; the marker is compound.

theorem Anderson4D.map_compoundChildren_contractParent {t : PlaneTree} (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (compound : Finset t.VPos) : Finset.map (collapseContractVertexEmbedding r) (childrenOf (contractParentVertex r hr0) ∩ compoundLeaves (t.contractAt ↑r) (contractCompound r compound)) = insert r (childrenOf (PlaneTree.parentV r) ∩ compoundLeaves t compound)

At the contracted parent, compound leaf children are the original compound leaf children together with the new marker.

The parent-node gamma increment

theorem Anderson4D.sum_contractMultiplicities_sub_one_map {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (S : Finset (t.contractAt ↑r).VPos) : ∑ u ∈ S, ((contractMultiplicities mu r s hs).m u - 1) = ∑ w ∈ Finset.map (collapseContractVertexEmbedding r) S, if w = r then s else mu.m w - 1

Reindex a contracted multiplicity-minus-one sum along the retained vertex embedding. The marker contributes exactly s; every other vertex keeps its original multiplicity.

theorem Anderson4D.sum_leafChildren_contractParent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) : ∑ l ∈ leafChildren (contractParentVertex r hr0), ((contractMultiplicities mu r s hs).m l - 1) = s + ∑ l ∈ leafChildren (PlaneTree.parentV r), (mu.m l - 1)

The leaf-child multiplicity sum at the contracted parent is the original sum plus the marker contribution s.

theorem Anderson4D.sum_compoundChildren_contractParent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (compound : Finset t.VPos) (s : ℕ) (hs : 1 ≤ s) : ∑ l ∈ childrenOf (contractParentVertex r hr0) ∩ compoundLeaves (t.contractAt ↑r) (contractCompound r compound), ((contractMultiplicities mu r s hs).m l - 1) = s + ∑ l ∈ childrenOf (PlaneTree.parentV r) ∩ compoundLeaves t compound, (mu.m l - 1)

The compound-child multiplicity sum at the contracted parent is the original sum plus the marker contribution s.

theorem Anderson4D.gammaInf_contract_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) : gammaInf (contractMultiplicities mu r s hs) (contractParentVertex r hr0) = gammaInf mu (PlaneTree.parentV r) + s

Paper (5.45)(iii), γ^∞ form. Replacing the branch child r by a compound marker of multiplicity s+1 increases the parent's exponent by exactly s.

theorem Anderson4D.gamma2_contract_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (compound : Finset t.VPos) (s : ℕ) (hs : 1 ≤ s) : gamma2 (contractMultiplicities mu r s hs) (contractCompound r compound) (contractParentVertex r hr0) = gamma2 mu compound (PlaneTree.parentV r) + s

Paper (5.45)(iii), γ² form. The contracted parent's γ² exponent is the original exponent plus exactly s.

Gamma exponents at all other retained branches

theorem Anderson4D.contractMarker_not_mem_childrenOf_of_ne_parent {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) : t.contractMarker ↑r ⋯ ∉ childrenOf v

Away from the original parent of r, the marker is not a child.

theorem Anderson4D.map_leafChildren_contractVertex_of_ne_parent {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) : Finset.map (collapseContractVertexEmbedding r) (leafChildren v) = leafChildren (PlaneTree.contractVertex ⋯ v)

At a retained vertex other than the collapsed subtree's parent, leaf children map exactly to the original leaf children.

theorem Anderson4D.map_simpleChildren_contractVertex_of_ne_parent {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (compound : Finset t.VPos) : Finset.map (collapseContractVertexEmbedding r) (childrenOf v ∩ simpleLeaves (t.contractAt ↑r) (contractCompound r compound)) = childrenOf (PlaneTree.contractVertex ⋯ v) ∩ simpleLeaves t compound

Simple leaf children are unchanged away from the collapsed subtree's parent.

theorem Anderson4D.map_compoundChildren_contractVertex_of_ne_parent {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (compound : Finset t.VPos) : Finset.map (collapseContractVertexEmbedding r) (childrenOf v ∩ compoundLeaves (t.contractAt ↑r) (contractCompound r compound)) = childrenOf (PlaneTree.contractVertex ⋯ v) ∩ compoundLeaves t compound

Compound leaf children are unchanged away from the collapsed subtree's parent.

theorem Anderson4D.sum_leafChildren_contractVertex_of_ne_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (s : ℕ) (hs : 1 ≤ s) : ∑ l ∈ leafChildren v, ((contractMultiplicities mu r s hs).m l - 1) = ∑ l ∈ leafChildren (PlaneTree.contractVertex ⋯ v), (mu.m l - 1)

The leaf-child multiplicity sum is unchanged at every retained branch other than the collapsed subtree's parent.

theorem Anderson4D.sum_compoundChildren_contractVertex_of_ne_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (compound : Finset t.VPos) (s : ℕ) (hs : 1 ≤ s) : ∑ l ∈ childrenOf v ∩ compoundLeaves (t.contractAt ↑r) (contractCompound r compound), ((contractMultiplicities mu r s hs).m l - 1) = ∑ l ∈ childrenOf (PlaneTree.contractVertex ⋯ v) ∩ compoundLeaves t compound, (mu.m l - 1)

The compound-child multiplicity sum is likewise unchanged away from the collapsed subtree's parent.

theorem Anderson4D.gammaInf_contract_of_ne_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (s : ℕ) (hs : 1 ≤ s) : gammaInf (contractMultiplicities mu r s hs) v = gammaInf mu (PlaneTree.contractVertex ⋯ v)

γ^∞ is unchanged at every retained branch other than the parent of the collapsed subtree.

theorem Anderson4D.gamma2_contract_of_ne_parent {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hv : ↑v ≠ ↑r) (hparent : PlaneTree.contractVertex ⋯ v ≠ PlaneTree.parentV r) (compound : Finset t.VPos) (s : ℕ) (hs : 1 ≤ s) : gamma2 (contractMultiplicities mu r s hs) (contractCompound r compound) v = gamma2 mu compound (PlaneTree.contractVertex ⋯ v)

γ² is unchanged at every retained branch other than the parent of the collapsed subtree.

Accumulated-scale ledger under contraction

theorem Anderson4D.map_branchNodesUnder_contractVertex {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) : Finset.map (collapseContractVertexEmbedding r) (branchNodesUnder v) = {u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) | ¬↑r <+: ↑u}

Descendant branches of the contracted tree are exactly the descendant branches of the original tree that do not lie in the removed rooted subtree.

theorem Anderson4D.gammaInf_contract_branch_formula {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) (v : (t.contractAt ↑r).VPos) (hvBranch : v ∈ (t.contractAt ↑r).BranchNodes) : gammaInf (contractMultiplicities mu r s hs) v = gammaInf mu (PlaneTree.contractVertex ⋯ v) + if PlaneTree.contractVertex ⋯ v = PlaneTree.parentV r then s else 0

Unified pointwise contraction ledger on branch nodes: the original exponent is retained, with one extra s exactly at the parent of the collapsed subtree.

theorem Anderson4D.accumulatedScale_contract_eq_retained_sum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) (v : (t.contractAt ↑r).VPos) : accumulatedScale (contractMarking Nm r) (contractMultiplicities mu r s hs) v = ∑ u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) with ¬↑r <+: ↑u, (gammaInf mu u + if u = PlaneTree.parentV r then s else 0) * scaleN Nm u

Exact retained-branch form of the contracted accumulated scale. It exhibits explicitly that the sole local change is the extra parent mass s * N_{parent(r)}; the removed subtree branches are absent from the filtered index set.

theorem Anderson4D.retainedBranches_union_removed {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hvr : ↑(PlaneTree.contractVertex ⋯ v) <+: ↑r) : {u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) | ¬↑r <+: ↑u} ∪ branchNodesUnder r = branchNodesUnder (PlaneTree.contractVertex ⋯ v)

If a retained vertex is above the contraction root, its original descendant branches split into the retained branches and exactly the branches of the removed rooted subtree.

theorem Anderson4D.retainedBranches_disjoint_removed {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) : Disjoint ({u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) | ¬↑r <+: ↑u}) (branchNodesUnder r)

The retained and removed branch pieces are disjoint.

theorem Anderson4D.retainedBranches_eq_all_of_incomparable {t : PlaneTree} (r : t.VPos) (v : (t.contractAt ↑r).VPos) (hvr : ¬↑(PlaneTree.contractVertex ⋯ v) <+: ↑r) (hrv : ¬↑r <+: ↑(PlaneTree.contractVertex ⋯ v)) : {u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) | ¬↑r <+: ↑u} = branchNodesUnder (PlaneTree.contractVertex ⋯ v)

If the retained vertex and contraction root are incomparable, no branch below the retained vertex is removed.

theorem Anderson4D.parent_mem_retainedBranches {t : PlaneTree} (ht : t.isValid = true) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (v : (t.contractAt ↑r).VPos) (hvBranch : v ∈ (t.contractAt ↑r).BranchNodes) (hvr : ↑(PlaneTree.contractVertex ⋯ v) <+: ↑r) : PlaneTree.parentV r ∈ {u ∈ branchNodesUnder (PlaneTree.contractVertex ⋯ v) | ¬↑r <+: ↑u}

When the retained branch is above r, the original parent of r belongs to the retained descendant-branch set.

theorem Anderson4D.accumulatedScale_le_contract {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) (habsorb : accumulatedScale Nm mu r ≤ s * scaleN Nm (PlaneTree.parentV r)) (v : (t.contractAt ↑r).VPos) (hvBranch : v ∈ (t.contractAt ↑r).BranchNodes) : accumulatedScale Nm mu (PlaneTree.contractVertex ⋯ v) ≤ accumulatedScale (contractMarking Nm r) (contractMultiplicities mu r s hs) v

Accumulated-scale absorption for contraction. If the marker's extra parent mass absorbs the removed subtree's accumulated scale, then every contracted branch has at least the accumulated scale of its original representative. This is the arithmetic input expected by satisfiesSubtreeDiameter_contract_of_accumulatedScale.

theorem Anderson4D.satisfiesSubtreeDiameter_contract {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (lstar : InsideLeaf r) (s : ℕ) (hs : 1 ≤ s) (hz : SatisfiesSubtreeDiameter Nm mu z) (habsorb : accumulatedScale Nm mu r ≤ s * scaleN Nm (PlaneTree.parentV r)) : SatisfiesSubtreeDiameter (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractEmbedding z r lstar)

Direct diameter-transport interface with the corrected absorption hypothesis.

theorem Anderson4D.accumulatedScale_le_contract_of_eligible {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (r : t.VPos) (hr : CollapseEligible Nm mu r) (s : ℕ) (hs : 1 ≤ s) (v : (t.contractAt ↑r).VPos) (hvBranch : v ∈ (t.contractAt ↑r).BranchNodes) : accumulatedScale Nm mu (PlaneTree.contractVertex ⋯ v) ≤ accumulatedScale (contractMarking Nm r) (contractMultiplicities mu r s hs) v

Eligibility supplies the absorption hypothesis automatically (already with factor eight to spare).

theorem Anderson4D.satisfiesSubtreeDiameter_contract_of_eligible {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (hr : CollapseEligible Nm mu r) (lstar : InsideLeaf r) (s : ℕ) (hs : 1 ≤ s) (hz : SatisfiesSubtreeDiameter Nm mu z) : SatisfiesSubtreeDiameter (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractEmbedding z r lstar)

Paper-facing eligible form of contracted diameter transport.