# Sequentialization formalization comparison Review date: 2026-07-21 ## Primary evidence added The local generated exposition is not sufficient authority for a library-level sequentialization theorem. The implementation plan is now cross-checked against: - Danos and Regnier, *The Structure of Multiplicatives*, Archive for Mathematical Logic 28, 181-203 (1989), DOI ; - Di Guardia and Laurent, *A Formalization of Multiplicative Proof-Nets in Rocq*, TLLA 2025, ; - the corresponding Rocq development, , reviewed locally at commit `9b582a53c4c9c94013146d2c749597dada9edf96` under its LGPL license; - Straßburger, *Proof Nets and the Identity of Proofs*, INRIA RR-6013 / arXiv `cs/0610123`, . The upstream source is a proof reference, not code to copy into this MIT repository. Any implementation here must be independently written and must state the representation translation it proves. ## Representation mismatch | Dimension | ProofNet-IR | Rocq `proofnet_mll` | |---|---|---| | Graph vertices | formula occurrences | rule and conclusion vertices | | Graph edges | axiom/tensor/par incidence edges between occurrences | formula-labeled directed edges | | Premise order | explicit link fields | edge-side labels and graph properties | | Conclusions | occurrence indices | an order list containing every conclusion edge once | | Cuts | absent | represented and sequentialized | | Correctness implementation | explicitly enumerate each par switching and test its undirected tree | colored-path formulation on one multigraph | | Sequentialization result | first-order tree whose desequentialization is `ProofNetEquivalent` to the input | a sequent proof whose desequentialization is graph-isomorphic to the input | The two correctness presentations are mathematically related, but the Rocq theorem cannot simply be restated for the Lean structure. In particular, the target theorem must use an explicit occurrence-preserving isomorphism or reindexing relation; literal certificate equality is too strong. ## Upstream proof architecture The reviewed Rocq development separates the argument into: 1. graph/path and finite multigraph lemmas; 2. proof-structure and correctness definitions; 3. desequentialization and proof that every sequent derivation gives a net; 4. existence of a terminal splitting vertex, using a generalized Yeo theorem; 5. inverse cases for axiom, par, tensor, and cut vertices; 6. well-founded recursion on graph edge count; 7. a final dependent result containing a sequent proof and an isomorphism from its desequentialization to the original proof net. Its final theorem has the essential shape "for every proof net `G`, there is a linear-logic proof `p` whose proof structure is isomorphic to `G`". This confirms that isomorphism is part of the correctness statement, not merely a serialization convenience. ## Lean implementation obligations The representation-specific general-sequentialization checklist is: 1. define certificate reindexing and an equivalence/isomorphism relation that preserves formulas, ordered tensor/par premises, conclusions, and axiom pairing while quotienting semantically irrelevant link storage order; 2. prove the checker and declarative correctness predicates invariant under that relation; 3. keep derivation-first soundness and reverse sequentialization distinct: successful inference denotes a kernel derivation, while reverse sequentialization proves the generated tree's output equivalent to the accepted input; 4. define terminal par and splitting tensor decomposition for the current occurrence graph; 5. prove each decomposition preserves proof-net correctness for its subnets; 6. prove a correct non-axiom net has an admissible terminal decomposition; 7. recurse on a strict size measure and return a first-order derivation together with an equivalence to the original certificate. Items 1-7 are now kernel checked for the supported unit-free, cut-free MLL representation. The exact generalized-Yeo and reconstruction evidence is recorded in [splitting-theorem-audit.md](splitting-theorem-audit.md). These obligations replace the earlier informal plan of simply "finding a splitting tensor". Their completion establishes the mathematical reverse theorem; it does not by itself satisfy the separate engineering and empirical requirements for a mature library. ## Current implementation checkpoint `ProofNetIR/Reindex.lean` establishes bounded vertex-renaming invariance and the narrower `ReindexEquivalent` relation. v0.3.1 proves its normal form is an in-class representative and a complete invariant for structurally well-formed certificates. This relation intentionally preserves link-list order. `ProofNetIR/NetEquivalence.lean` closes the additional identity boundary needed by sequentialization. `LinkPermutationEquivalent` keeps formula occurrences, ordered conclusions, axiom pairing, and ordered connective premises fixed but allows the link list to be permuted. Lean transports every independent par choice to a permuted selection and proves the corresponding switching graphs have the same tree property. `ProofNetEquivalent` is the equivalence generated by vertex renaming and link permutation, and preserves structural, declarative, and executable correctness. This broader relation is now the sequentialization target: desequentialization emits links in rule-tree postorder, whereas the checker correctly treats their storage order as irrelevant. It still does not quotient conclusion order or logical premise order, and it is not arbitrary unlabeled graph isomorphism.