λ-Cert: A Linear Calibration Budget Rules Out a Pipeline's Certificate Before Any Data Is Collected

Conformal calibration certifies one stage of an LLM pipeline, but a deployer needs the guarantee for the whole composition, and reusing calibration data across stages inflates the family-wise error unless it is accounted for. λ-Cert is a type-and-effect discipline whose typing judgment carries per-stage certificates: a linear calibration budget makes such reuse unrepresentable, the effect sums the risk-bearing leaves, and a well-typed feed-forward pipeline satisfies $\mathrm{Pr}[R(e)\le {\alpha }_{\mathrm{top}}]\ge 1-{\delta }_{\mathrm{tot}}$ with no end-to-end recalibration. No prior compositional risk-control result we know of has a mechanized composition step: Rocq checks with no axioms that typing and the union bound give $\mathrm{Pr}[R(e)\le a]\ge 1-{\sum }_i{\delta }_i$ at natural-number levels $a$, with the per-node bounds and per-stage certificates as hypotheses; the budget step ${\sum }_i{\delta }_i\le {\delta }_{\mathrm{tot}}$ is proved on paper. An impossibility result marks the scope: for closed loops whose deployment law moves with the selected threshold, no static calibrator meeting a utility floor holds the target, and a pair of such dynamics, each certifiable alone, exists. From the budget arithmetic alone, before any calibration data is collected, the discipline rules out 20 of 64 pipeline configurations. On Qwen2.5 and Qwen2.5-VL over four benchmarks, certificates hold where the confidence signal separates and are declined where it does not, and two further generations reproduce fourteen of the sixteen verdicts. Typing certifies a dependent chain from its two leaf certificates without an end-to-end pass, at a looser bound than an exact end-to-end bound computed from the labels on a fixed-threshold version of the same pipeline, with the typed leaf levels fixed in advance, and only where the recalibrated downstream leaf certifies. The correction costs coverage and certification power rather than validity: in a 3,000-split replication over the same configurations, the uncorrected family-wise error on the test-fold proxy is significantly above its target in one cell, which the corrected condition violates as well.