RoseTree double-cut coassociativity for Δ^c (combinatorial core of MCB 1.2.10)

[MCB25] [foissy-introduction-hopf-algebras-trees]

The combinatorial heart of Δ^c coassociativity: both (Δ^c ⊗ id) ∘ Δ^c and (id ⊗ Δ^c) ∘ Δ^c enumerate ordered pairs of nested admissible cuts of a tree, and under trace coherence the two enumerations agree as Nonplanar multisets. This file proves that agreement at the planar level (where cutSummandsCP recurses structurally); TraceNonplanar.lean descends it through Nonplanar.mk to close the Nonplanar doubleCut_eq.

Main results

• coassT — per-tree coassoc (dcLHSP τ t).map proj3 = (dcRHSP τ t).map proj3.
• coassL/coassA — children-list / per-child coassoc (mutual, mirroring cutListSummandsG/augActionG); coassA is where TraceCoherentP reconciles the marker a deeper cut writes on a trunk.
• dclN_clconv/dcrN_clconv — the two second-cut maps are multiplicative over the children-list convolution clconv (the engine of the induction).
• mconv — multiset convolution monoid, with mconv_prod_hom.

Status

[UPSTREAM] candidate. Sorry-free. The bijection statement was validated by exhaustive small-tree computation (canonical-form multiset comparison) before the structural proof, including the failure for marker-sensitive τ.

@[reducible, inline]

abbrev DoubleCut.FP (α : Type u_3) : Type u_3

Equations

• DoubleCut.FP α = RootedTree.Forest (RoseTree α)

@[reducible, inline]

abbrev DoubleCut.Pair (α : Type u_3) : Type u_3

Equations

• DoubleCut.Pair α = (DoubleCut.FP α × DoubleCut.FP α)

Generic multiset convolution over an additive monoid

mconv s t = (s ×ˢ t).map (·+·) — the convolution of two multisets over an AddCommMonoid. This is the per-component combination of cut pairs (forest crowns/trunks add) and, at the triple level, the combination of double-cut layers. Proved a commutative monoid with unit {0}.

def DoubleCut.mconv {M : Type u_3} [Add M] (s t : Multiset M) : Multiset M

Multiset convolution over an additive structure.

Equations

• DoubleCut.mconv s t = Multiset.map (fun (p : M × M) => p.1 + p.2) (s ×ˢ t)

theorem DoubleCut.mconv_bind {M : Type u_3} [AddCommMonoid M] (s t : Multiset M) : mconv s t = s.bind fun (a : M) => Multiset.map (fun (b : M) => a + b) t

theorem DoubleCut.mconv_zero_left {M : Type u_3} [AddCommMonoid M] (t : Multiset M) : mconv {0} t = t

theorem DoubleCut.mconv_comm {M : Type u_3} [AddCommMonoid M] (s t : Multiset M) : mconv s t = mconv t s

theorem DoubleCut.mconv_zero_right {M : Type u_3} [AddCommMonoid M] (s : Multiset M) : mconv s {0} = s

theorem DoubleCut.mconv_assoc {M : Type u_3} [AddCommMonoid M] (s t u : Multiset M) : mconv (mconv s t) u = mconv s (mconv t u)

theorem DoubleCut.mconv_left_comm {M : Type u_3} [AddCommMonoid M] (s t u : Multiset M) : mconv s (mconv t u) = mconv t (mconv s u)

instance DoubleCut.instLeftCommMconv {M : Type u_3} [AddCommMonoid M] : LeftCommutative mconv

theorem DoubleCut.mconv_add_left {M : Type u_3} [AddCommMonoid M] (s t u : Multiset M) : mconv (s + t) u = mconv s u + mconv t u

theorem DoubleCut.mconv_add_right {M : Type u_3} [AddCommMonoid M] (s t u : Multiset M) : mconv s (t + u) = mconv s t + mconv s u

@[reducible, inline]

