Documentation

Linglib.Core.Combinatorics.RootedTree.AdmissibleCut

⚠️ LEGACY — RESTORED SHIM (2026-05-13) #

Restored from commit e0876460^ after deletion at 0.230.913. Consumer migration (Phase D per scratch/mcb_full_architecture.md) hadn't happened; Merge stack files broke on clean build. Will be re-deleted when Phase D lands — its canonical replacement is Linglib/Core/Combinatorics/RootedTree/PlanarCut.lean (Cut/ChildCut/ChildCutList mutual inductive on Planar α).

Do not extend, do not add new consumers.

Admissible Cuts on Trees @cite{marcolli-chomsky-berwick-2025} #

Per @cite{marcolli-chomsky-berwick-2025} Definition 1.2.6, an admissible cut of a binary rooted tree T is a removal of a collection of edges of T such that no two lie on the same root-to-leaf path. Equivalently (Lemma 1.2.7), the data of an admissible cut on T is the same as a forest F_v = T_{v₁} ⊔ ⋯ ⊔ T_{vₙ} of disjoint accessible terms of T.

Trees with scalar trace labels #

This file defines CutShape on TraceTree α β (not on DecoratedTree α). The TraceTree carrier has scalar trace labels (.trace (b : β)) rather than recursive subtree data. This is the carrier the bialgebra of @cite{marcolli-chomsky-berwick-2025} Lemma 1.2.10 actually inhabits; see Decorated.lean for the rationale: per @cite{marcolli-skigin-2025} §10.1 (clarifying the brief discussion in M-C-B §1.3), trace labels are elements of a disjoint marked copy ̄SO₀ of the leaf alphabet, NOT recursive subtrees, for the bialgebra structure to be well-formed.

