Finite restricted realization data

The denominator in paper (5.6) counts only the discrete pair consisting of branch scales and leaf multiplicities. It must not count an admissible embedding or a word witness, and it must not distinguish junk values away from branching vertices or leaves.

For a fixed tree t, box radius M, and total word length m, this file uses the finite carriers

• BranchExponentData t (4 * M) = BranchNodes t → Fin (4 * M + 1), and
• LeafMultiplicityData t m = Leaves t → Fin (m + 1).

Both have canonical zero extensions to all vertices. The predicates BranchExponentData.IsValid, LeafMultiplicityData.AtLeastTwo, and LeafMultiplicityData.HasTotal express the general denominator constraints, while realizationDataFinset enumerates the pairs satisfying all of them. Evenness belongs only to the paired-vector specialization and is recorded separately by RealizationData.IsEven and RealizationData.IsPairedValid.

Branch-only exponent data

@[reducible, inline]

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

Branch exponents bounded by bound, stored only where they have meaning.

Equations

• t.BranchExponentData bound = (↥t.BranchNodes → Fin (bound + 1))

def Anderson4D.PlaneTree.BranchExponentData.raw {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) : t.Marking

Canonical zero extension of bounded branch exponent data to all vertices.

Equations

• N.raw v = if h : v ∈ t.BranchNodes then ↑(N ⟨v, h⟩) else 0

@[simp]

theorem Anderson4D.PlaneTree.BranchExponentData.raw_apply_of_mem {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) {v : t.VPos} (hv : v ∈ t.BranchNodes) : N.raw v = ↑(N ⟨v, hv⟩)

@[simp]

theorem Anderson4D.PlaneTree.BranchExponentData.raw_apply_of_not_mem {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) {v : t.VPos} (hv : v ∉ t.BranchNodes) : N.raw v = 0

theorem Anderson4D.PlaneTree.BranchExponentData.raw_le {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) (v : t.VPos) : N.raw v ≤ bound

theorem Anderson4D.PlaneTree.BranchExponentData.ext {t : PlaneTree} {bound : ℕ} {N N' : t.BranchExponentData bound} (h : ∀ (v : ↥t.BranchNodes), ↑(N v) = ↑(N' v)) : N = N'

Extensionality on the restricted branch carrier.

theorem Anderson4D.PlaneTree.BranchExponentData.raw_injective {t : PlaneTree} {bound : ℕ} : Function.Injective raw

The canonical raw view is injective; off-branch zeros carry no data.

