Power-counting reduction for the single-scale estimate

This file closes the product-to-exponential part of paper (5.69). Under the single-scale condition, every inverse parent-scale ratio is bounded by 8 times an exponential of its normalized accumulated scale. Reordering those exponents and applying (5.68) gives one uniform exponential loss in the total multiplicity.

The paper writes the final loss as an unspecified C^m; here the explicit choice is (8 * exp 4)^m. The factor 4 includes the inclusive-ancestor constant recorded in docs/PAPER_NOTES.md under (5.69).

noncomputable def Anderson4D.inverseParentScaleRatio {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : ℝ

The reciprocal of parentScaleRatio, namely N_{v⁺}/N_v.

Equations

• Anderson4D.inverseParentScaleRatio Nm v = ↑(Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV v)) / ↑(Anderson4D.scaleN Nm v)

theorem Anderson4D.inverseParentScaleRatio_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : 0 ≤ inverseParentScaleRatio Nm v

theorem Anderson4D.inverseParentScaleRatio_mul_parentScaleRatio {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : inverseParentScaleRatio Nm v * parentScaleRatio Nm v = 1

The auxiliary inverse ratio cancels the ratio appearing in the frozen right-hand sides.

theorem Anderson4D.inverseParentScaleRatio_le_eight_mul_exp {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : SatisfiesSingleScaleCondition Nm mu) {v : t.VPos} (hv : v ∈ nonrootBranches t) : inverseParentScaleRatio Nm v ≤ 8 * Real.exp (↑(accumulatedScale Nm mu v) / ↑(scaleN Nm v))

One factor in (5.69), before multiplying over non-root branch nodes.

theorem Anderson4D.prod_inverseParentScaleRatio_le_exp_cost {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : SatisfiesSingleScaleCondition Nm mu) : ∏ v ∈ nonrootBranches t, inverseParentScaleRatio Nm v ≤ 8 ^ (nonrootBranches t).card * Real.exp (singleScaleExponentCost Nm mu)

Finite-product form of (5.69), before bounding the number of branch nodes and the reordered exponent.

theorem Anderson4D.card_nonrootBranches_le_totalMultiplicity {t : PlaneTree} (ht : t.isValid = true) (mu : t.Multiplicities) : (nonrootBranches t).card ≤ totalMultiplicity mu

A valid tree has no more non-root branch nodes than word positions.

theorem Anderson4D.prod_inverseParentScaleRatio_le_uniform_power {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : SatisfiesSingleScaleCondition Nm mu) : ∏ v ∈ nonrootBranches t, inverseParentScaleRatio Nm v ≤ (8 * Real.exp 4) ^ totalMultiplicity mu

Explicit C^m form of paper (5.69), with C = 8 exp(4).