Documentation

Anderson4D.PermSum.MergeConstants

Final constant absorption for Proposition 5.7 #

This file closes the scalar ledger after the run-compression and all-simple-leaf reductions. Leaf multiplicities pay for the number of branch vertices, while one explicit exponential base absorbs the compressed word length, the tree factor, and the uniform merge loss.

source
theorem Anderson4D.card_branchNodes_le_of_totalMultiplicity_eq_two_mul {t : PlaneTree} (ht : t.isValid = true) (_hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (n : ℕ) (htotal : totalMultiplicity mu = 2 * n) :
t.BranchNodes.card ≤ n

A valid tree with total leaf multiplicity 2n has at most n branch vertices. This is the tree-count input to the final constant absorption in Proposition 5.7.

source
def Anderson4D.mergeGlobalConstant (C0 D : ℝ) :
ℝ

One explicit final base. The factor 64 simultaneously covers either the 16^n merge-pattern ledger or the coarser 64^n version.

Equations
Instances For
    source
    theorem Anderson4D.one_le_mergeGlobalConstant (C0 D : ℝ) :
    1 ≤ mergeGlobalConstant C0 D

    The chosen final base is at least one.

    source
    theorem Anderson4D.mergeGlobalConstant_absorbs (C0 D K : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (hK0 : 0 ≤ K) (hK64 : K ≤ 64) (n m b : ℕ) (hm : m ≤ 2 * n) (hb : b ≤ n) :
    C0 ^ m * D ^ b * K ^ n ≤ mergeGlobalConstant C0 D ^ n

    Scalar constant absorption. The hypotheses m ≤ 2n and b ≤ n are respectively the compressed-word and branch-count ledgers. Any nonnegative loss base up to 64 is absorbed.

    source
    theorem Anderson4D.mergeGlobalConstant_absorbs_sixtyFour (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (n m b : ℕ) (hm : m ≤ 2 * n) (hb : b ≤ n) :
    C0 ^ m * D ^ b * 64 ^ n ≤ mergeGlobalConstant C0 D ^ n

    The coarser 64^n ledger is directly absorbed.

    source
    theorem Anderson4D.mergeGlobalConstant_absorbs_tree {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (C0 D K : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (hK0 : 0 ≤ K) (hK64 : K ≤ 64) (n m : ℕ) (htotal : totalMultiplicity mu = 2 * n) (hm : m ≤ 2 * n) :
    C0 ^ m * D ^ t.BranchNodes.card * K ^ n ≤ mergeGlobalConstant C0 D ^ n

    Tree-facing form of the final scalar ledger. The tree hypotheses and totalMultiplicity = 2n discharge the branch exponent automatically.

    source
    theorem Anderson4D.mergeGlobalConstant_absorbs_tree_sixtyFour {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (mu : t.Multiplicities) (C0 D : ℝ) (hC0 : 1000 < C0) (hD : D = Real.exp (C0 ^ 10)) (n m : ℕ) (htotal : totalMultiplicity mu = 2 * n) (hm : m ≤ 2 * n) :
    C0 ^ m * D ^ t.BranchNodes.card * 64 ^ n ≤ mergeGlobalConstant C0 D ^ n

    Tree-facing specialization with the full 64^n loss budget.