{"id":"dd08544d-abb4-488e-9c05-a02b92a0f2a6","arxiv_id":"2510.07051","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Sound and complete relational logic for classical-quantum programs with unbounded assertions, built on a new classical-quantum optimal-transport duality theorem.","lead":"cqOTL, a new relational program logic for hybrid classical-quantum programs, is claimed to be sound and complete even when assertions are unbounded. If correct, it closes the last completeness gap in this line of work and gives a foundation for verifying post-quantum cryptography.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma C.2's trace-norm compactness of couplings is false for countable classical spaces; [Conseq], [Limit], and [Unbounded-Duality] all rely on it, so soundness—and hence the central completeness claim—is not established as written.","rationale":"The paper's central claim is Theorem 8.2: soundness and completeness of cqOTL for all HAST cqWhile programs and unbounded assertions. Completeness is built on the [Unbounded-Duality] rule, whose soundness in turn relies on the structural rules [Limit] and [Conseq]. All three soundness proofs in Appendix F explicitly invoke Lemma C.2 to pass from a sequence or family of couplings to a limiting coupling. That lemma is not merely under-proved; it is false for infinite countable classical state spaces, as the explicit transposition-coupling family shows. Since the classical state space of cqWhile is countable (and can be infinite), the proof of soundness as written has a genuine gap at the point where convergent subsequences are asserted to exist. The same counterexample also affects the compactness step used in [Conseq] to replace an infimum by a minimum. The reader's verdict identified the external dependence on Lemma C.2 as the weakest assumption; I agree, but the concern is stronger than the reader stated: the lemma is refuted by an elementary construction, not just unverified. A possible repair would be to replace trace-norm compactness by a weaker compactness (e.g., weak-* or narrow compactness for the induced classical-quantum densities) and to prove a corresponding Fatou lemma that works for unbounded assertions and pointwise limits; the paper does not currently supply such an argument. The subnormalized-state issue raised by the reader is also present in the [Unbounded-Duality] soundness proof, since Theorem 8.11 is stated for trace-1 states while the proof applies it to partial states; however, that issue is repairable by normalizing the common trace mass, so it is not the primary reason for rejecting. Overall, the central soundness/completeness claim is unsupported by the current proof because a load-bearing lemma is false.","tokens_in":69193,"tokens_out":8629,"duration_ms":77712,"concrete_test":"Verify the counterexample: take H=C, A1=A2=N, μ(i)=2^{-(i+1)}. For n≥1 define π_n=(0 n) and γ_n=Σ_i μ(i) δ_{(i,π_n(i))}. Check each γ_n has marginals μ, and ∥γ_n−γ_m∥_1 = 2(μ(0)+μ(n)+μ(m)) ≥ 1 for n≠m. Thus no subsequence converges, so the set of couplings is not compact in trace norm. Then re-run the soundness proof of [Limit] (§F.1) with this family as the Δ_n; if no trace-norm limit can be selected, the proof of the rule as stated fails.","verdict_should_be":"REJECT","load_bearing_attack":"Section C, Lemma C.2 asserts: for any cq-states Δ1, Δ2, {Δ | Δ:⟨Δ1,Δ2⟩} is compact in trace-norm topology. This is false even in the purely classical case H=C. Let A1=A2=N, μ(i)=2^{-(i+1)}, and Δ1=Δ2=μ. For each n≥1 let π_n be the transposition (0 n) and define γ_n = Σ_i μ(i) δ_{(i,π_n(i))}. Each γ_n is a coupling of μ with μ. For n≠m, the total-variation distance ∥γ_n−γ_m∥_1 = 2(μ(0)+μ(n)+μ(m)) ≥ 1, since μ(0)=1/2. Hence (γ_n) has no Cauchy subsequence, contradicting compactness. The proof of Lemma C.2 cites Friedland–Ge–Zhi Theorem 1.4, but that result cannot imply trace-norm compactness here: the trace-class unit ball of an infinite-dimensional Hilbert space is not compact. The false lemma is used in Appendix F: [Conseq] uses it to turn an infimum into a minimum, and [Limit] and [Unbounded-Duality] use it to extract a convergent subsequence from a family of couplings. Without a valid replacement (e.g., a weak/pointwise compactness argument plus a Fatou lemma appropriate for unbounded assertions), the soundness proofs of these structural rules collapse. The subnormalized-state issue in [Unbounded-Duality] is real but arguably repairable by scaling the trace-1 duality theorem; the compactness failure is a direct counterexample, not merely a missing justification.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops cqOTL, a sound and complete relational program logic for a classical-quantum while language (cqWhile) with unbounded, infinite-valued assertions. Judgments {ψ} c1 ∼ c2 {φ} are interpreted over state couplings: validity requires that for every input coupling there is an output coupling satisfying E[φ] ≤ E[ψ]. The proof system combines one-sided and two-sided rules with structural rules [Conseq], [Limit], and [Unbounded-Duality]. Completeness is obtained by first proving completeness for split postconditions via non-relational weakest preconditions, then using a Kantorovich–Rubinstein-type duality theorem (Theorem 8.11 / B.1) to reduce arbitrary postconditions to split ones. The appendix contains detailed proofs of the duality theorem, convergence results, soundness, and completeness, and the paper also derives completeness for pWhile and qWhile with unbounded assertions.","tokens_in":69550,"tokens_out":23501,"duration_ms":196868,"significance":"If the results are correct, Theorem 8.2 is a significant advance: it would be the first unconditional completeness theorem for a relational logic covering classical-quantum programs, improving on prior bounded-postcondition results [4, 10]. The duality theorem for hybrid classical-quantum states, with its dimension-independent norm bound, is a contribution of independent interest in quantum optimal transport. The paper is unusually detailed: the main duality proof is carried out in the appendix, and the proof system is exercised on nontrivial examples including deferred measurement and rejection sampling. However, the claimed scope is broader than the formal development, and two load-bearing proof points—the use of the duality theorem for subnormalized states and the proof of the coupling compactness lemma—need repair.","major_comments":[{"comment":"The title and abstract claim a logic for 'infinite-dimensional quantum programs' and 'infinite-dimensional duality theorems for infinite-dimensional quantum states,' but Section 3 explicitly says 'We only consider finite-dimensional Hilbert spaces,' and Theorem 8.11/B.1 is stated for finite-dimensional H1, H2. Appendix B further says the extension to general infinite-dimensional quantum density operators is deferred. The paper's actual infinite-dimensionality is in the countable classical state spaces and in unbounded assertions, not in the quantum registers. This overclaim should be corrected in the title/abstract or the results must be genuinely extended.","section":"Abstract, Section 3, Appendix B"},{"comment":"Theorem B.1 is stated only for states with tr(Δ1)=tr(Δ2)=1. In the soundness proof of [Unbounded-Duality], the proof applies this theorem to Δ'_1 = ⟦c1⟧(|σ1,tr2(ρ)|) and Δ'_2 = ⟦c2⟧(|σ2,tr1(ρ)|), whose common trace is t = tr(ρ), which can be strictly less than 1. The displayed manipulation 'tr(ψ(σ1,σ2)ρ) + n ≥ sup ...' should read 'tr(ψρ) + n·t ≥ ...', and the duality theorem then gives sup(E[φ1]+E[φ2] − n·t), not −n. A normalization/scaling argument for subnormalized states is needed. As written, the proof of soundness of this central rule is incomplete.","section":"Appendix F, soundness of [Unbounded-Duality]"},{"comment":"Lemma C.2 asserts trace-norm compactness of the set of couplings and cites Friedland–Ge–Zhi Theorem 1.4 as an immediate corollary. That theorem cannot imply trace-norm compactness of all couplings in a separable Hilbert space, since the trace-class unit ball of an infinite-dimensional Hilbert space is not trace-norm compact. In the present setting (finite-dimensional H, countable A) the lemma is in fact true and can be proved directly by a total-boundedness/truncation argument, but the supplied proof is not valid. This matters because the soundness proofs of [Conseq], [Limit], and [Unbounded-Duality] all rely on the compactness of the coupling set to turn approximate witnesses into exact ones. The proof must be replaced by a correct direct argument. (For completeness: the specific transposition counterexample that has been circulated does not refute the lemma—the proposed γ_n have second","section":"Appendix C, Lemma C.2"}],"minor_comments":[{"comment":"The definition of state coupling has a typo: it says 'Δ1 ∈ S(A2,H1)' and 'Δ2 ∈ S(A2,H2)'; the first should be S(A1,H1).","section":"Definition 5.4"},{"comment":"The paragraph introducing CVarrel and cStatesrel is repeated almost verbatim; one copy should be deleted.","section":"Section 5.2"},{"comment":"The headings read 'Classical-qantum monotone convergence' and 'Classical-qantum Fatou’s lemma'—likely typos for 'classical-quantum.'","section":"Propositions 8.12 and 8.13"},{"comment":"The definition of HAST reads awkwardly: 'almost-surely terminating, written c∈AST, if it is trace-preserving, and hereditarily trace-preserving, written c∈HAST, if all its sub-programs are.' It should explicitly say that HAST means all subprograms are AST/trace-preserving.","section":"Section 4.3"},{"comment":"The proof of Lemma C.2 should either prove the total-boundedness argument or cite a theorem that actually gives trace-norm compactness for the block-diagonal sub-class of couplings used here.","section":"Appendix C, Lemma C.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is technically substantial and the central completeness architecture is plausible, but it is not ready in its current form. The most serious issues are the mismatch between the claimed infinite-dimensional quantum scope and the finite-dimensional development, and the subnormalized-state gap in the soundness proof of [Unbounded-Duality]. The compactness lemma is true in the relevant finite-dimensional-H setting, but the cited proof is invalid and should be replaced. These are repairable within the manuscript's scope, so I recommend major revision rather than rejection."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here is my take. The paper has a genuine contribution: a classical-quantum duality theorem with a dimension-independent norm bound, used to lift bounded-completeness to unbounded postconditions for a hybrid classical-quantum relational logic. That is a real step beyond [4,10], and the completeness architecture is clearly explained. The examples are instructive, and the prototype/Lean piece shows serious intent.\n\nBut the main theorem is not established as written, because the compactness lemma it leans on is false. Appendix C, Lemma C.2 asserts the set of couplings of two cq-states is compact in trace-norm topology. Counterexample: take H=C, A1=A2=N, μ(i)=2^{-(i+1)}, and let π_n be the transposition (0 n), γ_n=Σ_i μ(i)δ_{(i,π_n(i))}. Each γ_n couples μ with μ, but for n≠m, ∥γ_n−γ_m∥_1=2(μ(0)+μ(n)+μ(m))≥1. So the sequence has no Cauchy subsequence. The cited Friedland–Ge–Zhi result cannot imply trace-norm compactness here; the trace-class unit ball of an infinite-dimensional Hilbert space is not compact. This lemma is used in [Conseq], [Limit], and [Unbounded-Duality] to turn infima into minima and to extract convergent subsequences. Without a replacement, the soundness proofs of those rules collapse, and completeness goes with them.\n\nThe subnormalized-state issue with Theorem B.1 is real but likely repairable by normalization. A second issue: the abstract promises infinite-dimensional quantum programs, but Section 3 restricts to finite-dimensional Hilbert spaces; the footnote says the extension is deferred. That is an overclaim, not the core problem.\n\nI do not think the paper is a wasted effort. The duality theorem and the norm-bound argument may be salvageable, and the overall plan is sound. But the current version overstates what is proved: the central completeness theorem is conditional on fixing the compactness argument. A serious referee should look at it, with explicit instructions to check Appendix C and the rules that rely on it. For my own work I would not yet cite it as a complete logic; I would cite it as a promising preprint with a known gap. I'd bring it to the reading group only if the group has patience for a dense appendix and a good counterexample discussion.","headline":"Genuine contribution, but the main completeness theorem is not established: the coupling compactness lemma is false, and the structural rules rest on it.","tokens_in":70079,"tokens_out":4188,"would_cite":false,"duration_ms":24696,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","81P68","49Q22","90C46"],"pacs":[],"model":"deepseek-v4-flash","headline":"cqOTL is the first sound and complete relational logic for classical-quantum programs, with completeness resting on a new duality theorem for hybrid quantum states with unbounded assertions.","keywords":["classical-quantum programs","relational Hoare logic","duality theorem","unbounded assertions","couplings","optimal transport","completeness","quantum verification"],"falsifier":"Exhibit a pair of classical-quantum states of equal total mass and a bounded assertion φ such that the infimum of EΔ[φ] over all couplings strictly exceeds the supremum of EΔ1[φ1]+EΔ2[φ2]−n over split assertions — a duality gap contradicting Theorem 8.11 and, with it, completeness. A more targeted check: build a sequence of approximate couplings of two subnormalized states with no convergent subsequence, which would break the cited compactness lemma that the limit rules depend on.","tokens_in":69063,"feed_emoji":"⚛️","tokens_out":10214,"duration_ms":76879,"temperature":0.7,"pith_summary":"This paper settles a standing question: can relational reasoning about hybrid classical-quantum programs be complete, so that every semantically valid judgment has a proof? The authors present cqOTL, a relational program logic for the cqWhile language, and prove that for almost-surely terminating programs every valid judgment — including those with unbounded, infinite-valued relational assertions over countably infinite classical state spaces — is derivable. The result rests on a duality theorem for classical-quantum states: the minimal expected value of an assertion over all couplings of two states equals a supremum over split assertions on the marginals, a hybrid analogue of classical optimal-transport duality. This identity lets the logic reduce arbitrary relational reasoning to non-relational weakest-preconditions. If correct, cqOTL is the first relational logic with unconditional completeness for quantum or classical-quantum programs, and the same theorem upgrades the probabilistic logic eRHL and the quantum logic qOTL to full unbounded completeness.","feed_headline":"Hybrid quantum programs get their first complete proof logic","feed_subtitle":"A new duality theorem makes every valid program relation provable, even with unbounded assertions.","key_machinery":"The central object is the duality set Y(φ) of a relational assertion φ: triples (n, φ1, φ2) with bounded unary assertions φ1, φ2 such that φ1⊗id + id⊗φ2 ⊑ φ + n·id. The duality identity — the infimum of E[φ] over all couplings equals the supremum of E[φ1]+E[φ2]−n over Y(φ) — converts any postcondition into a split one, where weakest-precondition reasoning applies. Its proof uses conic-programming duality on finite classical spaces, then a norm bound (Lemma B.4) on ε-approximate maximizers of the dual program that depends only on ‖φ‖ and ε — not on the size of the classical space or Hilbert-space dimension — which controls the approximation error when passing from finite subsets to the full c","core_discovery":"The central claim is Theorem 8.2: for HAST cqWhile commands c1, c2 and any unbounded relational assertion φ, semantic validity ⊨{ψ}c1∼c2{φ} implies derivability ⊢{ψ}c1∼c2{φ} in cqOTL. The engine is the classical-quantum duality theorem (Theorem 8.11): for states Δ1, Δ2 with equal total mass and bounded φ, the infimum of EΔ[φ] over couplings Δ equals the supremum of EΔ1[φ1]+EΔ2[φ2]−n over bounded split assertions φ1⊗id+id⊗φ2 ⊑ φ+n·id. Countably infinite classical state spaces rule out merely combining classical and finite-dimensional quantum duality; the proof adds a dimension-independent norm bound on ε-approximate dual optimizers and takes a finite-to-countable limit. The same duality gives","pith_inferences":["If the duality theorem is correct, it is likely to be useful beyond verification — hybrid classical-quantum optimal transport has lacked such an identity, and the claimed extension to infinite-dimensional density operators is a natural statement to verify.","Completeness moves the practical bottleneck from constructing couplings to discharging assertion-level math, so decision procedures for Dirac notation, orthomodular logic, and classical theories become the gating technology for tool support.","A testable extension: the same finite-approximation technique should yield duality for classical state spaces beyond countable sets (e.g., measurable spaces), provided the compactness of couplings holds there — a reader could check whether the subnormalized-state compactness needs a genuinely new proof."],"forward_implications":["cqOTL becomes the first relational logic with unconditional completeness for classical-quantum programs: every valid relational judgment, including unbounded quantitative assertions, has a proof.","The new unbounded duality rule removes prior boundedness restrictions: eRHL for probabilistic programs and qOTL for quantum programs are each sound and complete for arbitrary infinite-valued postconditions.","The unified coupling condition for sampling and measurement lets the logic relate programs whose random draws and measurements are misaligned, such as a Bernoulli sample matched against two qubit measurements.","The authors report a machine-checked prototype (~2.5K lines) suggesting the proof obligations can be mechanized, a step toward verification of post-quantum cryptography on a complete logical foundation."],"fun_headline_variants":["Unbounded assertions now provable in quantum logic","Complete proof logic for infinite-dimensional quantum programs","Quantum program logic handles unbounded assertions completely","New duality theorem completes quantum program verification","Infinite-dimensional quantum programs get complete relational logic"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"Soundness of the limit, consequence, and unbounded-duality rules presupposes that the set of couplings of two classical-quantum states is compact in the trace-norm topology, with the expectation function lower semicontinuous — a fact the paper takes from the literature rather than proving; if compactness fails for countably infinite classical support or subnormalized states, the convergent-subsequence arguments that promote approximate couplings to exact ones collapse.","fun_headline_variants_meta":{"raw":{"variants":["Unbounded assertions now provable in quantum logic","Complete proof logic for infinite-dimensional quantum programs","Quantum program logic handles unbounded assertions completely","New duality theorem completes quantum program verification","Infinite-dimensional quantum programs get complete relational logic"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000138,"raw_usage":{"total_tokens":927,"prompt_tokens":619,"completion_tokens":308,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":363,"completion_tokens_details":{"reasoning_tokens":240}},"tokens_in":363,"tokens_out":308,"duration_ms":2833,"temperature":1.0,"reasoning_tokens":240,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T11:03:39.196622+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Exhibit a pair of classical-quantum states of equal total mass and a bounded assertion φ such that the infimum of EΔ[φ] over all couplings strictly exceeds the supremum of EΔ1[φ1]+EΔ2[φ2]−n over split assertions — a duality gap contradicting Theorem 8.11 and, with it, completeness. A more targeted check: build a sequence of approximate couplings of two subnormalized states with no convergent subsequence, which would break the cited compactness lemma that the limit rules depend on.","supporting_citations":[],"review_version":1}