theorem Anderson4D.PlaneTree.BranchExponentData.raw_eq_iff {t : PlaneTree} {bound : ℕ} {N N' : t.BranchExponentData bound} : N.raw = N'.raw ↔ N = N'

def Anderson4D.PlaneTree.BranchExponentData.IsValid {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) : Prop

The paper's marking constraints, expressed entirely through restricted data. At a non-root branch the parent value is read from the canonical raw extension, so invalid unary-parent configurations cannot be hidden in junk.

Equations

• N.IsValid = ((∀ (v : ↥t.BranchNodes), 1 ≤ ↑(N v)) ∧ ∀ (v : ↥t.BranchNodes), ↑v ≠ t.rootV → N.raw (Anderson4D.PlaneTree.parentV ↑v) > ↑(N v))

@[implicit_reducible]

instance Anderson4D.PlaneTree.BranchExponentData.instDecidableIsValid {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) : Decidable N.IsValid

Equations

• N.instDecidableIsValid = id inferInstance

def Anderson4D.PlaneTree.BranchExponentData.toHeppMarking {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) (hN : N.IsValid) : t.HeppMarking

Valid restricted branch data defines a canonical HeppMarking.

Equations

• N.toHeppMarking hN = { Nexp := N.raw, pos := ⋯, parent_gt := ⋯ }

theorem Anderson4D.PlaneTree.BranchExponentData.toHeppMarking_canonicalRaw {t : PlaneTree} {bound : ℕ} (N : t.BranchExponentData bound) (hN : N.IsValid) : (N.toHeppMarking hN).canonicalRaw = N.raw

Converting valid restricted data to a marking preserves its canonical raw view literally.

def Anderson4D.PlaneTree.BranchExponentData.ofHeppMarking {t : PlaneTree} {bound : ℕ} (Nm : t.HeppMarking) (hbound : ∀ v ∈ t.BranchNodes, Nm.Nexp v ≤ bound) : t.BranchExponentData bound

Restrict a HeppMarking whose branch exponents have an explicit natural upper bound.

Equations

• Anderson4D.PlaneTree.BranchExponentData.ofHeppMarking Nm hbound v = ⟨Nm.Nexp ↑v, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.BranchExponentData.ofHeppMarking_apply {t : PlaneTree} {bound : ℕ} (Nm : t.HeppMarking) (hbound : ∀ v ∈ t.BranchNodes, Nm.Nexp v ≤ bound) (v : ↥t.BranchNodes) : ↑(ofHeppMarking Nm hbound v) = Nm.Nexp ↑v

theorem Anderson4D.PlaneTree.BranchExponentData.isValid_ofHeppMarking {t : PlaneTree} {bound : ℕ} (Nm : t.HeppMarking) (hbound : ∀ v ∈ t.BranchNodes, Nm.Nexp v ≤ bound) (hparent : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → parentV v ∈ t.BranchNodes) : (ofHeppMarking Nm hbound).IsValid

On a tree whose non-root branch vertices have branching parents, a genuine HeppMarking restricts to valid finite branch data.

Leaf-only multiplicity data

@[reducible, inline]

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

Leaf multiplicities bounded by the total word length bound, stored only at leaves.

Equations

• t.LeafMultiplicityData bound = (↥t.Leaves → Fin (bound + 1))

def Anderson4D.PlaneTree.LeafMultiplicityData.raw {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) : t.VPos → ℕ

Canonical zero extension of bounded leaf multiplicities to all vertices.

Equations

• mu.raw v = if h : v ∈ t.Leaves then ↑(mu ⟨v, h⟩) else 0

@[simp]

theorem Anderson4D.PlaneTree.LeafMultiplicityData.raw_apply_of_mem {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) {v : t.VPos} (hv : v ∈ t.Leaves) : mu.raw v = ↑(mu ⟨v, hv⟩)

@[simp]

theorem Anderson4D.PlaneTree.LeafMultiplicityData.raw_apply_of_not_mem {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) {v : t.VPos} (hv : v ∉ t.Leaves) : mu.raw v = 0

theorem Anderson4D.PlaneTree.LeafMultiplicityData.raw_le {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) (v : t.VPos) : mu.raw v ≤ bound

theorem Anderson4D.PlaneTree.LeafMultiplicityData.ext {t : PlaneTree} {bound : ℕ} {mu mu' : t.LeafMultiplicityData bound} (h : ∀ (l : ↥t.Leaves), ↑(mu l) = ↑(mu' l)) : mu = mu'

Extensionality on the restricted leaf carrier.

theorem Anderson4D.PlaneTree.LeafMultiplicityData.raw_injective {t : PlaneTree} {bound : ℕ} : Function.Injective raw

The canonical raw multiplicity view is injective.

