Eligible branches for the Proposition 5.9 collapse

This file formalizes the choice made in (5.40). Eligibility is written without division:

8 * N'_v ≤ N_{v⁺}.

If eligible branches exist, a branch of maximal address length is a valid "lowest" choice. The choice need not be unique, and none of the later arguments should depend on a tie-breaking convention.

def Anderson4D.CollapseEligible {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : Prop

Division-free form of the collapse condition (5.40).

Equations

• Anderson4D.CollapseEligible Nm mu v = (v ∈ Anderson4D.nonrootBranches t ∧ 8 * Anderson4D.accumulatedScale Nm mu v ≤ Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV v))

@[implicit_reducible]

instance Anderson4D.instDecidableCollapseEligible {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : Decidable (CollapseEligible Nm mu v)

Equations

• Anderson4D.instDecidableCollapseEligible Nm mu v = id inferInstance

def Anderson4D.eligibleBranches {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Finset t.VPos

The finite set of branches satisfying (5.40).

Equations

• Anderson4D.eligibleBranches Nm mu = {v ∈ Anderson4D.nonrootBranches t | 8 * Anderson4D.accumulatedScale Nm mu v ≤ Anderson4D.scaleN Nm (Anderson4D.PlaneTree.parentV v)}

@[simp]

theorem Anderson4D.mem_eligibleBranches_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : v ∈ eligibleBranches Nm mu ↔ CollapseEligible Nm mu v

def Anderson4D.IsLowestCollapseEligible {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (v : t.VPos) : Prop

A lowest eligible branch has no strictly lower eligible branch.

Equations

• Anderson4D.IsLowestCollapseEligible Nm mu v = (Anderson4D.CollapseEligible Nm mu v ∧ ∀ u ∈ Anderson4D.branchNodesUnder v, u ≠ v → ¬Anderson4D.CollapseEligible Nm mu u)

theorem Anderson4D.exists_lowestCollapseEligible {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hne : (eligibleBranches Nm mu).Nonempty) : ∃ (v : t.VPos), IsLowestCollapseEligible Nm mu v

Any nonempty eligible set has a lowest member. Maximizing address length is enough because strict descendants have strictly longer addresses.

theorem Anderson4D.eligible_accumulated_le_parent {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} {v : t.VPos} (hv : CollapseEligible Nm mu v) : accumulatedScale Nm mu v ≤ scaleN Nm (PlaneTree.parentV v)

An eligible branch's accumulated scale is bounded by its parent scale; the stronger factor-eight inequality is retained in CollapseEligible.

theorem Anderson4D.noEligible_implies_singleScale {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hempty : eligibleBranches Nm mu = ∅) : SatisfiesSingleScaleCondition Nm mu

If there is no eligible branch, the whole tree satisfies the single-scale condition (5.38). Equality is deliberately counted as eligible.

theorem Anderson4D.scaleN_isDyadicNat {t : PlaneTree} (Nm : t.HeppMarking) (v : t.VPos) : IsDyadicNat (scaleN Nm v)

Every scale carried by a marking is dyadic, including totalized junk values away from branch nodes.