Reindexing the increasing Hepp markings in (5.17)

For a fixed valid tree, an increasing branch marking is encoded by

• its root exponent;
• at a branch in the chosen free set, its own exponent;
• at every other non-root branch, the positive exponent gap to its parent.

The encoding is injective: starting at the root, the exponent at each branch is recovered either directly (free case) or by subtracting the recorded gap from the already recovered parent exponent. Moreover, on a non-free branch the parent-scale ratio is exactly 2⁻gap. Thus the constrained marking sum injects into the independent product domain used by sum_dyadicAssignmentWeight_le.

@[reducible, inline]

abbrev Anderson4D.ValidBranchExponentData (t : PlaneTree) (bound : ℕ) : Type

Valid bounded branch data, with no multiplicity or realization witness.

Equations

• Anderson4D.ValidBranchExponentData t bound = { N : t.BranchExponentData bound // N.IsValid }

@[reducible, inline]

abbrev Anderson4D.PrimitiveMarkingCode (t : PlaneTree) (bound : ℕ) : Type

Independent coordinates used to dominate an increasing marking: one root coordinate and one coordinate for every non-root branch.

Equations

• Anderson4D.PrimitiveMarkingCode t bound = (Fin (bound + 1) × (Anderson4D.NonrootBranch t → Fin (bound + 1)))

def Anderson4D.primitiveMarkingCode {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) : PrimitiveMarkingCode t bound

The root/free/gap code of a valid bounded marking. The gap coordinate is stored in the same Fin (bound+1) box because it is at most the parent exponent, hence at most bound.

Equations

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

@[simp]

theorem Anderson4D.primitiveMarkingCode_fst {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) : (primitiveMarkingCode hroot free N).1 = ↑N ⟨t.rootV, hroot⟩

@[simp]

theorem Anderson4D.primitiveMarkingCode_snd_of_mem {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) (v : NonrootBranch t) (hv : v ∈ free) : (primitiveMarkingCode hroot free N).2 v = ↑N ⟨↑v, ⋯⟩

@[simp]

theorem Anderson4D.primitiveMarkingCode_snd_of_not_mem {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) (v : NonrootBranch t) (hv : v ∉ free) : ↑((primitiveMarkingCode hroot free N).2 v) = (↑N).raw (PlaneTree.parentV ↑v) - ↑(↑N ⟨↑v, ⋯⟩)

theorem Anderson4D.primitiveMarkingCode_injective {t : PlaneTree} {bound : ℕ} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) : Function.Injective (primitiveMarkingCode hroot free)

The root/free/gap encoding is injective on valid increasing markings.

theorem Anderson4D.parentScaleRatio_eq_half_pow_markingCode {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) (v : NonrootBranch t) (hv : v ∉ free) : parentScaleRatio ((↑N).toHeppMarking ⋯) ↑v = (1 / 2) ^ ↑((primitiveMarkingCode hroot free N).2 v)

On a non-free branch, the recorded coordinate is the exact exponent gap, so its geometric weight is the exact parent-scale ratio.

noncomputable def Anderson4D.primitiveMarkingRatioWeight {t : PlaneTree} {bound : ℕ} (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) : ℝ

The ratio factor in (5.16), indexed on the genuine non-root branch carrier. Branches in free have no ratio factor.

Equations

• Anderson4D.primitiveMarkingRatioWeight free N = ∏ v : Anderson4D.NonrootBranch t, if v ∈ free then 1 else Anderson4D.parentScaleRatio ((↑N).toHeppMarking ⋯) ↑v

theorem Anderson4D.primitiveMarkingRatioWeight_nonneg {t : PlaneTree} {bound : ℕ} (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) : 0 ≤ primitiveMarkingRatioWeight free N

theorem Anderson4D.primitiveMarkingRatioWeight_eq_codeWeight {t : PlaneTree} {bound : ℕ} (hroot : t.rootV ∈ t.BranchNodes) (free : Finset (NonrootBranch t)) (N : ValidBranchExponentData t bound) : primitiveMarkingRatioWeight free N = dyadicAssignmentWeight (bound + 1) free (primitiveMarkingCode hroot free N).2

Pointwise identification of the actual marking-ratio product with the independent dyadic assignment weight of its code.

Bridge to the paper's ordinary vertex-subset indexing

