Tree symmetry for the v5 policy

The underlying subtree permutations are policy-independent and live in FD1D.TreeSymmetry. This module proves that the recursively propagated v5 rates and deletion masses are equivariant under those permutations.

theorem FD1D.V5.TreeSymmetry.rate_aboveSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : TreePolicy.rate (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a k w = TreePolicy.rate (Dynamics.aggregatedInventory x) a k w

Rates at every level weakly above the swapped node are unchanged.

theorem FD1D.V5.TreeSymmetry.rate_subtreeSwap_zero {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) (w : DyadicNode (d + 1)) : TreePolicy.rate (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a (d + 1) ((TreeSymmetry.subtreeSwap v 0) w) = TreePolicy.rate (Dynamics.aggregatedInventory x) a (d + 1) w

At the first level below v, rates follow the child swap.

theorem FD1D.V5.TreeSymmetry.rate_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {r : ℕ} (hrn : r ≤ n) (w : DyadicNode (d + 1 + r)) : TreePolicy.rate (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a (d + 1 + r) ((TreeSymmetry.subtreeSwap v r) w) = TreePolicy.rate (Dynamics.aggregatedInventory x) a (d + 1 + r) w

Rates at descendant nodes are transported by the subtree swap.

theorem FD1D.V5.TreeSymmetry.deletionMass_aboveSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k ≤ d) (w : DyadicNode k) : TreePolicy.deletionMass (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a k w = TreePolicy.deletionMass (Dynamics.aggregatedInventory x) a k w

Deletion masses at and above the swapped node are unchanged.

theorem FD1D.V5.TreeSymmetry.deletionMass_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {r : ℕ} (hrn : r ≤ n) (w : DyadicNode (d + 1 + r)) : TreePolicy.deletionMass (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a (d + 1 + r) ((TreeSymmetry.subtreeSwap v r) w) = TreePolicy.deletionMass (Dynamics.aggregatedInventory x) a (d + 1 + r) w

Deletion masses at descendants are transported by the subtree swap.

theorem FD1D.V5.TreeSymmetry.imbalance_swapNode {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a d v = -TreePolicy.imbalance (Dynamics.aggregatedInventory x) a d v

The fixed-label deletion imbalance at the swapped node changes sign.

theorem FD1D.V5.TreeSymmetry.imbalance_strictAncestor {d n m : ℕ} (v : DyadicNode d) (x : InventoryState (DyadicNode (d + 1 + n)) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x)) a k w = TreePolicy.imbalance (Dynamics.aggregatedInventory x) a k w

A strict ancestor's deletion imbalance is unchanged.

Arbitrary-depth wrappers

theorem FD1D.V5.TreeSymmetry.deletionMass_leafSwapWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) (w : DyadicNode L) : TreePolicy.deletionMass (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwapWithGap v r hlevel) x)) a L ((TreeSymmetry.leafSwapWithGap v r hlevel) w) = TreePolicy.deletionMass (Dynamics.aggregatedInventory x) a L w

theorem FD1D.V5.TreeSymmetry.imbalance_swapNodeWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwapWithGap v r hlevel) x)) a d v = -TreePolicy.imbalance (Dynamics.aggregatedInventory x) a d v

theorem FD1D.V5.TreeSymmetry.imbalance_strictAncestorWithGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (x : InventoryState (DyadicNode L) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwapWithGap v r hlevel) x)) a k w = TreePolicy.imbalance (Dynamics.aggregatedInventory x) a k w

theorem FD1D.V5.TreeSymmetry.deletionMass_leafSwap {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) (w : DyadicNode L) : TreePolicy.deletionMass (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwap hdL v) x)) a L ((TreeSymmetry.leafSwap hdL v) w) = TreePolicy.deletionMass (Dynamics.aggregatedInventory x) a L w

theorem FD1D.V5.TreeSymmetry.imbalance_swapNode_general {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwap hdL v) x)) a d v = -TreePolicy.imbalance (Dynamics.aggregatedInventory x) a d v

theorem FD1D.V5.TreeSymmetry.imbalance_strictAncestor_general {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (x : InventoryState (DyadicNode L) m) (a : ℝ) {k : ℕ} (hkd : k < d) (w : DyadicNode k) : TreePolicy.imbalance (Dynamics.aggregatedInventory ((TreeSymmetry.inventorySwap hdL v) x)) a k w = TreePolicy.imbalance (Dynamics.aggregatedInventory x) a k w

Kernel equivariance and invariant stationary laws

theorem FD1D.V5.TreeSymmetry.deletionRule_prob_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode (d + 1 + n)) m) (w : DyadicNode (d + 1 + n)) : (Dynamics.deletionRule a ha hm).prob ((TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n)) x) ((TreeSymmetry.subtreeSwap v n) w) = (Dynamics.deletionRule a ha hm).prob x w

theorem FD1D.V5.TreeSymmetry.kernel_equivariant_subtreeSwap {d n m : ℕ} (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (Dynamics.kernel a ha hm).Equivariant (TreeSymmetry.inventoryPerm (TreeSymmetry.subtreeSwap v n))

theorem FD1D.V5.TreeSymmetry.kernel_equivariant_withGap {d L m : ℕ} (v : DyadicNode d) (r : ℕ) (hlevel : d + 1 + r = L) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (Dynamics.kernel a ha hm).Equivariant (TreeSymmetry.inventorySwapWithGap v r hlevel)

theorem FD1D.V5.TreeSymmetry.kernel_equivariant {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) : (Dynamics.kernel a ha hm).Equivariant (TreeSymmetry.inventorySwap hdL v)

theorem FD1D.V5.TreeSymmetry.stationary_lawInvariant {d L m : ℕ} (hdL : d < L) (v : DyadicNode d) (a : ℝ) (ha : 0 < a) (hm : 0 < m) {μ : FiniteLaw (InventoryState (DyadicNode L) m)} (hμ : (Dynamics.kernel a ha hm).IsStationary μ) : FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap hdL v)