{"id":"50391c06-6e01-429e-bcab-634c9ab6b4a2","arxiv_id":"2607.11216","paper_version":1,"verdict":"ACCEPT","confidence":"HIGH","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"DH-CCS achieves spatial compositionality for quantum process calculi by representing states with named Deutsch-Hayden descriptors that split and merge without losing entanglement.","lead":"A new quantum process calculus (DH-CCS) uses adapted Deutsch-Hayden descriptors so each process can evolve its own qubits in isolation and the pieces can still be reassembled into the full entangled state. This spatial compositionality finally lets formal methods treat distributed quantum systems modularly and model open systems that entangle with the outside world.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified to the spatial-compositionality claim.","rationale":"The reader correctly isolates the paper’s strongest technical contribution and correctly flags that Theorem 22 is the most delicate supporting lemma. That lemma, however, is used only for the validity side-conditions of observer bisimulation (Definition 20, clause 4) and for the open-system security argument of Proposition 27; it is not an assumption of the compositionality theorem. Because the SOS rules never inspect descriptor contents beyond domain/support bookkeeping, compositionality holds even for stores that fail the Pauli equations. The paper is therefore internally consistent on its central claim, and the honest limitations it already states (gauge freedom, density-matrix fallback for information flow, omission of classical control) do not create a load-bearing hole in Theorem 15. The reader’s ACCEPT verdict with high confidence therefore needs no adjustment; the only refinement is that the weakest-assumption concern is real but orthogonal to the strongest claim.","tokens_in":29749,"tokens_out":529,"duration_ms":5246,"concrete_test":"Independently re-derive the unitary-update and Comm cases of the induction for Theorem 15, confirming that f_U(ρ)† ρ f_U(ρ) and the split/merge of a c!q / c?q pair both preserve the invariant “global store = union of the two local stores” without any extra global data. If either case requires information beyond the final local stores, the claim fails; otherwise it stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim (Theorem 15 / Definition 14) is that restriction and union of nominal DH stores give a partition/recomposition pair making DH-CCS spatially compositional. Once the representation of Section 3 is fixed, the proof is a routine induction on the SOS rules of Figure 2; the only non-trivial supporting result is Descriptor Completion (Theorem 22), which the paper uses for physical-validity checks in the observer bisimulation rather than for the compositionality statement itself. The Pauli equations are preserved by every transition that mutates a store (unitary update, split, merge), and the paper already notes that the calculus runs on unphysical stores. Consequently the reader’s weakest-assumption concern does not undermine Theorem 15. No internal inconsistency, missing case, or hidden global-state dependence appears in the argument for spatial compositionality.","agreement_with_reader":"partial"},"referee_report":{"model":"grok-4.5","summary":"The paper introduces DH-CCS, a quantum process calculus based on adapted Deutsch-Hayden (DH) descriptors. Its central claim is spatial compositionality: a global configuration ⟨P∥Q, ρ⟩ partitions into local views ⟨P, ρ|FV(P)⟩ and ⟨Q, ρ|FV(Q)⟩ that evolve independently under the SOS rules; the evolved stores recompose by union to recover the joint store (Definition 14, Theorem 15). Messages carry full single-qubit descriptor fragments rather than mere names. The paper supplies a physics-motivated observer equivalence (Definition 20) together with a subject bisimulation whose soundness proof exploits compositionality (Proposition 24), and illustrates open-system modelling on a BB84 fragment while noting that information-flow arguments still require density matrices.","tokens_in":29978,"tokens_out":689,"duration_ms":21448,"significance":"Spatial compositionality has been a persistent obstacle for quantum process calculi that rely on monolithic state vectors or density matrices. If the construction is sound, DH-CCS supplies the first modular state representation that preserves entanglement information under arbitrary split and merge, enabling process-local reasoning and true open-system interaction with external entanglement. The careful derivation of observer equivalence from continuous density-matrix monitoring and the Pauli equations, the algebraic completion theorem (Theorem 22), and the simplification of bisimulation soundness are genuine technical strengths. The BB84 case study demonstrates concrete utility for tracking qubit ownership across process and system boundaries. These contributions are of clear interest to the quantum concurrency and formal-methods communities.","major_comments":[],"minor_comments":[{"comment":"Section 2 title and several later occurrences write “Deutsch-Haynes”; the standard spelling is Hayden.","section":null},{"comment":"Example 3 contains the typo “Hamadard” for Hadamard.","section":null},{"comment":"Figure 1 and the surrounding text introduce both !!x.P / ??x.P and the env-process encoding; a short clarifying sentence that the two presentations are intentionally equivalent would help readers.","section":null},{"comment":"In Definition 13 the interaction set I is defined by a recursive case analysis; an explicit remark that the first matching clause wins would remove any ambiguity about overlapping patterns.","section":null},{"comment":"Section 8’s security argument for the “no external mention” case is clear, but a one-sentence pointer to the precise density-matrix reduction used for the complementary case would make the hybrid reasoning strategy more self-contained.","section":null}],"recommendation":"accept","confidential_remarks":"The manuscript is a solid, self-contained contribution that fits the journal’s scope. The central technical development is definitional and proof-theoretic; I see no hidden circularity or parameter fitting. The decision to omit classical control is openly discussed and does not undermine the compositionality claim. I recommend acceptance with only light copy-editing."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"The real news is that Inoue finally gives quantum process calculi a state representation that can be split and merged along process boundaries without losing entanglement information. Prior work (qCCS, CQP, lqCCS, etc.) all kept a monolithic density matrix or state vector and only shipped qubit names; messages here carry actual local DH-descriptor fragments, and independent local evolutions recompose by simple union (Theorem 15). That is the technical departure, and it is cleanly executed.\n\nWhat works: the adaptation of Deutsch-Hayden descriptors to named, splittable stores (Section 3) is careful; the SOS rules are standard once the representation is fixed; the compositionality proof is a routine induction; Descriptor Completion (Theorem 22) uses ordinary algebra (Skolem-Noether + polar decomposition) and is used only for the validity side-conditions of the observer bisimulation, not for the main claim. The BB84 fragment shows the open-system modelling payoff without overselling it. The paper is also unusually honest about the remaining gauge freedom and the fact that information-flow arguments still need density matrices.\n\nSoft spots are real but proportionate. Classical control is omitted (acknowledged); the observer equivalence is a bit heavy; and the Pauli-equation completeness assumption is load-bearing for physical-validity checks, though the stress-test is right that it does not touch Theorem 15 itself. No circularity, no free parameters, citations look normal for the subfield.\n\nThis is for people who already care about quantum process calculi or modular open-system reasoning. It is not a broad quantum-information paper, but inside its niche it is the first clean solution to a recognised obstacle. I would send it to referees; the core construction deserves a careful look. Worth engaging if you work on formal methods for quantum protocols.","headline":"Solid, non-incremental fix for the missing spatial compositionality in quantum process calculi; the math checks out and the limitations are stated honestly.","tokens_in":30547,"tokens_out":449,"would_cite":true,"duration_ms":6460,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"A quantum process calculus can split entangled system state along process boundaries and reassemble it without loss.","keywords":["quantum process calculus","spatial compositionality","Deutsch-Hayden descriptors","open quantum systems","process equivalence","BB84","qubit transfer"],"falsifier":"Exhibit a store that obeys the Pauli equations yet cannot arise as a unitary image of the all-zero store, or a pair of independently evolved local stores whose union fails to equal the true global store after a parallel step.","tokens_in":30634,"feed_emoji":"⚛️","tokens_out":548,"duration_ms":6266,"temperature":0.7,"pith_summary":"Standard quantum process calculi keep one global density matrix or state vector for every qubit in the system. That forces every local step to be checked against the whole, and it loses entanglement information when you try to focus on one process. This paper replaces that global store with Deutsch-Hayden descriptors that are indexed by qubit names rather than positions. Because each descriptor already encodes the history of operations that touched its qubit, fragments of the store can be cut out, evolved on their own, and later glued back together by simple union; the joint state is recovered exactly. The resulting calculus, DH-CCS, therefore lets messages carry the actual local state of a qubit instead of a mere name, unifies allocation, discard and measurement as boundary transfers, and supports open-system reasoning in which qubits leave, interact with an external party, and return while remaining entangled. A physics-grounded observational equivalence and a bisimulation whose soundness proof is simplified by the same compositionality complete the framework. The BB84 fragment shows both the power (tracking qubit ownership across boundaries) and the current limit (information-flow arguments still need density matrices).","feed_headline":"Quantum processes can now be split and rejoined without losing entanglement","feed_subtitle":"Named Deutsch-Hayden stores let each process evolve alone; their union recovers the joint state.","key_machinery":"Nominal Deutsch-Hayden stores (maps from qubit names to pairs of Hermitian operators in a colimit of finite-dimensional spaces) that obey the Pauli equations; they are split by domain restriction and recomposed by union, carrying entanglement structure as mutual mentions of names.","core_discovery":"Deutsch-Hayden descriptors, once re-indexed by stable qubit names, yield a spatially compositional quantum process calculus: every parallel configuration splits into independent local views whose independent evolutions recompose by union to the unique global evolved store, even under entanglement.","pith_inferences":[],"forward_implications":[],"fun_headline_variants":["Deutsch-Hayden stores let quantum processes split and rejoin without losing entanglement","Spatially compositional calculus tracks local qubit views that recompose under entanglemen","Quantum process calculus splits system state along boundaries while preserving joint info","Local process evolutions recompose to global store via re-indexed Deutsch-Hayden descripto","Qubit-transfer messages carry actual states, enabling independent process analysis"],"cache_read_input_tokens":16512,"weakest_assumption_plain":"Any store that satisfies the Pauli equations is physically realizable and can always be completed to a unitary evolution of the all-zero state.","fun_headline_variants_meta":{"raw":{"variants":["Deutsch-Hayden stores let quantum processes split and rejoin without losing entanglement","Spatially compositional calculus tracks local qubit views that recompose under entanglement","Quantum process calculus splits system state along boundaries while preserving joint info","Local process evolutions recompose to global store via re-indexed Deutsch-Hayden descriptors","Qubit-transfer messages carry actual states, enabling independent process analysis"]},"model":"grok-4.5","effort":"low","cost_usd":0.003446,"raw_usage":{"total_tokens":1101,"prompt_tokens":790,"num_sources_used":0,"completion_tokens":80,"cost_in_usd_ticks":34460000,"prompt_tokens_details":{"text_tokens":790,"audio_tokens":0,"image_tokens":0,"cached_tokens":0},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":231,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":790,"tokens_out":80,"duration_ms":3825,"temperature":1.0,"reasoning_tokens":231,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-14T06:12:47.179893+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"Exhibit a store that obeys the Pauli equations yet cannot arise as a unitary image of the all-zero store, or a pair of independently evolved local stores whose union fails to equal the true global store after a parallel step.","supporting_citations":[],"review_version":1}