Unit-free multiplicative proof nets

The calculus ${\mathsf{MLL}}^{-}$ of chapter 40 is classical, one-sided, and unit-free. Formulas have only named literals, tensor, and par; negation is the displayed involution; sequents are finite multisets. Identity links are atomic. Proof structures are formula-occurrence forests with a perfect dual-leaf matching. There is no unit, additive, exponential, box, quantifier, mix rule, generalized axiom, noncommutative order, or geometry-of-interaction dynamics.

Danos–Regnier correctness means that every correction graph is connected and acyclic. Rule preservation is lemma 40.8; translation soundness is theorem 40.9. The chapter next proves subnet existence, the empire boundary calculation, the tensor-kingdom identity, the kingdom order, and the splitting lemma. These are lemma 40.11–lemma 40.16. They yield sequentialization, with literal side conclusions, in theorem 40.17. All these proofs are local.

Cut links retain both incident edges. The exact two local contractions are compound tensor/par decomposition and atomic axiom–cut–axiom splicing. Local proofs establish correctness preservation, lexicographic strong normalization, and local confluence in lemma 40.23, lemma 40.24, lemma 40.26. Newman’s lemma gives confluence and a unique cut-free occurrence-graph normal form in theorem 40.28. Every complete reduction satisfies the explicit $c+2m$ step bound of corollary 40.25. Translating a sequent derivation to a cut net, normalizing, and sequentializing yields the sequent-calculus cut-elimination corollary corollary 40.29. The theorem is not stated for units, MALL, MELL, boxes, or other classical proof-net signatures.

The direct bit-vector/DFS checker is proved extensionally correct in proposition 40.19; its bound is $O(2^{k}n)$ time and $O(n+k)$ space, with a matching accepted-family lower bound for that implementation. The only imported theorem is Guerrini’s linear-time correctness and sequentialization result for nonredundantly represented unit-free multiplicative proof structures without constants, as stated and sourced in theorem 40.20. No linear bound is claimed for the direct enumerator.

Phase ordering and invariance under independent rule permutations are proved locally in definition 40.31, lemma 40.32. The exact cut-free quotient theorem is theorem 40.34. Straßburger’s Theorem 2.2.3 supplies only the historical commuting-conversion formulation identified in the chapter. The intuitionistic structural focused calculus treated in the preceding chapter is not translated into these classical linear nets.

The pinned Kappa supplement recorded in appendix E implements the direct switching enumerator and a reverse sequentializer. Its stable-ID corpus contains the correct, cyclic, disconnected, four-par positive, and last-switch-only cyclic structures, with exact rejection counts and reasons. The program does not implement Guerrini’s sequential-unification algorithm or the chapter’s cut vertices and reductions, and proves none of the local or imported metatheorems above.

Straßburger, Sections 2.1, 2.2, 2.5, and 2.7, arXiv:cs/0610123 PDF pp. 5–38, supplies the audited calculus, criterion, historical proof shape, and cut reductions. Guerrini, Definitions 1–4 and Theorem 5 on proceedings pp. 455–456 and Section 5.5/Theorem 15 on proceedings p. 462, supplies the linear algorithmic boundary. The connected-acyclic criterion is attributed to Danos and Regnier, but no theorem is imported from an uninspected original paper.