Geometric transport through the Proposition 5.9 collapse

This file connects the structural subtree/contraction operations to the embedding hypotheses used by Propositions 5.9 and 5.10.

Subtree incidence and scale transport

def Anderson4D.subtreeVertexEmbedding {t : PlaneTree} (r : t.VPos) : (t.subtreeAt ↑r).VPos ↪ t.VPos

The vertex inclusion of a rooted subtree, packaged as an embedding for finite-set transport.

Equations

• Anderson4D.subtreeVertexEmbedding r = { toFun := Anderson4D.PlaneTree.subtreeVertex r, inj' := ⋯ }

theorem Anderson4D.lcaPath_append_left (r p q : List ℕ) : lcaPath (r ++ p) (r ++ q) = r ++ lcaPath p q

Prepending the same path to both inputs commutes with their longest common prefix.

theorem Anderson4D.subtreeVertex_lcaV {t : PlaneTree} (r : t.VPos) (v w : (t.subtreeAt ↑r).VPos) : PlaneTree.subtreeVertex r (lcaV v w) = lcaV (PlaneTree.subtreeVertex r v) (PlaneTree.subtreeVertex r w)

LCA is preserved by the rooted-subtree vertex inclusion.

theorem Anderson4D.map_childrenOf_subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : Finset.map (subtreeVertexEmbedding r) (childrenOf v) = childrenOf (PlaneTree.subtreeVertex r v)

Children in a rooted subtree are exactly the original children of the included vertex.

theorem Anderson4D.mem_childrenOf_subtreeVertex_iff {t : PlaneTree} (r : t.VPos) (v w : (t.subtreeAt ↑r).VPos) : w ∈ childrenOf v ↔ PlaneTree.subtreeVertex r w ∈ childrenOf (PlaneTree.subtreeVertex r v)

Membership form of map_childrenOf_subtreeVertex.

theorem Anderson4D.map_leafChildren_subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : Finset.map (subtreeVertexEmbedding r) (leafChildren v) = leafChildren (PlaneTree.subtreeVertex r v)

Leaf children transport along the same inclusion.

theorem Anderson4D.gammaInf_restrictMultiplicities {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : gammaInf (restrictMultiplicities mu r) v = gammaInf mu (PlaneTree.subtreeVertex r v)

γ^∞ is unchanged at every branch of the restricted subtree.

theorem Anderson4D.map_branchNodesUnder_subtreeVertex {t : PlaneTree} (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : Finset.map (subtreeVertexEmbedding r) (branchNodesUnder v) = branchNodesUnder (PlaneTree.subtreeVertex r v)

Descendant branch sets transport exactly into the original tree.

theorem Anderson4D.accumulatedScale_restrict {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (r : t.VPos) (v : (t.subtreeAt ↑r).VPos) : accumulatedScale (restrictMarking Nm r) (restrictMultiplicities mu r) v = accumulatedScale Nm mu (PlaneTree.subtreeVertex r v)

The accumulated scale is unchanged under restriction.

Restricted single-scale and embedding hypotheses

theorem Anderson4D.lowestEligible_restrict_singleScale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {r : t.VPos} (hr : IsLowestCollapseEligible Nm mu r) : SatisfiesSingleScaleCondition (restrictMarking Nm r) (restrictMultiplicities mu r)

A lowest eligible branch has no eligible proper descendant, hence its restricted subtree satisfies the single-scale condition of Proposition 5.10.

theorem Anderson4D.eligible_restrict_p5Parameters {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {r : t.VPos} (hr : CollapseEligible Nm mu r) : IsDyadicNat (scaleN Nm (PlaneTree.parentV r)) ∧ accumulatedScale (restrictMarking Nm r) (restrictMultiplicities mu r) (t.subtreeAt ↑r).rootV ≤ scaleN Nm (PlaneTree.parentV r)

The parent scale of the collapsed root supplies exactly the dyadic scale and root accumulated-scale bound needed by the restricted P-5.10 call.

@[simp]

theorem Anderson4D.restrictLeafEquiv_vertex {t : PlaneTree} (r : t.VPos) (l : HeppLeaf (t.subtreeAt ↑r)) : ↑↑((restrictLeafEquiv r) l) = PlaneTree.subtreeVertex r ↑l

theorem Anderson4D.isSeparatedEmbedding_restrict {t : PlaneTree} (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (hz : IsSeparatedEmbedding Nm z) : IsSeparatedEmbedding (restrictMarking Nm r) (restrictEmbedding z r)

Restriction preserves separatedness, including injectivity and the exact LCA scale.

theorem Anderson4D.satisfiesSubtreeDiameter_restrict {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (hz : SatisfiesSubtreeDiameter Nm mu z) : SatisfiesSubtreeDiameter (restrictMarking Nm r) (restrictMultiplicities mu r) (restrictEmbedding z r)

Restriction preserves every subtree-diameter inequality exactly.

Contracted embedding

theorem Anderson4D.lcaPath_append_tail_of_not_prefix (r tail q : List ℕ) (hq : ¬r <+: q) : lcaPath (r ++ tail) q = lcaPath r q

Extending the left input below r does not change its LCA with a path outside r.

def Anderson4D.contractRepresentativeLeaf {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) : HeppLeaf (t.contractAt ↑r) → HeppLeaf t

The original leaf represented by a contracted leaf: the marker is sent to lstar, while outside leaves are unchanged.

Equations

• Anderson4D.contractRepresentativeLeaf r lstar l = Sum.elim (fun (x : Unit) => ↑lstar) (fun (lout : Anderson4D.OutsideLeaf r) => ↑lout) ((Anderson4D.contractLeafSumEquiv r) l)

@[simp]

theorem Anderson4D.contractRepresentativeLeaf_marker {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) : contractRepresentativeLeaf r lstar (contractMarkerLeaf r) = ↑lstar

@[simp]

theorem Anderson4D.contractRepresentativeLeaf_outside {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) (l : OutsideLeaf r) : contractRepresentativeLeaf r lstar (contractOutsideLeaf r l) = ↑l

theorem Anderson4D.contractEmbedding_eq_comp_representative {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) : contractEmbedding z r lstar = z ∘ contractRepresentativeLeaf r lstar

Contracting an embedding is composition with the representative-leaf map.

theorem Anderson4D.contractRepresentativeLeaf_injective {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) : Function.Injective (contractRepresentativeLeaf r lstar)

Choosing one inside representative and retaining every outside leaf is an injective map on the contracted leaf carrier.

theorem Anderson4D.contractVertex_lcaV_marker_outside {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) (lout : OutsideLeaf r) : PlaneTree.contractVertex ⋯ (lcaV ↑(contractMarkerLeaf r) ↑(contractOutsideLeaf r lout)) = lcaV ↑↑lstar ↑↑lout

LCA transport for the marker and an unchanged outside leaf.

theorem Anderson4D.contractVertex_lcaV_outside_outside {t : PlaneTree} (r : t.VPos) (lout lout' : OutsideLeaf r) : PlaneTree.contractVertex ⋯ (lcaV ↑(contractOutsideLeaf r lout) ↑(contractOutsideLeaf r lout')) = lcaV ↑↑lout ↑↑lout'

LCA transport for two unchanged outside leaves.

theorem Anderson4D.scaleN_lca_contractRepresentative_of_ne {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (lstar : InsideLeaf r) {l l' : HeppLeaf (t.contractAt ↑r)} (hne : l ≠ l') : scaleN (contractMarking Nm r) (lcaV ↑l ↑l') = scaleN Nm (lcaV ↑(contractRepresentativeLeaf r lstar l) ↑(contractRepresentativeLeaf r lstar l'))

At distinct contracted leaves, the contracted LCA scale is exactly the original LCA scale of their representatives.

theorem Anderson4D.isSeparatedEmbedding_contract {t : PlaneTree} (Nm : t.HeppMarking) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (hz : IsSeparatedEmbedding Nm z) : IsSeparatedEmbedding (contractMarking Nm r) (contractEmbedding z r lstar)

The contracted embedding remains separated. Eligibility is not needed for this structural fact; it enters the boundary-edge comparison below.

theorem Anderson4D.contractEmbedding_boundary_quarter {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hsep : IsSeparatedEmbedding Nm z) (hdiam : SatisfiesSubtreeDiameter Nm mu z) {r : t.VPos} (hr : CollapseEligible Nm mu r) (l lstar : InsideLeaf r) (y : OutsideLeaf r) : 4 * znorm (z ↑l - contractEmbedding z r lstar (contractMarkerLeaf r)) ≤ znorm (contractEmbedding z r lstar (contractOutsideLeaf r y) - z ↑l)

The eligible quarter-distance estimate expressed using the contracted marker and an unchanged contracted outside leaf. This is the geometric input for charging every changed boundary edge by 2.

theorem Anderson4D.contractRepresentativeLeaf_mem_leavesUnder {t : PlaneTree} (r : t.VPos) (lstar : InsideLeaf r) (v : (t.contractAt ↑r).VPos) (l : HeppLeaf (t.contractAt ↑r)) (hl : l ∈ leavesUnder v) : contractRepresentativeLeaf r lstar l ∈ leavesUnder (PlaneTree.contractVertex ⋯ v)

A contracted leaf below v represents an original leaf below the unchanged original vertex corresponding to v.

theorem Anderson4D.satisfiesSubtreeDiameter_contract_of_accumulatedScale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (r : t.VPos) (lstar : InsideLeaf r) (s : ℕ) (hs : 1 ≤ s) (hz : SatisfiesSubtreeDiameter Nm mu z) (haccumulated : ∀ v ∈ (t.contractAt ↑r).BranchNodes, accumulatedScale Nm mu (PlaneTree.contractVertex ⋯ v) ≤ accumulatedScale (contractMarking Nm r) (contractMultiplicities mu r s hs) v) : SatisfiesSubtreeDiameter (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractEmbedding z r lstar)

Diameter transport through contraction, isolated at its exact remaining arithmetic input: the contracted accumulated scale must dominate the original accumulated scale at every surviving branch. The leaf geometry and all carrier transport are discharged here; a later γ^∞ collapse ledger can supply haccumulated.