Factored right-hand sides for the Proposition 5.9 collapse

The frozen statements intentionally display all paper factors. This module rewrites them into the named leaf, branch-power, and parent-ratio ledgers used by the collapse audit.

The P-5.9 summand

noncomputable def Anderson4D.inductiveRHSSummand (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound W : Finset t.VPos) : ℝ

One W-summand of the factored right side of Proposition 5.9, without the global C0^m D^|B| coefficient.

Equations

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

theorem Anderson4D.inductiveRHS_eq_factored (C0 D : ℝ) (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : inductiveRHS C0 D m t Nm mu compound = C0 ^ m * D ^ t.BranchNodes.card * ∑ W ∈ (nonrootBranches t).powerset, inductiveRHSSummand m t Nm mu compound W

The frozen P-5.9 right side is the sum of the named factored summands.

noncomputable def Anderson4D.contractedInductiveTerm (C0 D : ℝ) (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound W : Finset t.VPos) : ℝ

One full contracted-tree induction term, including its global powers.

Equations

• Anderson4D.contractedInductiveTerm C0 D m t Nm mu compound W = C0 ^ m * D ^ t.BranchNodes.card * Anderson4D.inductiveRHSSummand m t Nm mu compound W

theorem Anderson4D.inductiveRHS_eq_sum_contractedInductiveTerm (C0 D : ℝ) (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : inductiveRHS C0 D m t Nm mu compound = ∑ W ∈ (nonrootBranches t).powerset, contractedInductiveTerm C0 D m t Nm mu compound W

Distribute the global P-5.9 coefficient into the finite W-sum.

The restricted P-5.10 right side

noncomputable def Anderson4D.restrictedSingleScaleTerm (C0 : ℝ) (m s : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : ℝ

P-5.10 on the selected subtree, written with the named leaf and branch factors and with its root-ratio contribution joined to the subtree cube product.

Equations

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

theorem Anderson4D.singleScaleRHS_restrict_eq (C0 : ℝ) (m s : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) : singleScaleRHS C0 m s (scaleN Nm (PlaneTree.parentV r)) (t.subtreeAt ↑r) (restrictMarking Nm r) (restrictMultiplicities mu r) (restrictCompound r compound) = restrictedSingleScaleTerm C0 m s Nm mu compound r

Exact specialized rewrite of the P-5.10 right side used in the collapse induction.

The contracted P-5.9 term

noncomputable def Anderson4D.contractedCollapseTerm (C0 D : ℝ) (m : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (W : Finset (t.contractAt ↑r).VPos) : ℝ

A contracted-tree induction term rewritten back to the original marking for its parent-ratio factor.

Equations

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

theorem Anderson4D.contractedInductiveTerm_eq_collapseTerm (C0 D : ℝ) (m : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (s : ℕ) (hs : 1 ≤ s) (W : Finset (t.contractAt ↑r).VPos) : contractedInductiveTerm C0 D m (t.contractAt ↑r) (contractMarking Nm r) (contractMultiplicities mu r s hs) (contractCompound r compound) W = contractedCollapseTerm C0 D m Nm mu compound r s hs W

Exact rewrite of one contracted induction summand.

Exact product audit

theorem Anderson4D.natScale_pow_cancel (R s : ℕ) (hR : 0 < R) : ↑R ^ (2 * s) * ↑R ^ (-2 * ↑s) = 1

The R^(2s) from P-5.10 cancels the R^(-2s) created by the contracted γ² ledger.

noncomputable def Anderson4D.combinedCollapseTerm (C0 D : ℝ) (n s m : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hs : 1 ≤ s) (W : Finset (t.contractAt ↑r).VPos) : ℝ

The product appearing after the geometric pointwise estimate and the two analytic calls, before the remaining scalar inequalities.

Equations

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

noncomputable def Anderson4D.combinedCollapseFactored (C0 D : ℝ) (n s m : ℕ) {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (W : Finset (t.contractAt ↑r).VPos) : ℝ

The same product after all exact tree ledgers and scale cancellation.

Equations

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

theorem Anderson4D.combinedCollapseTerm_eq_factored (C0 D : ℝ) (n s m : ℕ) {t : PlaneTree} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (r : t.VPos) (hr : r ∈ nonrootBranches t) (hs : 1 ≤ s) (W : Finset (t.contractAt ↑r).VPos) (hW : W ⊆ nonrootBranches (t.contractAt ↑r)) : combinedCollapseTerm C0 D n s m Nm mu compound r hs W = combinedCollapseFactored C0 D n s m Nm mu compound r W

Exact paper (5.45)--(5.46) factor audit before inequalities.

This is where the leaf ledger, γ² ledger, parent-ratio ledger, and the dyadic-scale cancellation meet.