def Anderson4D.nonrootBranchFinsetOfSubset {t : PlaneTree} (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : Finset (NonrootBranch t)

Regard a vertex finset known to lie in nonrootBranches as a finset of the genuine non-root branch subtype.

Equations

• Anderson4D.nonrootBranchFinsetOfSubset W hW = Finset.map { toFun := fun (v : ↥W) => ⟨↑v, ⋯⟩, inj' := ⋯ } W.attach

@[simp]

theorem Anderson4D.mem_nonrootBranchFinsetOfSubset {t : PlaneTree} {W : Finset t.VPos} (hW : W ⊆ nonrootBranches t) (v : NonrootBranch t) : v ∈ nonrootBranchFinsetOfSubset W hW ↔ ↑v ∈ W

@[simp]

theorem Anderson4D.card_nonrootBranchFinsetOfSubset {t : PlaneTree} (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : (nonrootBranchFinsetOfSubset W hW).card = W.card

theorem Anderson4D.primitiveMarkingRatioWeight_ofSubset {t : PlaneTree} {bound : ℕ} (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) (N : ValidBranchExponentData t bound) : primitiveMarkingRatioWeight (nonrootBranchFinsetOfSubset W hW) N = ∏ v ∈ nonrootBranches t \ W, parentScaleRatio ((↑N).toHeppMarking ⋯) v

The subtype-indexed ratio weight is literally the product over the paper's complement (B \\ {root}) \\ W.

theorem Anderson4D.sum_validBranchExponentData_ratioWeight_le {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (bound : ℕ) (free : Finset (NonrootBranch t)) : ∑ N : ValidBranchExponentData t bound, primitiveMarkingRatioWeight free N ≤ ↑(bound + 1) ^ (free.card + 1) * 2 ^ ((nonrootBranches t).card - free.card)

Increasing-marking reindexing for paper (5.17).

The sum is over the actual valid bounded branch markings. The root exponent costs one unrestricted coordinate, every branch in free costs one more, and every remaining branch is summed by a geometric series. The proof uses the injective root/free/gap code above; no independence of the original marking coordinates is assumed.

The logarithmic scale window used in the primitive estimate

theorem Anderson4D.nexp_le_log_four_mul_of_scaleN_le {t : PlaneTree} {Nm : t.HeppMarking} {M : ℕ} {v : t.VPos} (hscale : ↑(scaleN Nm v) ≤ 4 * ↑M) : Nm.Nexp v ≤ Nat.log 2 (4 * M)

The analytic scale cap 2^Nexp ≤ 4M places the exponent in the exact base-two logarithmic window. This is the sharp replacement for the coarse Nexp ≤ 4M bound used only to make the incidence denominator finite.

def Anderson4D.logBranchDataOfScaleBound {t : PlaneTree} {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) : t.BranchExponentData (Nat.log 2 (4 * M))

Canonical restriction of an analytically scale-capped marking to the logarithmic exponent carrier needed in (5.17).

Equations

• Anderson4D.logBranchDataOfScaleBound Nm hscale = Anderson4D.PlaneTree.BranchExponentData.ofHeppMarking Nm ⋯

@[simp]

theorem Anderson4D.logBranchDataOfScaleBound_apply {t : PlaneTree} {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (v : ↥t.BranchNodes) : ↑(logBranchDataOfScaleBound Nm hscale v) = Nm.Nexp ↑v

theorem Anderson4D.logBranchDataOfScaleBound_isValid {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) : (logBranchDataOfScaleBound Nm hscale).IsValid

theorem Anderson4D.parentScaleRatio_logBranchDataOfScaleBound {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (v : NonrootBranch t) : parentScaleRatio ((logBranchDataOfScaleBound Nm hscale).toHeppMarking ⋯) ↑v = parentScaleRatio Nm ↑v

The logarithmic restriction preserves every parent-scale ratio on the actual non-root branch carrier.

theorem Anderson4D.primitiveMarkingRatioWeight_logBranchDataOfScaleBound {t : PlaneTree} (ht : t.isValid = true) {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (free : Finset (NonrootBranch t)) : primitiveMarkingRatioWeight free ⟨logBranchDataOfScaleBound Nm hscale, ⋯⟩ = ∏ v : NonrootBranch t, if v ∈ free then 1 else parentScaleRatio Nm ↑v

Applying the logarithmic restriction changes neither the free branches nor the ratio weight appearing in (5.16).

theorem Anderson4D.sum_logBranchExponentData_ratioWeight_le {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (M : ℕ) (free : Finset (NonrootBranch t)) : ∑ N : ValidBranchExponentData t (Nat.log 2 (4 * M)), primitiveMarkingRatioWeight free N ≤ ↑(Nat.log 2 (4 * M) + 1) ^ (free.card + 1) * 2 ^ ((nonrootBranches t).card - free.card)

Paper-facing logarithmic form of the increasing-marking sum (5.17). All scale-capped realizing markings canonically lie in this finite domain by logBranchDataOfScaleBound.

theorem Anderson4D.sum_logBranchExponentData_parentScaleRatio_le {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (M : ℕ) (W : Finset t.VPos) (hW : W ⊆ nonrootBranches t) : ∑ N : ValidBranchExponentData t (Nat.log 2 (4 * M)), ∏ v ∈ nonrootBranches t \ W, parentScaleRatio ((↑N).toHeppMarking ⋯) v ≤ ↑(Nat.log 2 (4 * M) + 1) ^ (W.card + 1) * 2 ^ ((nonrootBranches t).card - W.card)

Direct ordinary-finset form of (5.17), matching the W indexing in permSumRHS. This is the form consumed by the primitive lattice assembly.