{"id":"bed424b3-cebe-4612-9a64-817258f2dd40","arxiv_id":"2608.05807","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A noise-aware quantum Hoare logic and an automated synthesis method produce hardware-specific optimal quantum subroutines, showing that classical probabilistic branching can be necessary for optimality.","lead":"This paper introduces a logic and algorithms for checking and generating small quantum programs against the specific error models of real quantum hardware, such as IBM's published calibration data. It finds that on real noisy hardware, the best short programs often differ from textbook circuits, and sometimes require classical random choices.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Counterexample to Lemma 5.1: DCP/CondBlock omits programs that branch on an initially non-constant classical variable, so the LP-based 'hardware-optimal' synthesis claim is false as stated.","rationale":"The reader correctly identified Lemma 5.1 and the completeness of the DCP/CondBlock enumeration as the weakest point. My stress test makes the concern concrete rather than merely a missing proof: because the grammar allows if as a top-level construct, a length-1 program can branch on a classical variable whose value is fixed within each initial ensemble but varies across the precondition. Eq. 8 only introduces branching after an instruction has been executed and produced multiple classical states, so such programs are absent from A_k. The counterexample above shows this is not a harmless omission: no fixed convex combination over A_1 can match the if-program's behavior on the two corners, and the LP target value is 0.5 instead of the achievable 1. Thus the paper's central claim that Eq. 12 returns a hardware-optimal program among all admissible loop-free programs of length at most k is false as stated. This does not invalidate the ensemble semantics, the soundness of nQHL, or the verification decision procedure for loop-free programs, which appear to be genuine contributions; but it does invalidate the headline synthesis optimality result. The appropriate disposition is therefore rejection or major revision, not conditional acceptance in the current form.","tokens_in":45080,"tokens_out":32123,"duration_ms":326037,"concrete_test":"Implement the paper's own definitions for the counterexample: one qubit q0, one classical variable x, instruction set J={H([q0]), X([q0])}, horizon k=1, precondition φ as the two singleton polytopes β0=(|0>,x=0) and β1=(|1>,x=1), and target set T={|+>,|0>}. Compute A_1 from Eq. 8 and solve the LP in Eq. 12. If the LP optimum is 0.5 while the program if(x){X([q0])}else{H([q0])} succeeds with probability 1, Lemma 5.1 and Theorem 5.2 are refuted as stated. If instead the intended A_k includes top-level CondBlock(β,k), Eq. 8 must be amended and the optimality theorem re-proved; the current text gives no such construction.","verdict_should_be":"REJECT","load_bearing_attack":"Lemma 5.1 is false as stated. Take ideal hardware, one qubit q0, one classical bit x, instruction set J={H([q0]), X([q0])}, horizon k=1, linear precondition φ = {P(q0=|0>∧x=0)=1} ∨ {P(q0=|1>∧x=1)=1}, and target postcondition ψ = P(q0=|+> ∨ q0=|0>)=1. The length-1 candidate program P = if(x){X([q0])}else{H([q0])} is admissible and the triple {φ}P{ψ} is valid: from β0=(|0>,x=0) it applies H and reaches |+>; from β1=(|1>,x=1) it applies X and reaches |0>. However, the set A_1 built by DCP/CondBlock from the corners contains only halt, H, and X (with halt suffixes): Eq. 8 only introduces branching after an instruction J has produced multiple classical states, so a program whose first action is if(x) is not generated. A fixed convex combination of A_1 programs would need, for β0, p_H+p_halt=1 and p_X=0; for β1, p_X=1 and p_H=p_halt=0. These conditions are incompatible, so no convex combination in A_1 satisfies ψ, contradicting Lemma 5.1. Consequently, the LP in Eq. 12 over A_1 returns max p=0.5, while P achieves p=1. The root cause is that a linear precondition may be a union of ensembles with different initial classical values; an optimal program may branch on that classical variable before executing any instruction, and the definition of DCP never starts with CondBlock(β,l).","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper develops a comprehensive framework for reasoning about quantum programs executed on noisy hardware. It introduces nQHL, a Hoare logic interpreted over ensembles (probability distributions over classical-quantum states) rather than density matrices, with proof rules parameterized by hardware error models; soundness is proved in the appendix (Theorem 3.1). It then presents an automated verification procedure (checkLin) for loop-free programs with linear preconditions, based on exploring ensemble graphs and encoding postcondition satisfaction in the first-order theory of real-closed fields; correctness is proved in the appendix (Theorem 4.3). For synthesis, the paper reduces bounded synthesis to enumeration of a finite set A_k of deterministic programs (Eq. (8), DCP/CondBlock), then computes optimal probabilistic mixtures by linear programming for target postconditions (Theorem 5.2) and by Bellman value iteration on quantum-belief game graphs for singular preconditions (Theorem 5.3). Experiments on five quantum subroutines across 55 IBM Qiskit hardware specifications report hardware-dependent optimal programs, frequently using probabilistic branching. The synthesis claims for linear preconditions rest on Lemma 5.1, which the main text justifies only by a one-paragraph appeal to Kuhn's theorem. Section 3.3 explicitly states that relative completeness of the logic is not studied, a reasonable scope limitation.","tokens_in":45387,"tokens_out":31227,"duration_ms":299232,"significance":"If the results held as stated, this would be a strong and timely contribution. The ensemble semantics is well motivated (Examples 1 and 2 show that density-matrix abstractions lose information needed for modular subroutine verification), the soundness proof of nQHL and the correctness proof of checkLin in the appendix appear correct, the arbitrary-precision treatment of verification is rigorous, and the evaluation across 55 hardware specifications is substantial. The paper also builds on and generalizes the authors' prior work [19] rather than duplicating it. However, the 'hardware-optimal' synthesis guarantee for linear preconditions is false as stated: Lemma 5.1 is contradicted by a concrete counterexample, and the optimality clause of Theorem 5.2 therefore fails (see Major Comments). The verification and logic contributions remain valuable; the synthesis contribution needs either a strengthened enumeration with a genuine completeness proof or a re-scoping of its claims.","major_comments":[{"comment":"Lemma 5.1 is false as stated. Consider ideal hardware, one qubit q0, one classical bit x, instruction set J={H([q0]), X([q0])}, horizon k=1, linear precondition φ := {P([q0]=|0> ∧ [x]=0)=1} ∨ {P([q0]=|1> ∧ [x]=1)=1} (two singleton polytopes), and target postcondition ψ := P([q0]=|+> ∨ [q0]=|0>)=1. The program P := if(x){X([q0])}else{H([q0])} is a candidate program of length 1, is admissible under the trivial guard, and {φ}P{ψ} is valid: from β0=(|0>,x=0) it takes the else-branch and reaches |+>, and from β1=(|1>,x=1) it takes the then-branch and reaches |0>. However, DCP(β0,1)=DCP(β1,1)={halt, H;halt, X;halt}: since |CStates(JJK_H(β))|=1 for every instruction applied to a corner, the CondBlock clause of Eq. (8) is never triggered, and A_1 contains no program whose first action is a conditional. For any convex combination of A_1 programs, the success probability from β0 is p_halt+p_H while from β1 it is p_X; validity of the triple requires both to equal 1, which is impossible (p_X=0 and p_X=1 simultaneously). The LP in Eq. (12) over A_1 therefore returns max p=0.5, whereas P achieves p=1. The root cause is that DCP is applied corner-by-corner and never branches on a classical variable that is non-constant across the precondition. The one-paragraph invocation of Kuhn's theorem does not repair this: the omitted programs are pure strategies, not mixed strategies, so the theorem is inapposite to the completeness of the enumeration.","section":"Section 5.1, Lemma 5.1 and Eq. (8)"},{"comment":"Theorem 5.2 inherits the failure of Lemma 5.1. Its optimality claim ('Moreover, Σ x_i P_i is optimal for the precondition φ and target φ') quantifies over all admissible programs of length at most k, but Eq. (12) only optimizes over the rows M_{ij} given by the incomplete set A_k (or A^{φ,φ}_k). The counterexample of Major Comment 1 shows the LP optimum (0.5) is strictly below the value achievable by an admissible length-1 program (1). The appendix (Section 10.1) does not prove Lemma 5.1; its proof of Theorem 5.2 simply states that 'we consider all deterministic programs that satisfy the instruction guard and are of length at most k,' which is precisely the completeness claim refuted above. Consequently, the 'hardware-optimal' wording in the abstract, the introduction, and in the linear-precondition experiments of Section 6.2 is unsupported for linear preconditions. The statement can be repaired either by extending the DCP/CondBlock enumeration to branch on the classical state of the initial ensemble (equivalently, partitioning the precondition's ensembles into beliefs before any instruction, as Section 5.3 already does for singular preconditions) and proving completeness of the extended enumeration over all length-≤k programs, or by explicitly restricting all optimality claims to the enumerated program family and re-framing the experiments accordingly. Note that in all benchmarks of Section 6 the initial classical state is constant (x0=0) across corners, so the reported numbers may survive the repair, but the claimed guarantees need re-statement.","section":"Section 5.2, Theorem 5.2 and Eq. (12)"}],"minor_comments":[{"comment":"The definition φ_Ω := ⋁_{P∈Ω} (⋀_{β∈P} φ_β), with φ_β singular, is not coherent for polytopes with more than one corner: the conjunction of two distinct singular assertions is unsatisfiable, yet Example 4 treats a two-corner polytope as a satisfiable precondition and Algorithm 1 iterates over conv(P) semantics. Please define polytope assertions directly (e.g., φ_P denotes the set conv(P)) and state the linearity assumption with that semantics.","section":"Section 4.2 (definition of linear assertion)"},{"comment":"The bound (N+1)·ρ·(k+1)+((N+1)/2)·log(N+1) for exactly solving Eq. (12) is asserted without proof, and citation [5] (Bland) guarantees finite termination only for the simplex method with a specific pivoting rule, not for arbitrary solvers. Please supply a derivation or restate the bound as a property of the implemented arbitrary-precision simplex procedure.","section":"Section 5.2 (precision bound after Theorem 5.2)"},{"comment":"The closing sentence says that game-theoretic synthesis of hardware-optimal programs with 'more general preconditions' is left as an open challenge, which conflicts with Section 5.2's claim of optimality for all linear preconditions; please clarify the scope of both statements in light of the issues with Lemma 5.1.","section":"Section 7 (Conclusion)"},{"comment":"The paper explicitly states that relative completeness of nQHL is not studied; given the novelty claims for the logic, I suggest adding a short discussion of what a completeness result for the loop-free fragment would require, so readers can calibrate the logic's power in comparison with dense-matrix-based logics.","section":"Section 3.3 and Section 1.2"}],"recommendation":"major_revision","confidential_remarks":"For the editor: the stress-test counterexample is valid as it stands and directly falsifies Lemma 5.1 and the optimality clause of Theorem 5.2. This is a genuine gap, not a presentation issue: the DCP/CondBlock enumeration is applied corner-by-corner and cannot produce programs that branch on classical information that varies across the corners of a linear precondition before any instruction is executed. I recommend major revision rather than rejection because (i) the soundness of nQHL and the correctness of checkLin appear solid, and (ii) the synthesis gap is localizable and plausibly repairable, e.g., by starting the enumeration with a partition of the initial ensemble into classical-state beliefs (as Section 5.3 already does for singular preconditions) and proving completeness of the extended enumeration. The experimental numbers in Section 6 may survive the repair because all benchmarks start from classical states that are constant (x0 = 0) across the corners of the precondition, but the 'hardware-optimal' phrasing must be re-validated or weakened. Also worth checking during revision: the definition of linear assertions (conjunct of singular corner assertions) and the unproved precision bound for the LP."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the honest read. The ensemble-based nQHL and the checkLin verification procedure are the real contributions, and they look correct. The soundness proof, the realForm translation, and the convexity argument for linear preconditions all check out. The Bell-state preparation example is the right illustration of why density matrices lose information needed for modular reasoning.\n\nThe synthesis part, though, has a problem that is deeper than a missing proof. Lemma 5.1 is false. The DCP enumeration in Eq. 8 never starts with CondBlock at the root, so it only generates programs whose first action is an instruction. If the precondition is a union of two ensembles with different initial classical values, an optimal program can branch on that classical variable before doing anything. The stress-test counterexample is correct: with J={H,X}, k=1, phi=(P(q0=|0>,x=0)=1) OR (P(q0=|1>,x=1)=1), and psi=P(q0=|+> OR q0=|0>)=1, the program if(x){X}else{H} is admissible, length 1, and reaches the target with probability 1. But A_1 from DCP is only {halt,H,X}; no convex combination of those reaches the target for both initial branches. So the LP in Eq. 12 returns 0.5, not 1. The claim in Theorem 5.2 that the LP solution is optimal over all programs of length at most k is therefore false as stated.\n\nThis is fixable, and it should be fixed. The right repair is likely to include CondBlock(beta,l) as an option at every DCP level, or to carefully define the program model so that the initial classical state is available for branching. The rest of the synthesis machinery—dominance, LP mixing, belief-MDP value iteration for singular preconditions—does not obviously depend on this specific enumeration, so the fix may be local.\n\nSmaller issues: no code or data artifact, and a few notational slips in the appendices. These are minor compared to the lemma.\n\nWho should read this: anyone working on quantum program logic, NISQ compilation, or hardware-aware synthesis. The verification semantics is worth studying even if the synthesis results are not taken at face value. This deserves a serious referee—not a desk reject—because the core ideas are important and the flaw is specific and addressable. My recommendation: major revision, with the completeness of the program enumeration as the main technical point to verify.","headline":"The verification semantics is a genuine contribution; the synthesis optimality theorem is false as stated, so this needs a major revision before the hardware-optimal claims can be trusted.","tokens_in":45959,"tokens_out":6055,"would_cite":true,"duration_ms":55261,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A new quantum Hoare logic verifies and synthesizes programs against real hardware noise, using ensembles rather than density matrices as the semantic primitive.","keywords":["quantum Hoare logic","noisy quantum hardware","hardware error models","ensemble semantics","density matrices","program synthesis","quantum program verification","probabilistic branching"],"falsifier":"Enumerate every loop-free program of length at most $k$ over a small instruction set (two classical bits, one measurement, a few gates) on a fixed vendor hardware specification, and compare the best worst-case reachability found by brute force against the value returned by the paper's linear-programming synthesis; if any brute-forced program beats the LP solution, the enumeration underlying Lemma 5.1 is incomplete and the hardware-optimality guarantee holds only within the enumerated set.","tokens_in":44831,"feed_emoji":"⚛️","tokens_out":16698,"duration_ms":143624,"temperature":0.7,"pith_summary":"The paper attempts to make quantum program correctness depend on the actual hardware a program will run on. It develops a quantum Hoare logic, nQHL, whose assertions are interpreted over ensembles—probability distributions over classical-quantum states—rather than density matrices, and whose proof rules are parameterised by vendor-published error models for gates and measurements. On top of this logic the paper builds a decision procedure for verifying loop-free programs with linear preconditions, and a synthesis method that, given any linear precondition and target postcondition, returns a program of bounded length that is optimal among all admissible programs for reaching the target set. This matters because short subroutines such as parity checks, state reset, and state discrimination behave differently on different noisy devices, and the synthesized programs beat the textbook noise-free solutions on the vendor hardware specifications used in the evaluation. The paper also reports that classical probabilistic branching can be strictly necessary for optimality, not merely a convenience.","feed_headline":"New logic verifies and synthesizes quantum programs for noisy chips","feed_subtitle":"By tracking full state distributions instead of averages, it beats textbook programs on real noisy hardware.","key_machinery":"The load-bearing object is the ensemble: a finite probability distribution over hybrid states, each hybrid state being a pure quantum state together with an assignment of the classical bits. A hardware specification assigns to every unitary instruction a completely positive trace-preserving set of noise operators and to every measurement a four-entry error matrix, which turns each instruction into a probabilistic successor function on ensembles; these successor functions give the semantics of the programming language and the transitions of the ensemble graph. The ensemble graph is the verification engine: an infinite Markov chain whose states are configurations (program plus ensemble), and for loop-free programs only a finite part reachable within the horizon is explored, with linear preconditions handled by checking the corners of each polytope via convexity. Synthesis is carried by two constructions: the recursive DCP/CondBlock enumeration, which builds the finite set of dominant deterministic programs of length at most $k$, and the maximin linear program of Equation 12, which assigns each dominant program a probability so that the worst-case reachability probability over all initial ensembles is maximized; for a unique initial ensemble, Bellman value iteration on a quantum-belief game graph plays the same role. The Hoare rules HM00–HM01 and HUnitary carry the logic itself, expressing each noisy step as a convex combination of branches weighted by noise probabilities.","core_discovery":"nQHL is the first quantum Hoare logic whose assertions are interpreted over arbitrary ensembles and the first to incorporate hardware error models, and the paper argues that both features are needed for modular reasoning about subroutines on real devices. The central conceptual claim is that ensembles, not density matrices, are the right semantic primitive: two different ensembles can have the same density matrix yet evolve under the same gate into globally distinguishable states, so a subroutine that correctly prepares a local Bell state from one ensemble realization can fail from another, and no density-matrix logic can express the difference. The proof system is shown sound, with noisy measurement and unitary instructions handled by rules that decompose each instruction into branches weighted by the probabilities of the hardware's noise operators. On the algorithmic side, verification of loop-free programs under linear preconditions is reduced to model checking a finite part of an ensemble graph, checking only the corners of each polytope of initial ensembles; and bounded synthesis for target postconditions is reduced to a maximin linear program that mixes finitely many deterministic candidate programs. The paper claims the resulting program is hardware-optimal—that is, it reaches the target set with the highest worst-case probability among all admissible loop-free programs of length at most $k$—and that when the precondition covers two or more ensembles, the optimal program can genuinely require classical probabilistic branching, as in the state-discrimination task where a 50/50 mixture attains 0.75 worst-case success while every deterministic program attains only 0.5.","pith_inferences":["A natural extension would run the verification procedure on pairs of global states with identical partial trace but different local ensemble structure (as in the Bell-state example); any tool built on density-matrix semantics must miss such cases by construction, so such pairs form a ready-made benchmark for separating the two semantics.","If the enumeration lemma is later proved complete, the same linear-programming core should scale to instruction sets with more classical state, where the space of behavioral strategies is much larger and mixed strategies are likely to matter even more.","The paper establishes only bounded-horizon guarantees and notes that unbounded reachability is undecidable even without noise; a natural follow-up is to study how per-horizon optimal values behave as the horizon grows on fixed hardware, whether they converge in practice, and how close bounded programs come to that limit.","The necessity of probabilistic branching for optimality suggests that noisy-hardware compilers should treat classical random choice as essentially free: mixing two or three deterministic strategies could buy substantial accuracy without adding a single quantum gate."],"forward_implications":["The same logical subroutine can be provably optimal for one device and suboptimal for another: the synthesized programs differ across hardware specifications and embeddings, and they differ from textbook noise-free solutions.","Modular verification becomes possible without knowing the global state: a subroutine proven correct under ensemble semantics keeps its guarantee for every ensemble realization consistent with a given reduced density matrix, which no density-matrix logic can express.","Optimal quantum programming may require classical probabilistic branching: for the state-discrimination task even the noise-free optimum is a 50/50 mixture achieving 0.75 worst-case success versus 0.5 for any deterministic program.","Bounded verification and synthesis run with exact rational arithmetic, giving quantitative reachability guarantees to a stated precision rather than only yes/no correctness, with the required precision growing polynomially in the program depth.","For common subroutines such as error-correction parity checks, state reset, and GHZ and Bell-state preparation, hardware-aware synthesis improves on textbook majority-vote programs by up to tens of percentage points on the tested vendor specifications."],"supporting_citations":[{"why":"supplies the standard objects the framework builds on: ensembles, density matrices, CPTP channels, and the textbook treatments of quantum state preparation, error correction, and nonorthogonal state discrimination.","marker":"[20]"},{"why":"the prior POMDP-based synthesis method for a unique initial ensemble and target-state reachability, which this paper generalizes to arbitrary linear preconditions and arbitrary postconditions.","marker":"[19]"},{"why":"the prior satisfaction-based quantum logic over ensembles whose assertions capture only measurement-observable properties, the contrast that grounds the claim that nQHL is the first logic over arbitrary ensembles.","marker":"[6]"},{"why":"defines the classical-quantum language QIMDP that the paper's hybrid programming language extends with a probabilistic branching statement.","marker":"[9]"},{"why":"Kuhn's equivalence of mixed and behavioral strategies, invoked in the one-paragraph justification of Lemma 5.1 on which the hardware-optimality claim of the synthesis method rests.","marker":"[16]"},{"why":"Bellman's dynamic-programming principle, which underlies the value-iteration algorithm used for optimal synthesis from a unique initial ensemble on the quantum-belief game graph.","marker":"[2]"},{"why":"finite pivoting rules for the simplex method, cited to argue that the synthesis linear program can be solved exactly with rational numbers in finitely many steps.","marker":"[5]"},{"why":"the Qiskit toolkit that supplies the 55 vendor hardware specifications from which all experiments draw error models and logical-to-physical qubit embeddings.","marker":"[23]"}],"fun_headline_variants":["Ensemble logic beats density matrices for noisy quantum programs","Noise-aware quantum logic synthesizes optimal subroutines","Quantum logic uses ensembles to verify and synthesize noisy programs","New quantum Hoare logic handles real hardware noise","First noise-aware quantum logic for verification and synthesis"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The synthesis method's guarantee of hardware-optimality rests on the assumption that its candidate list contains every admissible program of the chosen length; this is justified by an invoked game-theory theorem rather than a full proof, so if the list omits a program, optimality holds only within the list.","fun_headline_variants_meta":{"raw":{"variants":["Ensemble logic beats density matrices for noisy quantum programs","Noise-aware quantum logic synthesizes optimal subroutines","Quantum logic uses ensembles to verify and synthesize noisy programs","New quantum Hoare logic handles real hardware noise","First noise-aware quantum logic for verification and synthesis"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000454,"raw_usage":{"total_tokens":2311,"prompt_tokens":1003,"completion_tokens":1308,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":619,"completion_tokens_details":{"reasoning_tokens":1233}},"tokens_in":619,"tokens_out":1308,"duration_ms":10406,"temperature":1.0,"reasoning_tokens":1233,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T23:06:53.992923+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate every loop-free program of length at most $k$ over a small instruction set (two classical bits, one measurement, a few gates) on a fixed vendor hardware specification, and compare the best worst-case reachability found by brute force against the value returned by the paper's linear-programming synthesis; if any brute-forced program beats the LP solution, the enumeration underlying Lemma 5.1 is incomplete and the hardware-optimality guarantee holds only within the enumerated set.","supporting_citations":[{"cited_title":"Nielsen and Isaac L","cited_arxiv_id":null,"evidence_quote":"supplies the standard objects the framework builds on: ensembles, density matrices, CPTP channels, and the textbook treatments of quantum state preparation, error correction, and nonorthogonal state discrimination."},{"cited_title":"Henzinger","cited_arxiv_id":null,"evidence_quote":"the prior POMDP-based synthesis method for a unique initial ensemble and target-state reachability, which this paper generalizes to arbitrary linear preconditions and arbitrary postconditions."},{"cited_title":"Chadha, P","cited_arxiv_id":null,"evidence_quote":"the prior satisfaction-based quantum logic over ensembles whose assertions capture only measurement-observable properties, the contrast that grounds the claim that nQHL is the first logic over arbitrary ensembles."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"defines the classical-quantum language QIMDP that the paper's hybrid programming language extends with a probabilistic branching statement."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Kuhn's equivalence of mixed and behavioral strategies, invoked in the one-paragraph justification of Lemma 5.1 on which the hardware-optimality claim of the synthesis method rests."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Bellman's dynamic-programming principle, which underlies the value-iteration algorithm used for optimal synthesis from a unique initial ensemble on the quantum-belief game graph."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"finite pivoting rules for the simplex method, cited to argue that the synthesis linear program can be solved exactly with rational numbers in finitely many steps."}],"review_version":1}