Parent-scale-ratio ledger for the collapse induction

This file isolates the exact product bookkeeping in paper (5.45)--(5.46). The original non-root branches split into the selected branch, its strict branch descendants, and the branches retained by contraction.

The exact branch partition

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

Inclusion of every subtree vertex into the original tree.

Equations

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

def Anderson4D.liftSubtreeNonrootBranches {t : PlaneTree} (r : t.VPos) : Finset t.VPos

Original branches strictly below r, represented as a finset in the original vertex type.

Equations

• Anderson4D.liftSubtreeNonrootBranches r = Finset.map (Anderson4D.ratioSubtreeVertexEmbedding r) (Anderson4D.nonrootBranches (t.subtreeAt ↑r))

@[simp]

theorem Anderson4D.mem_liftSubtreeNonrootBranches_iff {t : PlaneTree} (r v : t.VPos) : v ∈ liftSubtreeNonrootBranches r ↔ ∃ u ∈ nonrootBranches (t.subtreeAt ↑r), PlaneTree.subtreeVertex r u = v

theorem Anderson4D.liftSubtreeNonrootBranches_subset {t : PlaneTree} (r : t.VPos) : liftSubtreeNonrootBranches r ⊆ nonrootBranches t

Every lifted strict descendant branch is an original non-root branch.

theorem Anderson4D.not_mem_liftSubtreeNonrootBranches {t : PlaneTree} (r : t.VPos) : r ∉ liftSubtreeNonrootBranches r

The selected root itself is not among its strict branch descendants.

theorem Anderson4D.prefix_of_mem_liftSubtreeNonrootBranches {t : PlaneTree} (r : t.VPos) {v : t.VPos} (hv : v ∈ liftSubtreeNonrootBranches r) : ↑r <+: ↑v

Lifted strict descendants really are weakly below r.

theorem Anderson4D.mem_liftSubtreeNonrootBranches_of_prefix {t : PlaneTree} (r : t.VPos) {v : t.VPos} (hv : v ∈ nonrootBranches t) (hprefix : ↑r <+: ↑v) (hne : v ≠ r) : v ∈ liftSubtreeNonrootBranches r

A strict descendant original branch belongs to the lifted subtree branch set.

theorem Anderson4D.mem_liftContract_nonrootBranches_of_not_prefix {t : PlaneTree} (r : t.VPos) {v : t.VPos} (hv : v ∈ nonrootBranches t) (hprefix : ¬↑r <+: ↑v) : v ∈ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r))

An original non-root branch outside the selected subtree is retained as a contracted non-root branch.

theorem Anderson4D.not_prefix_of_mem_liftContract_nonrootBranches {t : PlaneTree} (r : t.VPos) {v : t.VPos} (hv : v ∈ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r))) : ¬↑r <+: ↑v

Contracted branch images cannot lie below the selected subtree root.

theorem Anderson4D.disjoint_liftSubtree_liftContract_nonrootBranches {t : PlaneTree} (r : t.VPos) : Disjoint (liftSubtreeNonrootBranches r) (liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r)))

The strict-descendant and contraction pieces are disjoint.

theorem Anderson4D.nonrootBranches_eq_collapse_partition {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) : nonrootBranches t = insert r (liftSubtreeNonrootBranches r) ∪ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r))

Exact trichotomy of original non-root branches: r, strict descendants of r, and branches surviving contraction.

Finset and product reindexing

theorem Anderson4D.liftContractFinset_sdiff {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) (S W : Finset (t.contractAt p).VPos) : liftContractFinset hp (S \ W) = liftContractFinset hp S \ liftContractFinset hp W

theorem Anderson4D.liftContractFinset_mono {t : PlaneTree} {p : PlaneTree.Pos} (hp : t.IsPos p) {S W : Finset (t.contractAt p).VPos} (h : W ⊆ S) : liftContractFinset hp W ⊆ liftContractFinset hp S

theorem Anderson4D.prod_liftSubtreeNonrootBranches {t : PlaneTree} {M : Type u_1} [CommMonoid M] (r : t.VPos) (f : t.VPos → M) : ∏ v ∈ liftSubtreeNonrootBranches r, f v = ∏ u ∈ nonrootBranches (t.subtreeAt ↑r), f (PlaneTree.subtreeVertex r u)

Reindex a product over lifted strict-descendant branches.

theorem Anderson4D.prod_liftContractFinset {t : PlaneTree} {p : PlaneTree.Pos} {M : Type u_1} [CommMonoid M] (hp : t.IsPos p) (W : Finset (t.contractAt p).VPos) (f : t.VPos → M) : ∏ v ∈ liftContractFinset hp W, f v = ∏ u ∈ W, f (PlaneTree.contractVertex hp u)

Reindex a product over any lifted contracted vertex set.

theorem Anderson4D.nonrootBranches_sdiff_liftWPrime {t : PlaneTree} (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) {W : Finset (t.contractAt ↑r).VPos} (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : nonrootBranches t \ liftWPrime r s W = (if s = 1 then liftSubtreeNonrootBranches r else insert r (liftSubtreeNonrootBranches r)) ∪ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r) \ W)

