Documentation

Linglib.Syntax.Minimalist.Merge.MinimalYieldPsi

The intermediate-derivation character ψt and Sideward detection (MCB Cor. 3.5.4) #

[MCB25] §3.5.2.2, eq. (3.5.7)

The character ϕt of Prop. 3.5.3 only weights the complete construction L(T) → T, whose grading is always ≥ 0 (MCB Lemma 3.5.5) — so ϕt is nonpolar and cannot detect Sideward Merge. Cor. 3.5.4 introduces

ψt(T) = Σ_{(F,F') ∈ FT} (F → F') · t^{δ(F→F')},

summing over all intermediate derivation pairs (F, F') in the construction of T (forests with L(F) = L(F') = L(T) lying on some chain L(T) → ⋯ → F → ⋯ → F' → ⋯ → T). Since δ depends only on the endpoints (δb₀(F→F') = b₀ F − b₀ F', etc.), each segment contributes a single grading monomial.

This file is the lean t-grading model of ψt, parameterized by the multiset of intermediate segments S (the full FT-enumeration engine — derivation reachability for a target — is deferred; here S is the input). The essential content of Cor. 3.5.4 — and the reason ψt succeeds where ϕt fails — is captured by polarHahn_psiSeries: the polar (divergent) part of ψt is exactly the sum over its Sideward-divergent segments (δb₀ < 0, where b₀ increases — MCB's Sideward types 3(a)/3(b)). A single Sideward segment already makes ψt polar (polarHahn_psiSeries_sideward_3a), which the Birkhoff factorization then renormalizes away (Core/Algebra/RootedTree/BirkhoffLaurent).

Main definitions #

References #

[MCB25] (Cor. 3.5.4, eq. 3.5.7; Lemma 3.5.5; Prop. 3.5.6)

source
@[reducible, inline]
abbrev Minimalist.Merge.Segment (α : Type u_4) (β : Type u_5) :
Type (max u_5 u_4)

A workspace transformation (intermediate derivation segment) F → F'.

Equations
Instances For
    source
    noncomputable def Minimalist.Merge.psiSeries {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (S : Multiset (Segment α β)) :
    LaurentSeries R

    ψt in the lean t-grading model (MCB eq. 3.5.7, δ = δb₀): a graded sum Σ tᵟ over the multiset S of intermediate derivation segments of a target.

    Equations
    Instances For
      source
      @[simp]
      theorem Minimalist.Merge.psiSeries_zero {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] :
      psiSeries 0 = 0
      source
      @[simp]
      theorem Minimalist.Merge.psiSeries_cons {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (p : Segment α β) (S : Multiset (Segment α β)) :
      psiSeries (p ::ₘ S) = gradeMonomial (δb₀ p.1 p.2) + psiSeries S
      source
      @[simp]
      theorem Minimalist.Merge.psiSeries_singleton {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (p : Segment α β) :
      psiSeries {p} = gradeMonomial (δb₀ p.1 p.2)
      source
      @[simp]
      theorem Minimalist.Merge.psiSeries_add {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (S T : Multiset (Segment α β)) :
      psiSeries (S + T) = psiSeries S + psiSeries T

      The polar part of ψt is exactly the divergent (Sideward) segments #

      source
      theorem Minimalist.Merge.polarHahn_psiSeries {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (S : Multiset (Segment α β)) :
      (psiSeries S).polarHahn = psiSeries (Multiset.filter (fun (p : Segment α β) => δb₀ p.1 p.2 < 0) S)

      The polar (divergent) part of ψt (MCB §3.5.2.2): R·ψt is the sum of grading monomials over exactly the Sideward-divergent segments (δb₀ < 0, i.e. b₀ increases). The polar part detects Sideward Merge — the property ϕt lacks (Lemma 3.5.5).

      source
      theorem Minimalist.Merge.polarHahn_psiSeries_eq_zero {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (S : Multiset (Segment α β)) (h : ∀ p ∈ S, 0 ≤ δb₀ p.1 p.2) :
      (psiSeries S).polarHahn = 0

      If every intermediate segment respects no-divergence (δb₀ ≥ 0), then ψt is nonpolar — the ϕt-like case (a construction using only External/Internal Merge).

      source
      theorem Minimalist.Merge.psiSeries_sub_polarHahn {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (S : Multiset (Segment α β)) :
      psiSeries S - (psiSeries S).polarHahn = psiSeries (Multiset.filter (fun (p : Segment α β) => ¬δb₀ p.1 p.2 < 0) S)

      The nonpolar projection (1 − R)·ψt keeps exactly the non-divergent segments (δb₀ ≥ 0 — the External/Internal/Minimal-Yield-respecting derivations). At the level of a single target's series this projection already separates the good derivations from the Sideward-divergent ones; the subtlety MCB Prop. 3.5.6 addresses is that 1 − R fails to do this on the character level (products of series), where the full Birkhoff factorization is needed because R is not an algebra homomorphism.

      source
      theorem Minimalist.Merge.polarHahn_psiSeries_sideward_3a {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommRing R] (T_i Tnode T_iq : RootedTree.Nonplanar (α ⊕ β)) :
      (psiSeries {({T_i}, {Tnode, T_iq})}).polarHahn = gradeMonomial (-1)

      A single Sideward 3(a) segment already makes ψt polar (δb₀ = −1): its whole value is the divergent monomial t⁻¹. This is the contrast with ϕt (always nonpolar) — ψt sees the Sideward Merge, which the Birkhoff factorization then removes.