Proposition 5.7 on a fixed one-open-edge word fibre #
The dummy-closed pairing supplies a genuine primitive augmented word.
The exact multiplicity package from OpenEdgeMultiplicity supplies the
evenness, total order, and valid-word hypotheses of Proposition 5.7.
This file performs that application without summing over an arbitrary
marker family.
theorem
Anderson4D.primitiveChainWeight_le_paperSum_of_mem
{t : PlaneTree}
{q : ℕ}
(mu : t.Multiplicities)
(z : HeppLeaf t → Fin 4 → ℤ)
(w : Fin q → HeppLeaf t)
(hw : w ∈ validWords (leafMultiplicity mu))
:
One nonnegative primitive word summand is bounded by the complete paper factorial ledger over its valid-word fibre.
theorem
Anderson4D.openEdgeAugmented_chain_le_permSumRHS
{C : ℝ}
(hperm : PermSumEstimate C)
{t : PlaneTree}
{m M : ℕ}
(mu : t.Multiplicities)
(w : Fin m → HeppLeaf t)
(hw : w ∈ validWords (leafMultiplicity mu))
(κ : PartialPairing (Fin m))
(a b : Fin m)
(hm : 0 < m)
(hκab : κ a = b)
(hab : a < b)
(hfull : κ.IsFull)
(hprimitive : IsPrimitive κ)
(hrespect : ∀ (i : Fin m), i ≠ a → i ≠ b → w i = w (κ i))
(Nm : t.HeppMarking)
(z : HeppLeaf t → Fin 4 → ℤ)
(ht : t.isValid = true)
(hroot : t.rootV ∈ t.BranchNodes)
(hadm : IsAdmissible Nm M z)
:
∃ (n : ℕ),
2 ≤ n ∧ heppChainWeight z (openEdgeAugmentedWord w a b) ≤ permSumRHS C n t Nm (openEdgeAugmentedMultiplicities mu w hw a b)
A fixed genuine open edge, after dummy closure, is controlled by the literal Proposition 5.7 right-hand side for its packaged augmented multiplicity profile.