abbrev DoubleCut.convFP {α : Type u_1} {β : Type u_2} : Multiset (Pair (α ⊕ β)) → Multiset (Pair (α ⊕ β)) → Multiset (Pair (α ⊕ β))

Equations

• DoubleCut.convFP = DoubleCut.mconv

theorem DoubleCut.convFP_eq {α : Type u_1} {β : Type u_2} (s acc : Multiset (Pair (α ⊕ β))) : convFP s acc = Multiset.map (fun (pq : Pair (α ⊕ β) × Pair (α ⊕ β)) => (pq.1.1 + pq.2.1, pq.1.2 + pq.2.2)) (s ×ˢ acc)

def DoubleCut.treeCutsP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : Multiset (Pair (α ⊕ β))

RoseTree tree-cut enumerator (crown forest, trunk forest).

Equations

• DoubleCut.treeCutsP τ t = ({t}, 0) ::ₘ Multiset.map (fun (p : RootedTree.Forest (RoseTree (α ⊕ β)) × RoseTree (α ⊕ β)) => (p.1, {p.2})) (RootedTree.ConnesKreimer.cutSummandsCP τ t)

def DoubleCut.forestCutsP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) : Multiset (Pair (α ⊕ β))

Forest-cut enumerator: convolution over the component trees.

Equations

• DoubleCut.forestCutsP τ F = Multiset.foldr DoubleCut.convFP {(0, 0)} (Multiset.map (DoubleCut.treeCutsP τ) F)

def DoubleCut.dcLHSP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β))

LHS double-cut: re-cut the crown.

Equations

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

def DoubleCut.dcRHSP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β))

RHS double-cut: re-cut the trunk.

Equations

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

def DoubleCut.dcForestLHSP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β))

Forest double-cut LHS (outer is a forest cut).

Equations

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

def DoubleCut.dcForestRHSP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β))

Equations

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

def DoubleCut.proj3 {α : Type u_1} {β : Type u_2} (q : FP (α ⊕ β) × FP (α ⊕ β) × FP (α ⊕ β)) : Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β))

Projection of a triple of planar forests to nonplanar (mod planar order).

Equations

• DoubleCut.proj3 q = (Multiset.map RootedTree.Nonplanar.mk q.1, Multiset.map RootedTree.Nonplanar.mk q.2.1, Multiset.map RootedTree.Nonplanar.mk q.2.2)

Basic recursions for forestCutsP

theorem DoubleCut.forestCutsP_zero {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : forestCutsP τ 0 = {(0, 0)}

theorem DoubleCut.forestCutsP_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) : forestCutsP τ (t ::ₘ F) = convFP (treeCutsP τ t) (forestCutsP τ F)

