Exact branch-power ledger under subtree collapse

This module packages the γ² contribution to paper (5.45). Restriction contributes exactly the original branches below the collapse root, while contraction contributes exactly the retained branches and one additional -2s power at the original parent of the collapse root.

Original branch factors and their partition

noncomputable def Anderson4D.gamma2BranchFactor {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (v : t.VPos) : ℝ

The individual γ² factor occurring in singleScaleBranchPower.

Equations

• Anderson4D.gamma2BranchFactor Nm mu compound v = ↑(Anderson4D.scaleN Nm v) ^ (-2 * (↑(Anderson4D.gamma2 mu compound v) - 1))

noncomputable def Anderson4D.insideGamma2BranchPower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : ℝ

Original branch power over the branches weakly below r.

Equations

• Anderson4D.insideGamma2BranchPower Nm mu compound r = ∏ v : Anderson4D.PlaneTree.DescendantBranches r, Anderson4D.gamma2BranchFactor Nm mu compound ↑↑v

noncomputable def Anderson4D.retainedGamma2BranchPower {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : ℝ

Original branch power over the branches retained by contraction at r.

Equations

• Anderson4D.retainedGamma2BranchPower Nm mu compound r = ∏ v : t.BranchesOutside ↑r, Anderson4D.gamma2BranchFactor Nm mu compound ↑↑v

def Anderson4D.branchInsideOutsideEquiv {t : PlaneTree} (r : t.VPos) : ↥t.BranchNodes ≃ PlaneTree.DescendantBranches r ⊕ t.BranchesOutside ↑r

Original branches split into those weakly below r and those retained by contraction.

Equations

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

theorem Anderson4D.singleScaleBranchPower_eq_inside_mul_retained {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : singleScaleBranchPower Nm mu compound = insideGamma2BranchPower Nm mu compound r * retainedGamma2BranchPower Nm mu compound r

Exact partition of the original γ² branch power.

Restricted branch power

theorem Anderson4D.singleScaleBranchPower_restrict {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : singleScaleBranchPower (restrictMarking Nm r) (restrictMultiplicities mu r) (restrictCompound r compound) = insideGamma2BranchPower Nm mu compound r

Restriction contributes exactly the original branch factors below r.

Contracted branch power

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

Pointwise γ² ledger at every contracted branch.

theorem Anderson4D.gamma2BranchFactor_contract {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (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) : gamma2BranchFactor (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractCompound r compound) v = gamma2BranchFactor Nm mu compound (PlaneTree.contractVertex ⋯ v) * if PlaneTree.contractVertex ⋯ v = PlaneTree.parentV r then ↑(scaleN Nm (PlaneTree.parentV r)) ^ (-2 * ↑s) else 1

The contracted pointwise factor is the retained original factor, with an additional -2s parent-scale power exactly at parent(r).

def Anderson4D.collapseParentOutsideBranch {t : PlaneTree} (ht : t.isValid = true) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) : t.BranchesOutside ↑r

The parent of a non-root branch is retained by contraction.

Equations

• Anderson4D.collapseParentOutsideBranch ht r hr0 hrBranch = ⟨⟨Anderson4D.PlaneTree.parentV r, ⋯⟩, ⋯⟩

theorem Anderson4D.prod_parentScaleBonus {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) : (∏ v : t.BranchesOutside ↑r, if ↑↑v = PlaneTree.parentV r then ↑(scaleN Nm (PlaneTree.parentV r)) ^ (-2 * ↑s) else 1) = ↑(scaleN Nm (PlaneTree.parentV r)) ^ (-2 * ↑s)

The extra parent factor is a one-point product over retained branches.

theorem Anderson4D.singleScaleBranchPower_contract {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) : singleScaleBranchPower (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractCompound r compound) = retainedGamma2BranchPower Nm mu compound r * ↑(scaleN Nm (PlaneTree.parentV r)) ^ (-2 * ↑s)

Contraction contributes the retained original branch power and precisely one extra -2s power at the parent of r.

Complete (5.45) branch-power identity

theorem Anderson4D.singleScaleBranchPower_restrict_mul_contract {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hr0 : r ≠ t.rootV) (hrBranch : r ∈ t.BranchNodes) (s : ℕ) (hs : 1 ≤ s) : singleScaleBranchPower (restrictMarking Nm r) (restrictMultiplicities mu r) (restrictCompound r compound) * singleScaleBranchPower (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractCompound r compound) = singleScaleBranchPower Nm mu compound * ↑(scaleN Nm (PlaneTree.parentV r)) ^ (-2 * ↑s)

Exact γ² branch-power ledger used in the collapse induction.