Exact complement partition underlying W ↦ W'. If s = 1, the selected branch is removed from the complement; otherwise it remains.

Exact product ledgers

theorem Anderson4D.prod_nonrootBranches_eq_collapse_partition {t : PlaneTree} {M : Type u_1} [CommMonoid M] (r : t.VPos) (hr : r ∈ nonrootBranches t) (f : t.VPos → M) : ∏ v ∈ nonrootBranches t, f v = (f r * ∏ v ∈ liftSubtreeNonrootBranches r, f v) * ∏ v ∈ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r)), f v

Product form of the branch trichotomy.

theorem Anderson4D.prod_nonrootBranches_sdiff_liftWPrime {t : PlaneTree} {M : Type u_1} [CommMonoid M] (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) {W : Finset (t.contractAt ↑r).VPos} (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) (f : t.VPos → M) : ∏ v ∈ nonrootBranches t \ liftWPrime r s W, f v = (if s = 1 then ∏ v ∈ liftSubtreeNonrootBranches r, f v else f r * ∏ v ∈ liftSubtreeNonrootBranches r, f v) * ∏ u ∈ nonrootBranches (t.contractAt ↑r) \ W, f (PlaneTree.contractVertex ⋯ u)

Product form of the complement partition, already reindexed back to the contracted tree on the final factor.

theorem Anderson4D.prod_parentScaleRatio_restrictMarking_cube {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) : ∏ u ∈ nonrootBranches (t.subtreeAt ↑r), parentScaleRatio (restrictMarking Nm r) u ^ 3 = ∏ v ∈ liftSubtreeNonrootBranches r, parentScaleRatio Nm v ^ 3

Restriction transports the entire cube product to the strict-descendant piece of the original tree.

theorem Anderson4D.prod_parentScaleRatio_contractMarking_sq {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) : ∏ u ∈ nonrootBranches (t.contractAt ↑r), parentScaleRatio (contractMarking Nm r) u ^ 2 = ∏ v ∈ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r)), parentScaleRatio Nm v ^ 2

Contraction transports the square product to the retained branch piece of the original tree.

theorem Anderson4D.prod_parentScaleRatio_contractMarking_sdiff {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (W : Finset (t.contractAt ↑r).VPos) : ∏ u ∈ nonrootBranches (t.contractAt ↑r) \ W, parentScaleRatio (contractMarking Nm r) u = ∏ v ∈ liftContractFinset ⋯ (nonrootBranches (t.contractAt ↑r) \ W), parentScaleRatio Nm v

The contracted complement factor reindexes to the lifted complement.

theorem Anderson4D.prod_cube_eq_prod_sq_mul_prod {α : Type u_1} (S : Finset α) (f : α → ℝ) : ∏ x ∈ S, f x ^ 3 = (∏ x ∈ S, f x ^ 2) * ∏ x ∈ S, f x

A cube product is the square product times one complement copy.

theorem Anderson4D.min_two_mul_eq_root_ratio_exponent {s : ℕ} (hs : 0 < s) : min (2 * s) 3 = if s = 1 then 2 else 3

For positive s, the root exponent is two in the one-cut case and three in every multi-cut case.

noncomputable def Anderson4D.restrictionParentRatioFactor {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (s : ℕ) : ℝ

Restriction contribution in (5.45): the selected-root gain and all strict-descendant cubes.

Equations

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

noncomputable def Anderson4D.contractionParentRatioFactor {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (W : Finset (t.contractAt ↑r).VPos) : ℝ

Contraction/IH contribution in (5.45): retained squares and the complement of W.

Equations

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

noncomputable def Anderson4D.originalParentRatioFactor {t : PlaneTree} (Nm : t.HeppMarking) (W : Finset t.VPos) : ℝ

The target ratio ledger in the original-tree P-5.9 summand.

Equations

• Anderson4D.originalParentRatioFactor Nm W = (∏ v ∈ Anderson4D.nonrootBranches t, Anderson4D.parentScaleRatio Nm v ^ 2) * ∏ v ∈ Anderson4D.nonrootBranches t \ W, Anderson4D.parentScaleRatio Nm v

theorem Anderson4D.restriction_mul_contraction_parentRatioFactor {t : PlaneTree} (Nm : t.HeppMarking) (r : t.VPos) (hr : r ∈ nonrootBranches t) (s : ℕ) (hs : 0 < s) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : restrictionParentRatioFactor Nm r s * contractionParentRatioFactor Nm r W = originalParentRatioFactor Nm (liftWPrime r s W)

Paper (5.45)--(5.46), exact parent-ratio ledger.

When s = 1, r ∈ W', so its root exponent is two. When s ≥ 2, r ∉ W', so the exponent is three. All strict descendants contribute a cube, while retained contracted branches contribute the IH square and its W-complement copy.