No-collapse base case for Proposition 5.9

When (5.40) has no eligible branch, the whole tree satisfies (5.38). Proposition 5.10 is then applied with no skipped edge. This file records the pointwise and sum-level bridges for that reduction, together with a dyadic scale which always dominates a prescribed natural scale.

theorem Anderson4D.noAdjacentOutside_empty_of_noAdjacentEqual {α : Type u_1} [DecidableEq α] {m : ℕ} {w : Fin m → α} (hw : NoAdjacentEqual w) : NoAdjacentOutside ∅ w

With no skipped indices, NoAdjacentEqual implies the single-scale adjacency predicate.

@[simp]

theorem Anderson4D.heppChainWeightExcept_empty {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeightExcept z ∅ w = heppChainWeight z w

Omitting no edges leaves the chain product unchanged.

theorem Anderson4D.primitiveSeparatedChainWeight_le_singleScale_empty {t : PlaneTree} {m : ℕ} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : primitiveSeparatedChainWeight z w ≤ singleScaleChainWeight z ∅ w

Pointwise bridge from the P-5.9 summand to P-5.10 with O = ∅.

theorem Anderson4D.paperSum_primitiveSeparated_le_singleScale_empty {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) ≤ paperSum (leafMultiplicity mu) (singleScaleChainWeight z ∅)

The pointwise base bridge summed in the exact paperSum normalization.

theorem Anderson4D.exists_dyadicNat_ge (q : ℕ) : ∃ (R : ℕ), IsDyadicNat R ∧ q ≤ R

Every natural scale is dominated by a natural dyadic scale.

theorem Anderson4D.singleScaleRHS_zero_skips (C0 : ℝ) (m R : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : singleScaleRHS C0 m 0 R t Nm mu compound = (((C0 ^ (↑m / 2) * sqrtFactorial m * ∏ l ∈ simpleLeaves t compound, sqrtFactorial (mu.m l)) * ∏ l ∈ compoundLeaves t compound, factorialThreeQuarters (mu.m l)) * ∏ v ∈ t.BranchNodes, ↑(scaleN Nm v) ^ (-2 * (↑(gamma2 mu compound v) - 1))) * ∏ v ∈ nonrootBranches t, parentScaleRatio Nm v ^ 3

At zero skipped edges, the P-5.10 right side is independent of the auxiliary dyadic scale R.

theorem Anderson4D.singleScaleRHS_zero_le_inductiveRHS (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (m R : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) : singleScaleRHS C0 m 0 R t Nm mu compound ≤ inductiveRHS C0 D m t Nm mu compound

The zero-skipped single-scale right side is bounded by the P-5.9 right side. It is exactly the W = ∅ summand, apart from the smaller C0^(m/2) coefficient and the absent D factor.

theorem Anderson4D.noEligible_case_of_singleScale {C0 D : ℝ} (hsingle : SingleScaleEstimate C0) (hD : D = Real.exp (C0 ^ 10)) (m : ℕ) (t : PlaneTree) (Nm : t.HeppMarking) (mu : t.Multiplicities) (compound : Finset t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (hcompound : compound ⊆ t.Leaves) (htotal : totalMultiplicity mu = m) (hsep : IsSeparatedEmbedding Nm z) (hempty : eligibleBranches Nm mu = ∅) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) ≤ inductiveRHS C0 D m t Nm mu compound

Complete no-eligible-branch case of Proposition 5.9, parameterized by Proposition 5.10 with the same constant C0.