theorem DoubleCut.forestCutsP_singleton {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : forestCutsP τ {t} = treeCutsP τ t

theorem DoubleCut.forestCutsP_add {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F G : FP (α ⊕ β)) : forestCutsP τ (F + G) = convFP (forestCutsP τ F) (forestCutsP τ G)

Multiplicativity machinery

@[reducible, inline]

abbrev DoubleCut.Triple (α : Type u_3) : Type u_3

Equations

• DoubleCut.Triple α = (DoubleCut.FP α × DoubleCut.FP α × DoubleCut.FP α)

theorem DoubleCut.mconv_map_hom2 {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [Add N] (f f' g : M → N) (hg : ∀ (x y : M), g (x + y) = f x + f' y) (X Y : Multiset M) : Multiset.map g (mconv X Y) = mconv (Multiset.map f X) (Multiset.map f' Y)

mconv commutes with a map whose combination splits as g (x+y) = f x + f' y.

theorem DoubleCut.mconv_hom_bind {M : Type u_3} {T : Type u_4} [AddCommMonoid M] [AddCommMonoid T] (h : M → Multiset T) (hh : ∀ (p q : M), h (p + q) = mconv (h p) (h q)) (A B : Multiset M) : (mconv A B).bind h = mconv (A.bind h) (B.bind h)

A monoid hom h : (M,+) → (Multiset T, mconv) turns bind over a convolution into a convolution of binds.

proj3 is additive

theorem DoubleCut.proj3_add {α : Type u_1} {β : Type u_2} (p q : Triple (α ⊕ β)) : proj3 (p + q) = proj3 p + proj3 q

theorem DoubleCut.proj3_mconv {α : Type u_1} {β : Type u_2} (X Y : Multiset (Triple (α ⊕ β))) : Multiset.map proj3 (mconv X Y) = mconv (Multiset.map proj3 X) (Multiset.map proj3 Y)

The two second-cut maps are monoid homs

def DoubleCut.hL {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p : Pair (α ⊕ β)) : Multiset (Triple (α ⊕ β))

LHS second cut: re-cut the crown p.1, carrying trunk p.2.

Equations

• DoubleCut.hL τ p = Multiset.map (fun (A12 : DoubleCut.Pair (α ⊕ β)) => (A12.1, A12.2, p.2)) (DoubleCut.forestCutsP τ p.1)

def DoubleCut.hR {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p : Pair (α ⊕ β)) : Multiset (Triple (α ⊕ β))

RHS second cut: re-cut the trunk p.2, carrying crown p.1.

Equations

• DoubleCut.hR τ p = Multiset.map (fun (B12 : DoubleCut.Pair (α ⊕ β)) => (p.1, B12.1, B12.2)) (DoubleCut.forestCutsP τ p.2)

theorem DoubleCut.hL_hom {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p q : Pair (α ⊕ β)) : hL τ (p + q) = mconv (hL τ p) (hL τ q)

theorem DoubleCut.hR_hom {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (p q : Pair (α ⊕ β)) : hR τ (p + q) = mconv (hR τ p) (hR τ q)

Double-cut enumerators as binds of hL/hR

theorem DoubleCut.dcLHSP_eq_bind {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : dcLHSP τ t = (treeCutsP τ t).bind (hL τ)

theorem DoubleCut.dcRHSP_eq_bind {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : dcRHSP τ t = (treeCutsP τ t).bind (hR τ)

theorem DoubleCut.dcForestLHSP_eq_bind {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) : dcForestLHSP τ F = (forestCutsP τ F).bind (hL τ)

theorem DoubleCut.dcForestRHSP_eq_bind {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) : dcForestRHSP τ F = (forestCutsP τ F).bind (hR τ)

Multiplicativity of the forest double-cut

theorem DoubleCut.dcForestLHSP_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) : dcForestLHSP τ (t ::ₘ F) = mconv (dcLHSP τ t) (dcForestLHSP τ F)

theorem DoubleCut.dcForestRHSP_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (F : FP (α ⊕ β)) : dcForestRHSP τ (t ::ₘ F) = mconv (dcRHSP τ t) (dcForestRHSP τ F)

theorem DoubleCut.dcForestLHSP_zero {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : dcForestLHSP τ 0 = {(0, 0, 0)}

theorem DoubleCut.dcForestRHSP_zero {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : dcForestRHSP τ 0 = {(0, 0, 0)}

Forest coassoc from per-component tree coassoc

theorem DoubleCut.coassFP_of_components {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) (H : ∀ t ∈ F, Multiset.map proj3 (dcLHSP τ t) = Multiset.map proj3 (dcRHSP τ t)) : Multiset.map proj3 (dcForestLHSP τ F) = Multiset.map proj3 (dcForestRHSP τ F)

Node-level reduction of the per-tree double cut

The children-list cut enumerator (with trace leaves in the remainder), distinct from forestCutsP (deletion). treeCutsP/dcLHSP/dcRHSP of a node a cs decompose over it.

@[reducible, inline]

abbrev DoubleCut.Cl {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (cs : List (RoseTree (α ⊕ β))) : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))

Children-list cut enumerator: cutListSummandsG (extractC τ).

Equations

• DoubleCut.Cl τ cs = RootedTree.ConnesKreimer.cutListSummandsG (RootedTree.ConnesKreimer.extractC τ) cs

theorem DoubleCut.treeCutsP_node {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : treeCutsP τ (RoseTree.node a cs) = ({RoseTree.node a cs}, 0) ::ₘ Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, {RoseTree.node a p.2})) (Cl τ cs)

treeCutsP of a node: full cut, plus root-preserving cuts coming from the children-list cut wrapped with node a.

theorem DoubleCut.dcLHSP_node {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : dcLHSP τ (RoseTree.node a cs) = ({RoseTree.node a cs}, 0, 0) ::ₘ Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, {RoseTree.node a p.2}, 0)) (Cl τ cs) + (Cl τ cs).bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (c12 : Pair (α ⊕ β)) => (c12.1, c12.2, {RoseTree.node a p.2})) (forestCutsP τ p.1)

LHS double cut of a node: the full-cut boundary triple, the "split-at-root" middle terms, and the genuine children-crown re-cuts.

theorem DoubleCut.dcRHSP_node {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a : α ⊕ β) (cs : List (RoseTree (α ⊕ β))) : dcRHSP τ (RoseTree.node a cs) = {({RoseTree.node a cs}, 0, 0)} + (Cl τ cs).bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (B12 : Pair (α ⊕ β)) => (p.1, B12.1, B12.2)) (treeCutsP τ (RoseTree.node a p.2))

RHS double cut of a node: the full-cut boundary triple plus, for each children-cut, re-cutting the trunk tree node a remainder.

Children-list convolution clconv and Cl as a monoid hom

Cl τ = cutListSummandsG (extractC τ) is a monoid hom from (List, ++) to (Multiset (Forest × List), clconv). clconv is the cons-combiner of cutListSummandsG (forest add, list append) — a (non-commutative) monoid with unit {(0, [])}.

def DoubleCut.clconv {α : Type u_1} {β : Type u_2} (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))

The children-list cut combiner: add crown forests, append remainders.

Equations

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

theorem DoubleCut.clconv_bind {α : Type u_1} {β : Type u_2} (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : clconv S T = S.bind fun (s : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (t : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (s.1 + t.1, s.2 ++ t.2)) T

theorem DoubleCut.clconv_unit_left {α : Type u_1} {β : Type u_2} (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : clconv {(0, [])} S = S

theorem DoubleCut.clconv_unit_right {α : Type u_1} {β : Type u_2} (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : clconv S {(0, [])} = S

theorem DoubleCut.clconv_assoc {α : Type u_1} {β : Type u_2} (S T U : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : clconv (clconv S T) U = clconv S (clconv T U)

theorem DoubleCut.Cl_nil {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : Cl τ [] = {(0, [])}

theorem DoubleCut.Cl_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) (ts : List (RoseTree (α ⊕ β))) : Cl τ (t :: ts) = clconv (RootedTree.ConnesKreimer.augActionG (RootedTree.ConnesKreimer.extractC τ) t) (Cl τ ts)

theorem DoubleCut.Cl_append {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (l₁ l₂ : List (RoseTree (α ⊕ β))) : Cl τ (l₁ ++ l₂) = clconv (Cl τ l₁) (Cl τ l₂)

Generic convolution-multiplicativity over a cartesian-product cut

mconv_prod_hom: when the per-element map ΦN is a convolution hom for a combiner comb, binding ΦN over a comb-convolution of S and T factors as the mconv of the per-side binds. This is the engine of the children-list cons step.

theorem DoubleCut.mconv_bind_distrib {M : Type u_3} {A : Type u_4} {B : Type u_5} [AddCommMonoid M] (f : A → Multiset M) (g : B → Multiset M) (S : Multiset A) (T : Multiset B) : mconv (S.bind f) (T.bind g) = S.bind fun (a : A) => T.bind fun (b : B) => mconv (f a) (g b)

theorem DoubleCut.mconv_prod_hom {M : Type u_3} {A : Type u_4} [AddCommMonoid M] (ΦN : A → Multiset M) (comb : A → A → A) (hΦ : ∀ (s t : A), ΦN (comb s t) = mconv (ΦN s) (ΦN t)) (S T : Multiset A) : (Multiset.map (fun (pr : A × A) => comb pr.1 pr.2) (S ×ˢ T)).bind ΦN = mconv (S.bind ΦN) (T.bind ΦN)

The two double-cut maps and their clconv-multiplicativity (mod proj)

dcl/dcr are the children-list double-cut enumerators (re-cut crown via forestCutsP, vs re-cut remainder via Cl). Projected through proj3L (third component = remainder list → multiset of nonplanar trees), each is multiplicative over clconv.

def DoubleCut.proj3L {α : Type u_1} {β : Type u_2} (q : FP (α ⊕ β) × FP (α ⊕ β) × List (RoseTree (α ⊕ β))) : Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β))

Projection of a (crown, mid, remainder-list) triple to nonplanar.

Equations

• DoubleCut.proj3L q = (Multiset.map RootedTree.Nonplanar.mk q.1, Multiset.map RootedTree.Nonplanar.mk q.2.1, ↑(List.map RootedTree.Nonplanar.mk q.2.2))

theorem DoubleCut.proj3L_add {α : Type u_1} {β : Type u_2} (a a' b b' : FP (α ⊕ β)) (l l' : List (RoseTree (α ⊕ β))) : proj3L (a + a', b + b', l ++ l') = proj3L (a, b, l) + proj3L (a', b', l')

def DoubleCut.dcl {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × List (RoseTree (α ⊕ β)))

LHS children-list double cut: re-cut crown p.1, keep remainder p.2.

Equations

• DoubleCut.dcl τ S = S.bind fun (p : DoubleCut.FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (c12 : DoubleCut.Pair (α ⊕ β)) => (c12.1, c12.2, p.2)) (DoubleCut.forestCutsP τ p.1)

def DoubleCut.dcr {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset (FP (α ⊕ β) × FP (α ⊕ β) × List (RoseTree (α ⊕ β)))

RHS children-list double cut: keep crown p.1, re-cut remainder p.2.

Equations

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

theorem DoubleCut.dclN_eq {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset.map proj3L (dcl τ S) = S.bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (c12 : Pair (α ⊕ β)) => proj3L (c12.1, c12.2, p.2)) (forestCutsP τ p.1)

theorem DoubleCut.dcrN_eq {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset.map proj3L (dcr τ S) = S.bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (q : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => proj3L (p.1, q.1, q.2)) (Cl τ p.2)

theorem DoubleCut.dclN_clconv {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset.map proj3L (dcl τ (clconv S T)) = mconv (Multiset.map proj3L (dcl τ S)) (Multiset.map proj3L (dcl τ T))

theorem DoubleCut.dcrN_clconv {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (S T : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : Multiset.map proj3L (dcr τ (clconv S T)) = mconv (Multiset.map proj3L (dcr τ S)) (Multiset.map proj3L (dcr τ T))

The children-list coassociativity engine

coassL: the root-free children-list coassoc (LLEM3), proved by induction on the list using clconv-multiplicativity, the per-child coassA, and the tail IH. coassA (per-child) reduces to coassL of the child's children with TraceCoherent reconciling the extract-whole marker.

def DoubleCut.TraceCoherentP {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) : Prop

RoseTree trace coherence: τ of a cut trunk equals τ of the tree. The descent of TraceCoherent (Nonplanar) along Nonplanar.mk.

Equations

• DoubleCut.TraceCoherentP τ = ∀ (t : RoseTree (α ⊕ β)), ∀ p ∈ RootedTree.ConnesKreimer.cutSummandsCP τ t, τ p.2 = τ t

theorem DoubleCut.Cl_singleton {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (t : RoseTree (α ⊕ β)) : Cl τ [t] = RootedTree.ConnesKreimer.augActionG (RootedTree.ConnesKreimer.extractC τ) t

Children-list cut of a singleton list is the per-child augmented action.

theorem DoubleCut.proj3L_list_wrap {α : Type u_1} {β : Type u_2} (a' : α ⊕ β) (x y : FP (α ⊕ β)) (l : List (RoseTree (α ⊕ β))) : proj3L (x, y, [RoseTree.node a' l]) = ((proj3L (x, y, l)).1, (proj3L (x, y, l)).2.1, {RootedTree.Nonplanar.node a' (proj3L (x, y, l)).2.2})

Projecting a triple whose remainder is a singleton [node a' l] equals nonplanar node a'-wrapping the projection with raw remainder l.

theorem DoubleCut.dcl_INH_wrap {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a' : α ⊕ β) (cs'' : List (RoseTree (α ⊕ β))) : Multiset.map proj3L (dcl τ (Multiset.map (fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, [RoseTree.node a' p.2])) (Cl τ cs''))) = Multiset.map (fun (z : Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β))) => (z.1, z.2.1, {RootedTree.Nonplanar.node a' z.2.2})) (Multiset.map proj3L (dcl τ (Cl τ cs'')))

The [node a']-wrapped dcl of the children cut, projected, equals the nonplanar node a'-wrap of the projected dcl.

theorem DoubleCut.dcr_nonEW_wrap {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (a' : α ⊕ β) (cs'' : List (RoseTree (α ⊕ β))) : Multiset.map proj3L ((Cl τ cs'').bind fun (p : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => Multiset.map (fun (p'' : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (p.1, p''.1, [RoseTree.node a' p''.2])) (Cl τ p.2)) = Multiset.map (fun (z : Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β)) × Multiset (RootedTree.Nonplanar (α ⊕ β))) => (z.1, z.2.1, {RootedTree.Nonplanar.node a' z.2.2})) (Multiset.map proj3L (dcr τ (Cl τ cs'')))

The non-extract-whole part of the trunk re-cut, projected, equals the nonplanar node a'-wrap of the projected dcr.

theorem DoubleCut.dcl_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) (l : List (RoseTree (α ⊕ β))) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : dcl τ ((F, l) ::ₘ S) = Multiset.map (fun (c12 : Pair (α ⊕ β)) => (c12.1, c12.2, l)) (forestCutsP τ F) + dcl τ S

dcl distributes over a cons outer cut.

theorem DoubleCut.dcr_cons {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (F : FP (α ⊕ β)) (l : List (RoseTree (α ⊕ β))) (S : Multiset (FP (α ⊕ β) × List (RoseTree (α ⊕ β)))) : dcr τ ((F, l) ::ₘ S) = Multiset.map (fun (q : FP (α ⊕ β) × List (RoseTree (α ⊕ β))) => (F, q.1, q.2)) (Cl τ l) + dcr τ S

dcr distributes over a cons outer cut.

Children-list coassoc (coassL) and per-child coassoc (coassA), proved by mutual structural recursion mirroring cutListSummandsG/augActionG. coassL is the engine of the per-tree node step; coassA is the coherence-using combinatorial core.

theorem DoubleCut.coassL {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (cs : List (RoseTree (α ⊕ β))) : Multiset.map proj3L (dcl τ (Cl τ cs)) = Multiset.map proj3L (dcr τ (Cl τ cs))

theorem DoubleCut.coassA {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (c : RoseTree (α ⊕ β)) : Multiset.map proj3L (dcl τ (RootedTree.ConnesKreimer.augActionG (RootedTree.ConnesKreimer.extractC τ) c)) = Multiset.map proj3L (dcr τ (RootedTree.ConnesKreimer.augActionG (RootedTree.ConnesKreimer.extractC τ) c))

Per-tree coassoc coassT from coassL (node reduction + root wrap)

theorem DoubleCut.coassT {α : Type u_1} {β : Type u_2} (τ : RoseTree (α ⊕ β) → β) (hτ : TraceCoherentP τ) (t : RoseTree (α ⊕ β)) : Multiset.map proj3 (dcLHSP τ t) = Multiset.map proj3 (dcRHSP τ t)