Extremal endpoint assembly for the primitive lattice estimate

When the non-root branch count is n - 2, validity and total multiplicity force exactly n leaves, each of multiplicity two. A primitive compatible word then has distinct first and last leaves. This makes the endpoint constraint in primitiveEndpointMarkingRatioSum available and closes the extremal logarithmic marking sum, including the finite sum over endpoint leaf pairs.

theorem Anderson4D.endpointLcaV_mem_branchNodes_of_ne {t : PlaneTree} (l l' : HeppLeaf t) : l ≠ l' → lcaV ↑l ↑l' ∈ t.BranchNodes

theorem Anderson4D.endpointExtremal_leafCount_eq {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (n : ℕ) (htotal : totalMultiplicity mu = 2 * n) (hbranchCard : (nonrootBranches t).card = n - 2) : t.leafCount = n

theorem Anderson4D.endpointExtremal_leafMultiplicity_eq_two {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (n : ℕ) (htotal : totalMultiplicity mu = 2 * n) (hbranchCard : (nonrootBranches t).card = n - 2) (l : HeppLeaf t) : leafMultiplicity mu l = 2

theorem Anderson4D.noProperLeafBlock_endpoint_ne {α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (hn : 2 ≤ n) (w : Fin (2 * n) → α) (hfiber : ∀ (a : α), {j : Fin (2 * n) | w j = a}.card = 2) (hprimitive : NoProperLeafBlock w) : w (primitiveEndpointLeft n ⋯) ≠ w (primitiveEndpointRight n ⋯)

theorem Anderson4D.activeExtremalEndpointLeaves {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (hbranchCard : (nonrootBranches t).card = n - 2) (d : PrimitiveActiveEndpointData t M n hn Y A x₀ x₁) : ∃ (f₀ : HeppLeaf t) (f₁ : HeppLeaf t) (z : HeppLeaf t → Z4), IsAdmissible (pairedMarking ↑d) M z ∧ z f₀ = x₀ ∧ z f₁ = x₁ ∧ f₀ ≠ f₁

theorem Anderson4D.activeExtremalLogMarking_eq {t : PlaneTree} (ht : t.isValid = true) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (d : PrimitiveActiveEndpointData t M n hn Y A x₀ x₁) : (↑(primitiveActiveEndpointBranchData ht d)).toHeppMarking ⋯ = pairedMarking ↑d

noncomputable def Anderson4D.activeExtremalEndpointChoice {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (hbranchCard : (nonrootBranches t).card = n - 2) (d : PrimitiveActiveEndpointData t M n hn Y A x₀ x₁) : (f₀ : HeppLeaf t) × (f₁ : HeppLeaf t) × { z : HeppLeaf t → Z4 // IsAdmissible (pairedMarking ↑d) M z ∧ z f₀ = x₀ ∧ z f₁ = x₁ ∧ f₀ ≠ f₁ }

Equations

• Anderson4D.activeExtremalEndpointChoice ht hroot hbranchCard d = ⟨Classical.choose ⋯, ⟨Classical.choose ⋯, ⟨Classical.choose ⋯, ⋯⟩⟩⟩

@[reducible, inline]

abbrev Anderson4D.ActiveExtremalEndpointCodeTarget (t : PlaneTree) (M : ℕ) (x₀ x₁ : Z4) : Type

Equations

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

noncomputable def Anderson4D.activeExtremalEndpointCode {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (hbranchCard : (nonrootBranches t).card = n - 2) (d : PrimitiveActiveEndpointData t M n hn Y A x₀ x₁) : ActiveExtremalEndpointCodeTarget t M x₀ x₁

Equations

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

theorem Anderson4D.activeExtremalEndpointCode_injective {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (hbranchCard : (nonrootBranches t).card = n - 2) : Function.Injective (activeExtremalEndpointCode ht hroot hbranchCard)

theorem Anderson4D.sum_activeExtremal_le_endpointMarkingSums {C : ℝ} (hC : 0 ≤ C) {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) {M n : ℕ} {hn : 1 ≤ n} {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} (hbranchCard : (nonrootBranches t).card = n - 2) : ∑ d : PrimitiveActiveEndpointData t M n hn Y A x₀ x₁, primitiveRatioRHS C n t (pairedMarking ↑d) ≤ ∑ p : { p : HeppLeaf t × HeppLeaf t // p.1 ≠ p.2 }, primitiveEndpointMarkingRatioSum C n M t (↑p).1 (↑p).2 x₀ x₁

theorem Anderson4D.sum_endpointMarkingSums_le_final {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (hbranchCard : (nonrootBranches t).card = n - 2) (x₀ x₁ : Z4) : ∑ p : { p : HeppLeaf t × HeppLeaf t // p.1 ≠ p.2 }, primitiveEndpointMarkingRatioSum C n M t (↑p).1 (↑p).2 x₀ x₁ ≤ ↑(n * n) * ((256 * C * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2))

theorem Anderson4D.sum_activeExtremal_le_final {C : ℝ} (hC : 0 ≤ C) {n M K : ℕ} {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (hn : 2 ≤ n) (htotal : totalMultiplicity mu = 2 * n) (hnL : n ≤ K * (Nat.log 2 (4 * M) + 1)) (hbranchCard : (nonrootBranches t).card = n - 2) {Y : Finset (Fin (2 * n) → Z4)} {A : Finset (Fin (2 * n))} {x₀ x₁ : Z4} : ∑ d : PrimitiveActiveEndpointData t M n ⋯ Y A x₀ x₁, primitiveRatioRHS C n t (pairedMarking ↑d) ≤ ↑(n * n) * ((256 * C * (↑K + 1)) ^ n * ↑(Nat.log 2 (4 * M) + 1) ^ (n - 2))