Linear carbon-cycle impulse responses: post-cessation monotonicity, certified peak delays, and two concentration maxima from a single emission hump (a model result; the unimodality theory is classical)

We study the linear impulse-response model u(t) = ∫0t m(z) h(t−z) dz with the Joos et al. (2013) multi-model-mean IRF h(t) = a0 + Σ ai e−t/τi, for nonnegative emission paths m. “Concentration” always means the model excess u; nothing is said about the real atmosphere. (a) After emissions cease, u is completely monotone (non-increasing, convex) with limit a0∫m: hand proof for continuous m (Tier C), Lean proof for discrete nonnegative emission measures only (Tier A, statement lock owed). (b) Interval-arithmetic enclosures of the time of the concentration maximum and its delay for Seshadri's emission family in 63 scenarios (Tier C; global uniqueness of each peak is Tier X). (c) For every completely monotone, strictly decreasing IRF that is not a single exponential (in particular the Joos IRF), single-humped emission paths exist for which u has two local maxima separated by a strictly lower value: an explicit staircase window B/A in (h(d), L) is proved necessary and sufficient within the family (Tier C), and three Joos instances are certified with exact rationals and interval arithmetic, one for a strictly unimodal emission path. The mechanism is classical. It follows from Ibragimov's 1956 theorem on strong unimodality (convolution preserves unimodality iff the kernel is log-concave), which we read only from secondary sources; the single exponential is its log-concave special case. What is added is the explicit window, the certified Joos instances and the carbon-cycle framing. To our knowledge (not a systematic search) no carbon-cycle paper states it. What this is NOT. Not a statement about the real (nonlinear, state-dependent) carbon cycle, not about realistic emission pathways, tonnes, warming or policy, and not a new phenomenon class. The Joos fit is valid for 0–1000 yr only; the limit a0W and a 0–6000 yr scan describe the fitted formula beyond that range. Limitations. Independently audited by a different AI agent instance (AUDIT.md, ACCEPT_WITH_CORRECTIONS, twelve corrections applied); no human audit and no statement lock (owed). Unverified: global peak uniqueness (float scans), the float maps and three-maximum cases in (c), Ibragimov's original text, the systematic literature search, the ordering of the preregistration (hash matches). Not in Lean: continuous emissions, the single-exponential and staircase theorems, part (b). The Elenchus ledger gate exits with code 1 (0 blocking findings, 2 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row).