The Flow Property of the Exact B-Series

The exact-flow B-series compose as a one-parameter group: B_h ∘ B_{h'} = B_{h+h'}, i.e.

convolution (scaledExact h) (scaledExact h') = scaledExact (h + h'),

by the flow identity for cuts. Consequently the exact solution's character is an odd character: the exact solution is a symmetric method (isOdd_toCharacter_exact), the fact underlying the order theory of symmetric components (arXiv:2507.21006, Section 7; Butcher; HLW III.1).

theorem BSeries.Series.convolution_scaledExact {R : Type u} [Field R] [CharZero R] (h h' : R) : (scaledExact h).convolution (scaledExact h') = scaledExact (h + h')

The flow property of the exact B-series: exact flows compose as a one-parameter group, B_h ∘ B_{h'} = B_{h+h'} (Butcher; HLW III.1).

theorem BSeries.Series.convolution_exact_neg {R : Type u} [Field R] [CharZero R] : (exact R).convolution (scaledExact (-1)) = unit R

The exact flow composed with its time-reversal is the identity.

theorem BSeries.Series.convolution_neg_exact {R : Type u} [Field R] [CharZero R] : (scaledExact (-1)).convolution (exact R) = unit R

theorem BSeries.Series.involution_toCharacter_exact {R : Type u} [Field R] [CharZero R] : ForestAlgebra.Character.involution (exact R).toCharacter = (scaledExact (-1)).toCharacter

The canonical involution of the exact character is the time-reversed exact flow.

theorem BSeries.Series.isOdd_toCharacter_exact {R : Type u} [Field R] [CharZero R] : ForestAlgebra.Character.IsOdd (exact R).toCharacter

The exact solution of an ODE is a symmetric method: its B-series character is an odd character (arXiv:2507.21006, Section 7, a = a*).

theorem BSeries.Series.adjointCharacter_agree_exact {R : Type u} [Field R] [CharZero R] {χ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ.evalForest φ = (exact R).toCharacter.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n → (ForestAlgebra.Character.adjointCharacter χ).evalForest φ = (exact R).toCharacter.evalForest φ

The adjoint preserves the order of a B-series method: if a character agrees with the exact solution up to order n, so does its adjoint (arXiv:2507.21006, Proposition 7.1(1), one direction).

theorem BSeries.Series.adjointCharacter_agree_exact_iff {R : Type u} [Field R] [CharZero R] (χ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) : (∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ.evalForest φ = (exact R).toCharacter.evalForest φ) ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → (ForestAlgebra.Character.adjointCharacter χ).evalForest φ = (exact R).toCharacter.evalForest φ

A method and its adjoint have the same order: ord(ψ) = ord(ψ*) (arXiv:2507.21006, Proposition 7.1(1)).

theorem BSeries.Series.adjointCharacter_evalForest_congr {R : Type u} [Field R] {χ ξ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ.evalForest φ = ξ.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n → (ForestAlgebra.Character.adjointCharacter χ).evalForest φ = (ForestAlgebra.Character.adjointCharacter ξ).evalForest φ

Order-agreement transports through the adjoint.

theorem BSeries.Series.adjointCharacter_evalForest_congr_pair {R : Type u} [Field R] {χ ξ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ.evalForest φ = ξ.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n → (ForestAlgebra.Character.adjointCharacter χ).evalForest φ = (ForestAlgebra.Character.adjointCharacter ξ).evalForest φ

Order-agreement between two characters transports through the adjoint.

theorem BSeries.Series.convolution_evalForest_congr {R : Type u} [Field R] {χ₁ χ₂ ξ₁ ξ₂ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h₁ : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ₁.evalForest φ = ξ₁.evalForest φ) (h₂ : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ₂.evalForest φ = ξ₂.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n → (χ₁.convolution χ₂).evalForest φ = (ξ₁.convolution ξ₂).evalForest φ

Order-agreement transports through character convolution.

theorem BSeries.Series.symmetricPart_agree_exact {R : Type u} [Field R] [CharZero R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → ψ.evalForest φ = (exact R).toCharacter.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n → (ForestAlgebra.Character.symmetricPart ψ) (HopfAlgebras.ForestAlgebra.ofForest φ) = (exact R).toCharacter.evalForest φ

The symmetric component of a method has at least the order of the method: if ψ agrees with the exact solution up to order n, so does ψ⁻ (arXiv:2507.21006, Propositions 7.1(3) and 7.2).

theorem BSeries.Series.convolution_evalForest_boundary_split {R : Type u} [Field R] (χ₁ χ₂ : HopfAlgebras.ForestAlgebra.Character R) {τ : HopfAlgebras.RootedForest} (hτne : τ ≠ 0) : (χ₁.convolution χ₂).evalForest τ = χ₂.evalForest τ + χ₁.evalForest τ + (List.map (fun (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => χ₁.evalForest term.1 * χ₂.evalForest term.2) (List.filter (fun (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => decide (0 < term.1.order ∧ 0 < term.2.order)) τ.coproductTerms)).sum

Splitting a character convolution at the two boundary cuts.

theorem BSeries.Series.adjointCharacter_eval_first_defect {R : Type u} [Field R] [CharZero R] {ψ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → ψ.evalForest φ = (exact R).toCharacter.evalForest φ) {τ : HopfAlgebras.RootedForest} (hτ : τ.order = n + 1) : (ForestAlgebra.Character.adjointCharacter ψ).evalForest τ - (exact R).toCharacter.evalForest τ = (-1) ^ n * (ψ.evalForest τ - (exact R).toCharacter.evalForest τ)

The adjoint's defect at the first failing order: if ψ agrees with the exact solution up to order n, then at order n + 1 the adjoint's defect is (-1)^n times the defect of ψ (arXiv:2507.21006, Section 7).

theorem BSeries.Series.symmetricPart_eval_first_defect {R : Type u} [Field R] [CharZero R] [Invertible 2] {ψ : HopfAlgebras.ForestAlgebra.Character R} {n : ℕ} (hn : Even n) (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → ψ.evalForest φ = (exact R).toCharacter.evalForest φ) {τ : HopfAlgebras.RootedForest} (hτ : τ.order = n + 1) : (ForestAlgebra.Character.symmetricPart ψ) (HopfAlgebras.ForestAlgebra.ofForest τ) = ψ.evalForest τ

The symmetric component detects the leading defect: if ψ agrees with the exact solution up to an even order n, then at order n + 1 the symmetric component takes the same values as ψ itself. In particular a method of order exactly n (with n even) has symmetric component of order exactly n (arXiv:2507.21006, Section 7).

theorem BSeries.Series.isOdd_agree_exact_succ {R : Type u} [Field R] [CharZero R] {χ : HopfAlgebras.ForestAlgebra.Character R} (hodd : ForestAlgebra.Character.IsOdd χ) {n : ℕ} (hn : Odd n) (h : ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → χ.evalForest φ = (exact R).toCharacter.evalForest φ) (φ : HopfAlgebras.RootedForest) : φ.order ≤ n + 1 → χ.evalForest φ = (exact R).toCharacter.evalForest φ

Symmetric methods have even order, in step form (Hairer–Nørsett–Wanner, Theorem II.8.10; arXiv:2507.21006, Section 8): if a symmetric (odd) character agrees with the exact solution up to an odd order n, the agreement extends automatically to order n + 1. Hence the finite order of a symmetric B-series method is always even.