Scale-ratio transport through restriction and contraction

The markings constructed in CollapseData preserve branch scales. This module records the corresponding parent-ratio identities used in the factor audit (5.45)--(5.46).

@[simp]

theorem Anderson4D.scaleN_restrictMarking_root {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) : scaleN (restrictMarking Nm r) (t.subtreeAt ↑r).rootV = scaleN Nm r

The root scale of the restricted subtree is the original scale at the selected branch.

theorem Anderson4D.parentScaleRatio_restrictMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) (hv : v ∈ nonrootBranches (t.subtreeAt ↑r)) : parentScaleRatio (restrictMarking Nm r) v = parentScaleRatio Nm (PlaneTree.subtreeVertex r v)

Parent ratios of non-root subtree branches are unchanged.

@[simp]

theorem Anderson4D.parentScaleRatio_contractMarking {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (v : (t.contractAt ↑r).VPos) : parentScaleRatio (contractMarking Nm r) v = parentScaleRatio Nm (PlaneTree.contractVertex ⋯ v)

Parent ratios of all contracted vertices are unchanged. Mathematical uses specialize this to contracted non-root branches.

theorem Anderson4D.subtreeVertex_mem_nonrootBranches {t : PlaneTree} (r : t.VPos) {v : (t.subtreeAt ↑r).VPos} (hv : v ∈ nonrootBranches (t.subtreeAt ↑r)) : PlaneTree.subtreeVertex r v ∈ nonrootBranches t

A non-root branch in the restricted subtree maps to an original non-root branch.

def Anderson4D.subtreeNonrootBranchEmbedding {t : PlaneTree} (r : t.VPos) : ↥(nonrootBranches (t.subtreeAt ↑r)) ↪ ↥(nonrootBranches t)

The restricted subtree's non-root branches embed in the original branch set, preserving address order and scale ratios.

Equations

• Anderson4D.subtreeNonrootBranchEmbedding r = { toFun := fun (v : ↥(Anderson4D.nonrootBranches (t.subtreeAt ↑r))) => ⟨Anderson4D.PlaneTree.subtreeVertex r ↑v, ⋯⟩, inj' := ⋯ }