Composition refusal (Python registry.compose)

General composition of holonomic generators is not a closure operation. The counterexample is exp ∘ exp: both factors are order-1 holonomic (f' - f = 0), yet exp(exp x) is not D-finite.

Axiom boundary

Mathlib v4.31 has no Stanley root-growth theorem linking Bell numbers to the Taylor series of exp ∘ exp. The single named axiom below records that analytic fact; theorems cite it explicitly. There is no silent sorry.

All Python self-test residual certificates (including sum and mixed product) are proved in HolonomicInstances.

inductive ISAR.ComposeOutcome : Type

Outcome of a requested composition, mirroring Python registry.compose.

• impossible (proof : String) : ComposeOutcome

def ISAR.instReprComposeOutcome.repr : ComposeOutcome → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ISAR.instReprComposeOutcome : Repr ComposeOutcome

Equations

• ISAR.instReprComposeOutcome = { reprPrec := ISAR.instReprComposeOutcome.repr }

def ISAR.composeRefuse : ComposeOutcome

Structured refusal returned by the composition interface.

Equations

• ISAR.composeRefuse = ISAR.ComposeOutcome.impossible "Composition of holonomic generators is not closed in general (counterexample: exp ∘ exp; Bell/Stanley obstruction)."

def ISAR.compose (_outer _inner : HolonomicCertificate) : ComposeOutcome

The registry composition operation always refuses in the general case.

Equations

• ISAR.compose _outer _inner = ISAR.composeRefuse

theorem ISAR.compose_refuses_in_general (c₁ c₂ : HolonomicCertificate) : compose c₁ c₂ = composeRefuse

Sole analytic axiom for composition obstruction

axiom ISAR.exp_exp_not_holonomic : ¬IsHolonomic fun (x : ℝ) => Real.exp (Real.exp x)

Direct non-holonomicity of exp ∘ exp.

Content (classical analysis): the Taylor coefficients of exp(exp x) at 0 involve Bell numbers whose root growth diverges, so by Stanley’s criterion the function is not D-finite / holonomic. Mathlib does not yet contain this chain; we import the conclusion as one named axiom. No Mathlib Bell-number / D-finiteness criterion is available to sketch a proof from; the axiom stays named.

Proved interface facts

theorem ISAR.exp_exp_factors_holonomic : IsHolonomic Real.exp ∧ IsHolonomic Real.exp

Both factors of the composition counterexample are holonomic.

theorem ISAR.holonomic_compose_would_imply_exp_exp (H : ∀ (f g : ℝ → ℝ), IsHolonomic f → IsHolonomic g → IsHolonomic (f ∘ g)) : IsHolonomic fun (x : ℝ) => Real.exp (Real.exp x)

If holonomic functions were closed under composition, then exp ∘ exp would be holonomic. Combined with exp_exp_not_holonomic, this yields the general refusal.

theorem ISAR.holonomic_not_closed_under_compose : ¬∀ (f g : ℝ → ℝ), IsHolonomic f → IsHolonomic g → IsHolonomic (f ∘ g)

General composition closure is impossible: it would contradict exp_exp_not_holonomic.

theorem ISAR.compose_impossibility_package : IsHolonomic Real.exp ∧ IsHolonomic Real.exp ∧ (¬IsHolonomic fun (x : ℝ) => Real.exp (Real.exp x)) ∧ ∀ (c₁ c₂ : HolonomicCertificate), compose c₁ c₂ = composeRefuse

Python compose_is_provably_impossible_in_general evidence package.