For the bialgebra layer, β = Unit (no informative trace label) — the minimal instance, sufficient for coassoc but a strict simplification of M-S. For the linguistic layer (CI interpretation, FormCopy), a richer β plus a head-function-transparent extractor realizes @cite{marcolli-skigin-2025} Definition 10.3 (head function projects each contracted subtree to its head leaf's struck-through label).

This file is [UPSTREAM] — generic over α : Type* and β : Type*.

Crucial M-C-B reading: leaves ARE accessible terms #

Per @cite{marcolli-chomsky-berwick-2025} Definition 1.2.2, accessible terms are subtrees T_v for v ∈ V_int(T) := V(T) \ {root of T}. M-C-B's "internal" excludes the root vertex but includes leaves — so leaves of T are accessible terms. (Verified against the worked example on book p. 35, inline in §1.2 just before §1.2.1.)

Representation: 5-constructor enum #

A CutShape T for T : TraceTree α β records cut choices position- by-position. Leaves admit only the trivial pass-through (no edges to cut); nodes have four choices based on (cut left edge?) × (cut right edge?). The antichain condition (M-C-B Def 1.2.6: no two cuts on the same root-leaf path) is baked in by construction.

Layer status #

[UPSTREAM]. Future home is something like Mathlib.Combinatorics.HopfAlgebra.ConnesKreimer.AdmissibleCut. This file is part of the Stage 0.5 hoist out of Theories/Syntax/Minimalist/Hopf/ (per scratch/mcb_stage1_plan.md).

§1: Cut shape #

Universe-polymorphic in α : Type* and β : Type*. The inductive takes both as parameters (not per-constructor indices), letting mathlib upstream reuse this construction over arbitrary leaf-and-trace-label types.

source
inductive ConnesKreimer.CutShape {α : Type u_3} {β : Type u_4} :
TraceTree α β → Type (max u_3 u_4)

An admissible cut on a tree T : TraceTree α β.

Trace-extraction restriction (substrate fix for coassoc). The cuts that EXTRACT a child subtree (bothCut, onlyLeftCut, onlyRightCut) require that child to NOT be a .trace marker (IsNotTrace). Without this restriction, iterated cuts on the remainder of an outer cut would accumulate .trace-of-.trace nesting, breaking the cuts-of-cuts bijection (M-C-B Lemma 1.2.10 / Foissy 2002 §2). With scalar trace labels (β not DecoratedTree), this nesting is what causes the basis cardinality to blow up; the IsNotTrace constraint prevents it.

The bothRecurse constructor — which doesn't extract anything at this node — has no restriction; it composes recursively into the children's CutShapes. The atomic atLeaf / atTrace constructors are also unrestricted.

Instances For

    §2: The empty (trivial) cut #

    source
    def ConnesKreimer.CutShape.empty {α : Type u_1} {β : Type u_2} (T : TraceTree α β) :
    CutShape T

    The empty cut on T: extract nothing, leave T unchanged.

    Equations
    Instances For

      §3: Decidable equality and finite enumeration #

      source
      @[implicit_reducible]
      instance ConnesKreimer.CutShape.decEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (T : TraceTree α β) :
      DecidableEq (CutShape T)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def ConnesKreimer.CutShape.all {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (T : TraceTree α β) :
      Finset (CutShape T)

      The finite set of all cut shapes on T. The bothCut / onlyLeftCut / onlyRightCut constructors are conditionally included based on whether the relevant children pass IsNotTrace.

      Equations
      Instances For
        source
        theorem ConnesKreimer.CutShape.mem_all {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (T : TraceTree α β) (c : CutShape T) :
        c ∈ all T

        Every cut shape on T is in all T.

        source
        @[implicit_reducible]
        instance ConnesKreimer.CutShape.fintype {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (T : TraceTree α β) :
        Fintype (CutShape T)
        Equations

        §4: Pruned forest F_v and remainder T/^c F_v #

        For an admissible cut c : CutShape T:

        The trace label is a SCALAR β (not a recursive subtree). For β = Unit, the trace marker carries no information; for β = α, it carries a head label per @cite{marcolli-skigin-2025} Definition 10.3.

        source
        def ConnesKreimer.CutShape.cutForest {α : Type u_1} {β : Type u_2} {T : TraceTree α β} :
        CutShape T → TraceForest α β

        The pruned forest of a cut: the multiset of extracted subtrees. M-C-B Definition 1.2.4: F_v = T_{v_1} ⊔ ⋯ ⊔ T_{v_n}.

        Equations
        Instances For
          source
          def ConnesKreimer.CutShape.remainder {α : Type u_1} {β : Type u_2} [Inhabited β] {T : TraceTree α β} :
          CutShape T → TraceTree α β

          The remainder of a cut (contraction-with-trace, M-C-B Def 1.2.4): T with each cut subtree replaced by a .trace default leaf.

          The trace label is default : β from [Inhabited β]. Both algebraic-side β = Unit (default = (), irrelevant) and linguistic-side β = Nat (default = 0, sentinel binding index) have Inhabited automatically. Callers wanting a specific label can provide it via a custom Inhabited β instance at the call site (rare; in practice the default suffices).

          Note: by the IsNotTrace constraint on the extracting constructors, the children getting wrapped with .trace here are guaranteed to NOT already be .trace markers.

          Equations
          Instances For
            source
            def ConnesKreimer.CutShape.remainderDeletion {α : Type u_1} {β : Type u_2} {T : TraceTree α β} :
            CutShape T → Option (TraceTree α β)

            The remainder of a cut (deletion-with-rebinarization, M-C-B Def 1.2.5): T with each cut subtree REMOVED (no trace), then edge-contracted to recover binarity. Used by Δ^d (the coproduct that linguistic Merge uses, per M-C-B Definition 1.3.4 p. 42: "consider the coproduct Δ = Δ^d of (1.2.8)").

            Returns Option (TraceTree α β) because cutting both children of a node leaves a vertex with no children — neither a leaf nor a binary node. Such a vertex collapses (returns None); upstream binders absorb the collapse via edge contraction:

            • At a node, if BOTH children's deletion-remainder collapse, the node itself collapses.
            • At a node, if ONE child collapses, the other becomes the remainder (the parent's edge to the survivor is "contracted", effectively absorbing the parent into the survivor).

            This handling is faithful to M-C-B Def 1.2.5's "unique maximal binary rooted tree obtainable via contraction."

            Equations
            Instances For

              §5: Structural facts about cutForest #

              source
              theorem ConnesKreimer.CutShape.size_lt_of_mem_cutForest {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (t : TraceTree α β) :
              t ∈ c.cutForest → t.size < T.size

              Every subtree extracted by a cut on T is a proper subtree of T — its size is strictly less than T.size. Used to prove T ∉ cutForest c, which in turn drives the term-elimination in algebraic Merge bridge proofs (Theories/Syntax/Minimalist/Merge/Action.lean).

              source
              theorem ConnesKreimer.CutShape.not_mem_cutForest_self {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
              T ∉ c.cutForest

              A tree is not a member of any of its own cut forests (proper subtrees).

              source
              theorem ConnesKreimer.CutShape.cutForest_ne_singleton_self {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
              c.cutForest ≠ {T}

              A cut forest never equals the singleton multiset of the source tree.

              source
              theorem ConnesKreimer.CutShape.cutForest_add_ne_insert_pair {α : Type u_1} {β : Type u_2} {S S' : TraceTree α β} (c : CutShape S) (c' : CutShape S') :
              c.cutForest + c'.cutForest ≠ {S, S'}

              Pair-cross elimination: for cuts c : CutShape S and c' : CutShape S', the multiset sum cutForest c + cutForest c' cannot equal {S, S'}.

              Used in the algebraic Merge bridge (Theories/Syntax/Minimalist/Merge/Action.lean) to eliminate cross-terms in the expansion of Δ^d({S, S'}): any cut on one side combined with any cut on the other side produces a cut-forest different from {S, S'}, so δ_{S,S'} zeroes that term.

              Proof: if the sum were {S, S'}, then S and S' are each in either cutForest c or cutForest c'. Membership in cutForest c (resp. c') forces a strict size decrease versus S (resp. S'), so S ∉ cutForest c and S' ∉ cutForest c'. This forces S ∈ cutForest c' and S' ∈ cutForest c, yielding S.size < S'.size and S'.size < S.size — contradiction.

              source
              theorem ConnesKreimer.CutShape.eq_empty_of_cutForest_eq_zero {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
              c.cutForest = 0 → c = empty T

              Empty-cut characterization: cutForest c = 0 iff c = empty T.

              Used in the algebraic Merge bridge's factor-out lemma to identify the unique LEFT-empty contributor in comulTreeDel T.

              source
              theorem ConnesKreimer.CutShape.cutForest_eq_zero_iff {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
              c.cutForest = 0 ↔ c = empty T

              Combined empty-cut characterization: cutForest c = 0 ↔ c = empty T. The mpr direction restates cutForest_empty (in §6 below).

              @cite{marcolli-chomsky-berwick-2025} §1.5

              Per @cite{marcolli-chomsky-berwick-2025} Definition in §1.5.2 (p. 59), each extracted accessible term T_v ⊂ T carries a weight ε^{d_v} where d_v = dist(v, v_T) is the depth of vertex v from the root of T.

              cutTotalDepth c computes the sum Σ d_v over all subtrees extracted by c. This is the load-bearing quantity for the Minimal Search cost function: c(M(α, β)) = depth(α) + depth(β) per M-C-B rule 5 (p. 59), and the cost of a single mergeOp call equals cutTotalDepth of the joint cut producing (α, β).

              The empty cut contributes 0 (no extractions). The non-empty cut on a node adds 1 (depth of immediate children) plus recursive contributions shifted by 1.

              Phase 7d (Minimal Search) consumes this for the weighted Merge operator M^ε and Proposition 1.5.1 (p. 60) — EM/IM are zero-cost; Sideward is positive-cost.

              Note: this captures only the EXTRACTION-side depth (positive contributions per M-C-B rule 1). Quotient depth (rule 2, with ε^{-d} weights) cancels the extraction depth in the IM composition; we don't track it separately here because the cancellation-aware ℕ cost function we'll build computes the final c(M) directly.

              source
              def ConnesKreimer.CutShape.cutTotalDepth {α : Type u_1} {β : Type u_2} {T : TraceTree α β} :
              CutShape T → ℕ

              The total depth of a cut: the sum, over all subtrees extracted by c, of the depth at which each subtree was extracted (= distance from the root of the source tree to the vertex where the cut occurred).

              For a cut on .node l r:

              • bothCut: extracts l and r each at depth 1 → total = 2.
              • onlyLeftCut hl cr: extracts l at depth 1, plus cr's extractions from inside r (each shifted +1) → 1 + (cutTotalDepth cr + |cutForest cr|).
              • onlyRightCut hr cl: symmetric.
              • bothRecurse cl cr: shifted contributions from both children.
              Equations
              Instances For

                §5.5.1: Sanity checks for cutTotalDepth #

                source
                @[simp]
                theorem ConnesKreimer.CutShape.cutTotalDepth_empty {α : Type u_1} {β : Type u_2} (T : TraceTree α β) :
                (empty T).cutTotalDepth = 0

                The empty cut has depth 0 (no extractions).

                source
                theorem ConnesKreimer.CutShape.cutTotalDepth_eq_zero_of_cutForest_eq_zero {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (h : c.cutForest = 0) :
                c.cutTotalDepth = 0

                A cut has depth 0 iff its cut-forest is empty (extracts nothing). Combined with cutForest_eq_zero_iff, this gives cutTotalDepth c = 0 ↔ c = empty T. The cost-weighted Minimal Search formalism uses this to characterize "no actual extraction" cases.

                source
                theorem ConnesKreimer.CutShape.eq_empty_of_cutTotalDepth_eq_zero {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                c.cutTotalDepth = 0 → c = empty T

                Converse: cutTotalDepth c = 0 forces c = empty T. The non-empty cut constructors all contribute strictly positive depth (extracting at least one subtree at depth ≥ 1).

                source
                theorem ConnesKreimer.CutShape.cutTotalDepth_eq_zero_iff {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                c.cutTotalDepth = 0 ↔ c = empty T

                The full characterization: cutTotalDepth c = 0 ↔ c = empty T.

                §6: Sanity checks #

                source
                @[simp]
                theorem ConnesKreimer.CutShape.cutForest_empty {α : Type u_1} {β : Type u_2} (T : TraceTree α β) :
                (empty T).cutForest = 0

                The empty cut extracts nothing.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.remainder_empty {α : Type u_1} {β : Type u_2} [Inhabited β] (T : TraceTree α β) :
                (empty T).remainder = T

                The empty cut leaves T unchanged.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.remainderDeletion_empty {α : Type u_1} {β : Type u_2} (T : TraceTree α β) :
                (empty T).remainderDeletion = some T

                The empty cut's deletion-remainder is some T — the whole tree, unchanged. Used by the algebraic Merge bridge's factor-out lemma to identify the empty-cut term in comulTreeDel T as 1 ⊗ forestToHc {T}.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.cutForest_bothCut {α : Type u_1} {β : Type u_2} {l r : TraceTree α β} (hl : l.IsNotTrace) (hr : r.IsNotTrace) :
                (bothCut hl hr).cutForest = {l, r}

                Cut both child edges of a node: extracts both children.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.cutForest_atLeaf {α : Type u_1} {β : Type u_2} {a : α} :
                atLeaf.cutForest = 0

                The unique cut on a leaf has empty cutForest.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.remainder_atLeaf {α : Type u_1} {β : Type u_2} [Inhabited β] {a : α} :
                atLeaf.remainder = TraceTree.leaf a

                The unique cut on a leaf leaves the leaf unchanged.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.cutForest_atTrace {α : Type u_1} {β : Type u_2} {b : β} :
                atTrace.cutForest = 0

                The unique cut on a trace has empty cutForest.

                source
                @[simp]
                theorem ConnesKreimer.CutShape.remainder_atTrace {α : Type u_1} {β : Type u_2} [Inhabited β] {b : β} :
                atTrace.remainder = TraceTree.trace b

                The unique cut on a trace leaves the trace unchanged.

                §6: Position vs. value: cutForest is NOT injective (and that's correct) #

                A natural question: is cutForest : CutShape T → TraceForest α β injective (per M-C-B Lemma 1.2.7's bijection)? The answer is no in general, and that's actually consistent with M-C-B.

                Counterexample: take T = .node X X (same subtree X on both sides). Then bothRecurse cl cr and bothRecurse cr cl are syntactically distinct CutShape T values but produce identical cutForest multisets (multiset addition is commutative). More generally, whenever subtrees on the left and right have shared substructure, swapping cut choices gives the same value-level multiset but distinct positional cut data.

                This is consistent with M-C-B because Eq (1.2.8)'s Σ_{F_v} ranges over positional subforests of disjoint accessible terms (per M-C-B's "disjoint in T" qualifier in Lemma 1.2.7), not over value- deduplicated multisets. Two positionally-distinct cuts that happen to extract the same value-multiset CONTRIBUTE TWO TERMS to the sum.

                Our Σ c : CutShape T correctly enumerates positionally — CutShape T is the positional cut data. The map cutForest then projects position to value; non-injectivity here corresponds to multiplicities in the value-multiset projection of the sum, which is exactly what M-C-B's sum is supposed to track.

                Bottom line: don't try to prove cutForest injective; the sum over CutShape is the right semantics, and value-level collisions are genuine multiplicity contributions.

                §7: IsNotTrace is preserved by remainder #

                For cl : CutShape l, remainder cl has the same top-level constructor as l (modulo .trace markers introduced for extracted children). In particular, IsNotTrace l holds iff IsNotTrace (remainder cl) holds — the only .trace- shaped tree's only CutShape is atTrace, whose remainder is the same .trace.

                source
                theorem ConnesKreimer.CutShape.isNotTrace_remainder_iff {α : Type u_1} {β : Type u_2} [Inhabited β] {l : TraceTree α β} (cl : CutShape l) :
                cl.remainder.IsNotTrace ↔ l.IsNotTrace

                IsNotTrace is preserved by remainder in both directions.

                source
                theorem ConnesKreimer.CutShape.isNotTrace_remainder {α : Type u_1} {β : Type u_2} [Inhabited β] {l : TraceTree α β} (cl : CutShape l) (h : l.IsNotTrace) :
                cl.remainder.IsNotTrace

                Forward direction: if l is not a trace marker, neither is its remainder after any cut.

                source
                theorem ConnesKreimer.CutShape.isNotTrace_of_isNotTrace_remainder {α : Type u_1} {β : Type u_2} [Inhabited β] {l : TraceTree α β} (cl : CutShape l) (h : cl.remainder.IsNotTrace) :
                l.IsNotTrace

                Backward direction: if remainder cl is not a trace marker, neither is l.

                §8: Δ^d leafCount conservation (M-C-B Def 1.6.2 + book p. 64 remark) #

                For any admissible cut c on T, the deletion-coproduct's two channels together account for all of T's leaves:

                c.cutForest.degForest + (deletionLeafCount c) = T.leafCount

                where deletionLeafCount c is (t.leafCount) if c.remainderDeletion = some t, else 0. This is M-C-B's degree-conservation observation (book p. 64, paragraph after Def 1.6.2): "the overall deg(F) = #L(F) of the workspace F ∈ 𝔉_{SO_0} is a conserved quantity throughout all the forms of Merge described by (1.3.7)."

                Load-bearing for the IM positive direction of Prop 1.6.10 (im_satisfiesNCL in Theories/Syntax/Minimalist/Merge/NoComplexityLoss.lean): the IM workspace transformation {T} → {.node Q β} preserves total leafCount because β.leafCount + Q.leafCount = T.leafCount for Q = T/β via this lemma.

                source
                def ConnesKreimer.CutShape.deletionLeafCount {α : Type u_1} {β : Type u_2} {T : TraceTree α β} :
                CutShape T → ℕ

                Total leafCount of the deletion-remainder, defined structurally on the cut. For each cut constructor, the remainder leaf count is computed directly: extracted leaves count as 1 (atLeaf/atTrace), edge contractions contribute 0 (bothCut), recursive cases pass through (only*Cut), and bothRecurse adds children's contributions.

                Equivalent to Option.elim 0 leafCount ∘ remainderDeletion but structurally tractable for proofs.

                Equations
                Instances For
                  source
                  theorem ConnesKreimer.CutShape.cut_leafCount_conservation {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                  c.cutForest.degForest + c.deletionLeafCount = T.leafCount

                  Δ^d analog of M-C-B's degree-conservation remark, book p. 64: the deletion-coproduct preserves total leafCount. For any cut c on T: c.cutForest.degForest + deletionLeafCount c = T.leafCount.

                  M-C-B (book p. 64, paragraph after Def 1.6.2): "Observe that the overall degree deg(F) = #L(F) of the workspace … is a conserved quantity throughout all the forms of Merge described by (1.3.7), as none of the lexical items originally in the workspace is ever removed."

                  Note: this is the leafCount (= #L) slice only. M-C-B's Lemma 1.6.3 (book p. 65) and Proposition 1.6.4 (book p. 66) concern α (accessible terms count) and σ (= b₀ + α), which are different counting functions and are NOT formalized here. Those would be needed for the Sideward NCL negative directions (per Remark 1.6.9, leafCount alone cannot distinguish Sideward 2(b) from IM).

                  Structural induction on the cut: each constructor's contribution balances out so the total leafCount is conserved.

                  source
                  theorem ConnesKreimer.CutShape.deletionLeafCount_eq_option_elim {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                  c.deletionLeafCount = c.remainderDeletion.elim 0 TraceTree.leafCount

                  Master bridge: the structural deletionLeafCount agrees with the Option.elim 0 leafCount of remainderDeletion. Both encode "leaves surviving in the deletion-quotient", but deletionLeafCount is structural (induction-friendly) while remainderDeletion is the actual Δ^d output (Option-valued).

                  source
                  theorem ConnesKreimer.CutShape.deletionLeafCount_eq_of_remainderDeletion_some {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (t : TraceTree α β) (h : c.remainderDeletion = some t) :
                  c.deletionLeafCount = t.leafCount

                  Corollary: when a cut has a non-trivial Δ^d remainder some t, the structural deletionLeafCount agrees with t.leafCount. The IM-NCL theorem in Theories/Syntax/Minimalist/Merge/NoComplexityLoss.lean uses this to identify Q.leafCount = deletionLeafCount c0 for c0.remainderDeletion = some Q.

                  §9: Δ^d size conservation (MCB Lemma 1.6.3 size analog) #

                  The size analog of cut_leafCount_conservation: for any admissible cut c on T,

                  T.size = c.cutForest.sizeForest + deletionSize c + numContractions c

                  where:

                  This generalizes the leafCount conservation (which is contraction-free because contractions only affect non-leaf vertices). The single-edge case (cutForest = {β_t}, remainderDeletion = some Q) yields T.size = β_t.size + Q.size + 1 (exactly 1 contraction at the immediate parent of the cut edge).

                  source
                  def ConnesKreimer.CutShape.numContractions {α : Type u_1} {β : Type u_2} {T : TraceTree α β} :
                  CutShape T → ℕ

                  Number of vertices lost to edge contraction in the Δ^d quotient. See §9 docstring for the per-constructor recursion.

                  Equations
                  Instances For
                    source
                    theorem ConnesKreimer.CutShape.cut_size_conservation {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                    T.size = c.cutForest.sizeForest + c.remainderDeletion.elim 0 TraceTree.size + c.numContractions

                    Δ^d size conservation (MCB Lemma 1.6.3 size analog, book p. 65). For any cut c on T, the source tree's vertex count decomposes as the sum of extracted-subtree vertices, deletion-remainder vertices, and contracted vertices. Structural induction; each cut constructor contributes a known number of contractions per the numContractions recursion.

                    Δ^c size conservation #

                    source
                    theorem ConnesKreimer.CutShape.cut_size_conservation_contraction {α : Type u_1} {β : Type u_2} [Inhabited β] {T : TraceTree α β} (c : CutShape T) :
                    T.nonTraceSize = T.size → T.size = c.cutForest.sizeForest + c.remainder.nonTraceSize

                    Δ^c size conservation (MCB Lemma 1.6.3 size analog for the contraction quotient, book p. 65). For any cut c on a trace-free T, the source tree's vertex count decomposes cleanly into extracted-subtree vertices plus the contraction-remainder's NON-TRACE vertex count:

                    T.size = c.cutForest.sizeForest + (c.remainder).nonTraceSize

                    The trace-free hypothesis is encoded as T.nonTraceSize = T.size — matching MCB's setup where syntactic objects in the workspace are trace-free; trace markers appear only in quotient trees.

                    No "contraction count" appears here — Δ^c preserves all parent vertices (they hold the trace markers). The trace markers in the remainder don't count toward nonTraceSize, exactly recovering the extracted subtrees' vertex bookkeeping.

                    Compare to cut_size_conservation for Δ^d which has an extra numContractions c term.

                    source
                    theorem ConnesKreimer.CutShape.nonTraceSize_eq_size_of_mem_cutForest {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (t : TraceTree α β) :
                    T.nonTraceSize = T.size → t ∈ c.cutForest → t.nonTraceSize = t.size

                    Trace-freeness propagates: any subtree extracted by a cut on a trace-free T is itself trace-free. Used by Δ^c counting to certify that extracted accessible terms (β_t) have accCountC = accCount.

                    source
                    theorem ConnesKreimer.CutShape.nonTraceSize_remainder_pos_of_node {α : Type u_1} {β : Type u_2} [Inhabited β] {l r : TraceTree α β} (c : CutShape (l.node r)) :
                    c.remainder.nonTraceSize ≥ 1

                    For a cut on a .node source tree, the contraction-remainder has nonTraceSize ≥ 1 (the root parent vertex is preserved as a .node, contributing 1 regardless of which child is replaced by .trace).

                    source
                    theorem ConnesKreimer.CutShape.isNode_of_cutForest_singleton {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) :
                    c.cutForest = {β_t} → ∃ (l : TraceTree α β) (r : TraceTree α β), T = l.node r

                    A cut with a singleton cutForest forces T to be a .node. (Leaf and trace roots have only the trivial empty cut, with cutForest = 0.) Useful for downstream proofs that need to use nonTraceSize_remainder_pos_of_node on a T introduced as TraceTree α β rather than .node l r syntactically.

                    source
                    theorem ConnesKreimer.CutShape.nonTraceSize_remainder_pos_of_cutForest_singleton {α : Type u_1} {β : Type u_2} [Inhabited β] {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) (h_cf : c.cutForest = {β_t}) :
                    c.remainder.nonTraceSize ≥ 1

                    Convenience wrapper: a cut with singleton cutForest has remainder.nonTraceSize ≥ 1 regardless of how T is syntactically introduced. Combines isNode_of_cutForest_singleton and nonTraceSize_remainder_pos_of_node.

                    source
                    theorem ConnesKreimer.CutShape.singleEdgeCut_contraction_alpha {α : Type u_1} {β : Type u_2} [Inhabited β] {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) (h_tf : T.nonTraceSize = T.size) (h_cf : c.cutForest = {β_t}) :
                    T.accCount = β_t.accCount + c.remainder.accCountC + 1

                    MCB Lemma 1.6.3 eq. 1.6.8 (book p. 65): for a single-edge cut on T extracting accessible term β_t, the contraction-quotient's accCountC satisfies α(T) = α(T_v) + α^c(T/^c T_v) + 1. The +1 accounts for the root vertex of T (counted in accCount T = T.size − 1 but not in the per-piece sum since the root is the new merged node when re-merging).

                    Concretely: T.size − 1 = (β_t.size − 1) + ((T/^c β_t).nonTraceSize − 1) + 1 follows from cut_size_conservation_contraction with cutForest = {β_t} and the size-pos witnesses.

                    source
                    theorem ConnesKreimer.CutShape.singleEdgeCut_contraction_sigma {α : Type u_1} {β : Type u_2} [Inhabited β] {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) (h_tf : T.nonTraceSize = T.size) (h_cf : c.cutForest = {β_t}) :
                    {T}.sigma = {β_t}.sigma + {c.remainder}.sigmaC

                    MCB Lemma 1.6.3 eq. 1.6.10 (book p. 65): σ(T) = σ(T_v) + σ(T/^c T_v) for a single-edge cut on T extracting β_t. (No +1 in this case — the root vertex is already counted in σ_v + σ_q via the b₀ contribution.)

                    Concretely: 1 + (T.size − 1) = (1 + (β_t.size − 1)) + (1 + ((T/^c β_t).nonTraceSize − 1)) follows from cut_size_conservation_contraction.

                    source
                    theorem ConnesKreimer.CutShape.remainderDeletion_ne_none_of_cutForest_singleton {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) :
                    c.cutForest = {β_t} → c.remainderDeletion ≠ none

                    Single-edge cut produces non-collapsing remainder: if a cut has a singleton cutForest = {β_t}, then its remainderDeletion is some _ (cannot be none). Contrapositive: a none remainder requires a .bothCut at some node, which contributes ≥ 2 elements to cutForest.

                    Proved by structural recursion on the tree (and case-analysis on the cut at each level), using eq_empty_of_cutForest_eq_zero to identify the empty subordinate cuts and remainderDeletion_empty to discharge them.

                    source
                    @[simp]
                    theorem ConnesKreimer.CutShape.numContractions_empty {α : Type u_1} {β : Type u_2} (T : TraceTree α β) :
                    (empty T).numContractions = 0

                    The empty cut contracts no vertices.

                    source
                    theorem ConnesKreimer.CutShape.cutForest_card_eq_numContractions_add {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) :
                    Multiset.card c.cutForest = c.numContractions + c.remainderDeletion.elim 1 fun (x : TraceTree α β) => 0

                    Vertex-accounting master equation (sharper bookkeeping at the cardinality layer; companion to cut_size_conservation at the size layer).

                    For any cut c : CutShape T, c.cutForest.card = numContractions c + (1 if rd = none, else 0).

                    Geometric reading: each cut edge contributes one extracted subtree to cutForest and one contracted parent vertex to numContractions. The root of T contributes an extra contraction precisely when the cut includes a .bothCut at the root (rd = none); when rd = some, the root survives into the deletion remainder.

                    Subsumes the legacy single-edge / two-edge contraction-count lemmas (numContractions_singleEdge, numContractions_twoEdge); both are restated below as 1-line omega corollaries.

                    source
                    theorem ConnesKreimer.CutShape.numContractions_eq_card_of_remainderDeletion_some {α : Type u_1} {β : Type u_2} {T : TraceTree α β} {c : CutShape T} {Q : TraceTree α β} (h_rd : c.remainderDeletion = some Q) :
                    c.numContractions = Multiset.card c.cutForest

                    Specialization of cutForest_card_eq_numContractions_add for the rd = some branch: numContractions c = c.cutForest.card.

                    source
                    theorem ConnesKreimer.CutShape.numContractions_succ_eq_card_of_remainderDeletion_none {α : Type u_1} {β : Type u_2} {T : TraceTree α β} {c : CutShape T} (h_rd : c.remainderDeletion = none) :
                    c.numContractions + 1 = Multiset.card c.cutForest

                    Specialization of cutForest_card_eq_numContractions_add for the rd = none branch: numContractions c + 1 = c.cutForest.card.

                    source
                    theorem ConnesKreimer.CutShape.numContractions_singleEdge {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (β_t : TraceTree α β) (h_cf : c.cutForest = {β_t}) :
                    c.numContractions = 1

                    A single-edge cut has exactly 1 contracted vertex: the parent of the cut edge. Corollary of numContractions_eq_card_of_remainderDeletion_some with cutForest.card = 1 and the singleton-implies-rd-some witness remainderDeletion_ne_none_of_cutForest_singleton.

                    source
                    theorem ConnesKreimer.CutShape.numContractions_twoEdge {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (Q : TraceTree α β) (h_card : Multiset.card c.cutForest = 2) (h_rd : c.remainderDeletion = some Q) :
                    c.numContractions = 2

                    Two-edge cut has exactly 2 contracted vertices (MCB Prop 1.6.8 case 3(a), book p. 70: "two edges are contracted, and hence the counting of (non-root) vertices decreases by 2"). Corollary of numContractions_eq_card_of_remainderDeletion_some with cutForest.card = 2.

                    source
                    theorem ConnesKreimer.CutShape.singleEdgeCut_size_relation {α : Type u_1} {β : Type u_2} {T : TraceTree α β} (c : CutShape T) (β_t Q : TraceTree α β) (h_cf : c.cutForest = {β_t}) (h_rd : c.remainderDeletion = some Q) :
                    T.size = β_t.size + Q.size + 1

                    Single-edge-cut size relation (MCB Lemma 1.6.3 size analog of eq. 1.6.7 / 1.6.9, book p. 65). For any cut c : CutShape T whose cutForest is the singleton {β_t} and whose remainderDeletion is some Q, the source tree T decomposes as T.size = β_t.size + Q.size + 1.

                    Geometric reading: a single edge cut splits T into the extracted accessible term β_t and the binarized deletion-quotient Q, plus the contracted parent vertex of the cut edge (the +1).

                    Corollary of cut_size_conservation with numContractions = 1 (single-edge case, by numContractions_singleEdge).

                    Used by MinimalYield.im_pair_size_deltas_deltaD and MinimalYield.sideward_2b_size_deltas_deltaD to discharge the h_size hypothesis from cut data.