theorem Anderson4D.PlaneTree.LeafMultiplicityData.raw_eq_iff {t : PlaneTree} {bound : ℕ} {mu mu' : t.LeafMultiplicityData bound} : mu.raw = mu'.raw ↔ mu = mu'

def Anderson4D.PlaneTree.LeafMultiplicityData.AtLeastTwo {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) : Prop

Every leaf multiplicity is at least two.

Equations

• mu.AtLeastTwo = ∀ (l : ↥t.Leaves), 2 ≤ ↑(mu l)

def Anderson4D.PlaneTree.LeafMultiplicityData.IsEven {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) : Prop

Every leaf multiplicity is even (the paired-vector specialization used after the Gaussian expectation).

Equations

• mu.IsEven = ∀ (l : ↥t.Leaves), Even ↑(mu l)

def Anderson4D.PlaneTree.LeafMultiplicityData.HasTotal {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) (total : ℕ) : Prop

The sum of all leaf multiplicities is the prescribed total length.

Equations

• mu.HasTotal total = (∑ l : ↥t.Leaves, ↑(mu l) = total)

@[implicit_reducible]

instance Anderson4D.PlaneTree.LeafMultiplicityData.instDecidableAtLeastTwo {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) : Decidable mu.AtLeastTwo

Equations

• mu.instDecidableAtLeastTwo = id inferInstance

@[implicit_reducible]

instance Anderson4D.PlaneTree.LeafMultiplicityData.instDecidableIsEven {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) : Decidable mu.IsEven

Equations

• mu.instDecidableIsEven = id inferInstance

@[implicit_reducible]

instance Anderson4D.PlaneTree.LeafMultiplicityData.instDecidableHasTotal {t : PlaneTree} {bound total : ℕ} (mu : t.LeafMultiplicityData bound) : Decidable (mu.HasTotal total)

Equations

• mu.instDecidableHasTotal = id inferInstance

def Anderson4D.PlaneTree.LeafMultiplicityData.toMultiplicities {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) (htwo : mu.AtLeastTwo) : t.Multiplicities

Restricted multiplicity data satisfying the lower bound defines a canonical Multiplicities bundle.

Equations

• mu.toMultiplicities htwo = { m := mu.raw, two_le := ⋯ }

theorem Anderson4D.PlaneTree.LeafMultiplicityData.toMultiplicities_canonicalRaw {t : PlaneTree} {bound : ℕ} (mu : t.LeafMultiplicityData bound) (htwo : mu.AtLeastTwo) : (mu.toMultiplicities htwo).canonicalRaw = mu.raw

def Anderson4D.PlaneTree.LeafMultiplicityData.ofMultiplicities {t : PlaneTree} {bound : ℕ} (mu : t.Multiplicities) (hbound : ∀ v ∈ t.Leaves, mu.m v ≤ bound) : t.LeafMultiplicityData bound

Restrict a Multiplicities bundle with an explicit leafwise bound.

Equations

• Anderson4D.PlaneTree.LeafMultiplicityData.ofMultiplicities mu hbound l = ⟨mu.m ↑l, ⋯⟩

@[simp]

theorem Anderson4D.PlaneTree.LeafMultiplicityData.ofMultiplicities_apply {t : PlaneTree} {bound : ℕ} (mu : t.Multiplicities) (hbound : ∀ v ∈ t.Leaves, mu.m v ≤ bound) (l : ↥t.Leaves) : ↑(ofMultiplicities mu hbound l) = mu.m ↑l

theorem Anderson4D.PlaneTree.LeafMultiplicityData.atLeastTwo_ofMultiplicities {t : PlaneTree} {bound : ℕ} (mu : t.Multiplicities) (hbound : ∀ v ∈ t.Leaves, mu.m v ≤ bound) : (ofMultiplicities mu hbound).AtLeastTwo

theorem Anderson4D.PlaneTree.LeafMultiplicityData.value_le_of_hasTotal {t : PlaneTree} {bound total : ℕ} (mu : t.LeafMultiplicityData bound) (htotal : mu.HasTotal total) (l : ↥t.Leaves) : ↑(mu l) ≤ total

A summand is bounded by the total sum of all leaf multiplicities.

The finite denominator carrier

@[reducible, inline]

abbrev Anderson4D.PlaneTree.RealizationData (t : PlaneTree) (M m : ℕ) : Type

Discrete realization data for paper (5.6). There are no embedding or word witnesses in this type.

Equations

• t.RealizationData M m = (t.BranchExponentData (4 * M) × t.LeafMultiplicityData m)

def Anderson4D.PlaneTree.RealizationData.IsValid {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Prop

General validity for the denominator in (5.6): valid branch scales, leaf multiplicities at least two, and the prescribed total. Evenness is deliberately not part of this predicate.

Equations

• d.IsValid = (d.1.IsValid ∧ d.2.AtLeastTwo ∧ d.2.HasTotal m)

@[implicit_reducible]

instance Anderson4D.PlaneTree.RealizationData.instDecidableIsValid {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Decidable d.IsValid

Equations

• d.instDecidableIsValid = id inferInstance

def Anderson4D.PlaneTree.RealizationData.IsEven {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Prop

Extra leafwise parity condition for data supplied by a pairing.

Equations

• d.IsEven = d.2.IsEven

@[implicit_reducible]

instance Anderson4D.PlaneTree.RealizationData.instDecidableIsEven {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Decidable d.IsEven

Equations

• d.instDecidableIsEven = id inferInstance

def Anderson4D.PlaneTree.RealizationData.IsPairedValid {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Prop

Paired-vector validity is general denominator validity together with the separate parity property.

Equations

• d.IsPairedValid = (d.IsValid ∧ d.IsEven)

@[implicit_reducible]

instance Anderson4D.PlaneTree.RealizationData.instDecidableIsPairedValid {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) : Decidable d.IsPairedValid

Equations

• d.instDecidableIsPairedValid = id inferInstance

def Anderson4D.PlaneTree.RealizationData.toHeppMarking {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) (hd : d.IsValid) : t.HeppMarking

Convert valid denominator data to the marking bundle.

Equations

• d.toHeppMarking hd = d.1.toHeppMarking ⋯

def Anderson4D.PlaneTree.RealizationData.toMultiplicities {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) (hd : d.IsValid) : t.Multiplicities

Convert valid denominator data to the multiplicity bundle.

Equations

• d.toMultiplicities hd = d.2.toMultiplicities ⋯

theorem Anderson4D.PlaneTree.RealizationData.toMultiplicities_even {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) (hd : d.IsValid) (heven : d.IsEven) (l : ↥t.Leaves) : Even ((d.toMultiplicities hd).m ↑l)

theorem Anderson4D.PlaneTree.RealizationData.toMultiplicities_total {t : PlaneTree} {M m : ℕ} (d : t.RealizationData M m) (hd : d.IsValid) : ∑ l : ↥t.Leaves, (d.toMultiplicities hd).m ↑l = m

@[reducible, inline]

abbrev Anderson4D.PlaneTree.PairedValidRealizationData (t : PlaneTree) (M m : ℕ) : Type

Valid denominator data carrying the additional parity property supplied by a pairing. It is intentionally distinct from the general denominator subtype.

Equations

• t.PairedValidRealizationData M m = { d : t.RealizationData M m // d.IsPairedValid }

def Anderson4D.PlaneTree.realizationDataFinset (t : PlaneTree) (M m : ℕ) : Finset (t.RealizationData M m)

The finite enumeration of valid restricted realization data for fixed t, M, and total length m.

Equations

• t.realizationDataFinset M m = Finset.filter Anderson4D.PlaneTree.RealizationData.IsValid Finset.univ

@[simp]

theorem Anderson4D.PlaneTree.mem_realizationDataFinset {t : PlaneTree} {M m : ℕ} {d : t.RealizationData M m} : d ∈ t.realizationDataFinset M m ↔ d.IsValid

theorem Anderson4D.PlaneTree.card_realizationData_type (t : PlaneTree) (M m : ℕ) : Fintype.card (t.RealizationData M m) = (4 * M + 1) ^ t.BranchNodes.card * (m + 1) ^ t.Leaves.card

The explicit ambient cardinality of the restricted data carrier.

theorem Anderson4D.PlaneTree.card_realizationDataFinset_le (t : PlaneTree) (M m : ℕ) : (t.realizationDataFinset M m).card ≤ (4 * M + 1) ^ t.BranchNodes.card * (m + 1) ^ t.Leaves.card

Explicit finiteness bound for the actual denominator enumeration.

theorem Anderson4D.PlaneTree.finite_validRealizationData (t : PlaneTree) (M m : ℕ) : {d : t.RealizationData M m | d.IsValid}.Finite

The valid restricted data form a finite set, independently of any realization witnesses.

From the analytic scale bound to the finite natural bound

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

The analytic bound 2^Nexp ≤ 4M implies the deliberately coarse natural bound Nexp ≤ 4M used by the finite carrier.

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

Restrict a marking satisfying the paper's scale bound to the finite branch carrier used in RealizationData.

Equations

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

@[simp]

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

theorem Anderson4D.PlaneTree.branchDataOfScaleBound_isValid {t : PlaneTree} {M : ℕ} (Nm : t.HeppMarking) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (hparent : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → parentV v ∈ t.BranchNodes) : (branchDataOfScaleBound Nm hscale).IsValid

Bundle-to-carrier bridge without realization witnesses

theorem Anderson4D.PlaneTree.multiplicity_le_total {t : PlaneTree} {mu : t.Multiplicities} {m : ℕ} (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (l : ↥t.Leaves) : mu.m ↑l ≤ m

If the leaf multiplicities sum to m, each individual multiplicity is at most m.

def Anderson4D.PlaneTree.leafDataOfTotal {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : t.LeafMultiplicityData m

Restrict a multiplicity bundle using its prescribed total as the finite leafwise bound.

Equations

• Anderson4D.PlaneTree.leafDataOfTotal mu htotal = Anderson4D.PlaneTree.LeafMultiplicityData.ofMultiplicities mu ⋯

theorem Anderson4D.PlaneTree.leafDataOfTotal_atLeastTwo {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : (leafDataOfTotal mu htotal).AtLeastTwo

theorem Anderson4D.PlaneTree.leafDataOfTotal_isEven {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (heven : ∀ (l : ↥t.Leaves), Even (mu.m ↑l)) : (leafDataOfTotal mu htotal).IsEven

theorem Anderson4D.PlaneTree.leafDataOfTotal_hasTotal {t : PlaneTree} {m : ℕ} (mu : t.Multiplicities) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : (leafDataOfTotal mu htotal).HasTotal m

def Anderson4D.PlaneTree.realizationDataOfBundles {t : PlaneTree} {M m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : t.RealizationData M m

Form the finite denominator datum from the marking and multiplicity bundles. The construction contains no embedding and no word witness.

Equations

• Anderson4D.PlaneTree.realizationDataOfBundles Nm mu hscale htotal = (Anderson4D.PlaneTree.branchDataOfScaleBound Nm hscale, Anderson4D.PlaneTree.leafDataOfTotal mu htotal)

theorem Anderson4D.PlaneTree.realizationDataOfBundles_isValid {t : PlaneTree} {M m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hparent : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → parentV v ∈ t.BranchNodes) : (realizationDataOfBundles Nm mu hscale htotal).IsValid

theorem Anderson4D.PlaneTree.realizationDataOfBundles_isEven {t : PlaneTree} {M m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (heven : ∀ (l : ↥t.Leaves), Even (mu.m ↑l)) : (realizationDataOfBundles Nm mu hscale htotal).IsEven

Bundle data from a paired vector satisfies the separately recorded parity predicate.

theorem Anderson4D.PlaneTree.realizationDataOfBundles_isPairedValid {t : PlaneTree} {M m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (heven : ∀ (l : ↥t.Leaves), Even (mu.m ↑l)) (hparent : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → parentV v ∈ t.BranchNodes) : (realizationDataOfBundles Nm mu hscale htotal).IsPairedValid

Bundle data satisfying both the general and paired-vector conditions.

theorem Anderson4D.PlaneTree.realizationDataOfBundles_mem {t : PlaneTree} {M m : ℕ} (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (hparent : ∀ v ∈ t.BranchNodes, v ≠ t.rootV → parentV v ∈ t.BranchNodes) : realizationDataOfBundles Nm mu hscale htotal ∈ t.realizationDataFinset M m

theorem Anderson4D.PlaneTree.realizationDataOfBundles_isValid_of_treeValid {t : PlaneTree} {M m : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : (realizationDataOfBundles Nm mu hscale htotal).IsValid

On a valid Hepp tree the structural parent hypothesis is automatic.

theorem Anderson4D.PlaneTree.realizationDataOfBundles_isPairedValid_of_treeValid {t : PlaneTree} {M m : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) (heven : ∀ (l : ↥t.Leaves), Even (mu.m ↑l)) : (realizationDataOfBundles Nm mu hscale htotal).IsPairedValid

On a valid tree, paired-vector bundle data is paired-valid.

theorem Anderson4D.PlaneTree.realizationDataOfBundles_mem_of_treeValid {t : PlaneTree} {M m : ℕ} (ht : t.isValid = true) (Nm : t.HeppMarking) (mu : t.Multiplicities) (hscale : ∀ v ∈ t.BranchNodes, ↑(scaleN Nm v) ≤ 4 * ↑M) (htotal : ∑ l : ↥t.Leaves, mu.m ↑l = m) : realizationDataOfBundles Nm mu hscale htotal ∈ t.realizationDataFinset M m