Search

The development of logic has largely been through the 'deductive' paradigm: conclusions are inferred from established premisses. However, the use of logic in the context of both human and machine reasoning is typically through the dual 'reductive' perspective: collections of sufficient premisses are generated from putative conclusions. We call this paradigm, 'reductive logic'. This expression of logic encompass as diverse reasoning activities as proving a formula in a formal system to seeking to meet a friend before noon on Saturday. This paper is a semantical analysis of reductive logic. In particular, we provide mathematical foundations for representing and reasoning about 'reduction operators'. Heuristically, reduction operators may be thought of as `backwards' inference rules. In this paper, we address their mathematical representation, how they are used in the context of reductive reasoning, and, crucially, what makes them 'valid'.

Sandqvist gave a proof-theoretic semantics (P-tS) for classical logic (CL) that explicates the meaning of the connectives without assuming bivalance. Later, he gave a semantics for intuitionistic propositional logic (IPL). While soundness in both cases is proved through standard techniques, the proof completeness for CL is complex and somewhat obscure, but clear and simple for IPL. Makinson gave a simplified proof of completeness for classical propositional logic (CPL) by directly relating the the P-tS to the logic's extant truth-functional semantics. In this paper, we give an elementary, constructive, and native -- in the sense that it does not presuppose the model-theoretic interpretation of classical logic -- proof of completeness the P-tS of CL using the techniques applies for IPL. Simultaneously, we give a proof of soundness and completeness for first-order intuitionistic logic (IL).

A fundamental problem in quantum many-body physics is that of finding ground states of local Hamiltonians. A number of recent works gave provably efficient machine learning (ML) algorithms for learning ground states. Specifically, [Huang et al. Science 2022], introduced an approach for learning properties of the ground state of an $n$-qubit gapped local Hamiltonian $H$ from only $n^{\mathcal{O}(1)}$ data points sampled from Hamiltonians in the same phase of matter. This was subsequently improved by [Lewis et al. Nature Communications 2024], to $\mathcal{O}(\log n)$ samples when the geometry of the $n$-qubit system is known. In this work, we introduce two approaches that achieve a constant sample complexity, independent of system size $n$, for learning ground state properties. Our first algorithm consists of a simple modification of the ML model used by Lewis et al. and applies to a property of interest known beforehand. Our second algorithm, which applies even if a description of the property is not known, is a deep neural network model. While empirical results showing the performance of neural networks have been demonstrated, to our knowledge, this is the first rigorous sample complexity bound on a neural network model for predicting ground state properties. We also perform numerical experiments that confirm the improved scaling of our approach compared to earlier results., Comment: 11 pages, 7 figures + 40-page appendix

A proof of quantumness is an efficiently verifiable interactive test that an efficient quantum computer can pass, but all efficient classical computers cannot (under some cryptographic assumption). Such protocols play a crucial role in the certification of quantum devices. Existing single-round protocols (like asking the quantum computer to factor a large number) require large quantum circuits, whereas multi-round ones use smaller circuits but require experimentally challenging mid-circuit measurements. As such, current proofs of quantumness are out of reach for near-term devices. In this work, we construct efficient single-round proofs of quantumness based on existing knowledge assumptions. While knowledge assumptions have not been previously considered in this context, we show that they provide a natural basis for separating classical and quantum computation. Specifically, we show that multi-round protocols based on Decisional Diffie-Hellman (DDH) or Learning With Errors (LWE) can be "compiled" into single-round protocols using a knowledge-of-exponent assumption or knowledge-of-lattice-point assumption, respectively. We also prove an adaptive hardcore-bit statement for a family of claw-free functions based on DDH, which might be of independent interest. Previous approaches to constructing single-round protocols relied on the random oracle model and thus incurred the overhead associated with instantiating the oracle with a cryptographic hash function. In contrast, our protocols have the same resource requirements as their multi-round counterparts without necessitating mid-circuit measurements, making them, arguably, the most efficient single-round proofs of quantumness to date. Our work also helps in understanding the interplay between black-box/white-box reductions and cryptographic assumptions in the design of proofs of quantumness., Comment: 51 pages

A central concept within informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how 'inferentialism' -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components., Comment: An abstract of conference paper 'Inferentialist Resource Semantics' (Accepted at MFPS 2024) that was presented at SLSS 2024. arXiv admin note: substantial text overlap with arXiv:2402.09217

Viewing group cohomology as a so-called cohomological functor, G. Mislin has generalised Tate cohomology from finite groups to all discrete groups by defining a completion for cohomological functors in [24]. For any cohomological functor $T^{\bullet}: \mathcal{C} \rightarrow \mathcal{D}$ we have constructed its Mislin completion $\widehat{T}^{\bullet}: \mathcal{C} \rightarrow \mathcal{D}$ in [15] under mild assumptions on the abelian categories $\mathcal{C}$ and $\mathcal{D}$ which generalises Tate cohomology to all $T1$ topological groups. In this paper we investigate the properties of Mislin completions. As their main feature, Mislin completions of Ext-functors detect finite projective dimension of objects in the domain category. We establish a version of dimension shifting, an Eckmann-Shapiro result as well as cohomology products such as external products, cup products and Yoneda products., Comment: 43 pages

A short essay presenting the State-Effect Interpretation of natural deduction rules as an explanatory framework for recent developments in proof-theoretic semantics., Comment: Submitted to 'Logic and Philosophy: Historical and Contemporary Issues Conference'

In systems modelling, a 'system' typically comprises located resources relative to which processes execute. One important use of logic in informatics is in modelling such systems for the purpose of reasoning (perhaps automated) about their behaviour and properties. To this end, one requires an interpretation of logical formulae in terms of the resources and states of the system; such an interpretation is called a 'resource semantics' of the logic. This paper shows how inferentialism -- the view that meaning is given in terms of inferential behaviour -- enables a versatile and expressive framework for resource semantics. Specifically, how inferentialism seamlessly incorporates the assertion-based approach of the logic of Bunched Implications, foundational in program verification (e.g., as the basis of Separation Logic), and the renowned number-of-uses reading of Linear Logic. This integration enables reasoning about shared and separated resources in intuitive and familiar ways, as well as about the composition and interfacing of system components.

The detection and classification of diseases in Robusta coffee leaves are essential to ensure that plants are healthy and the crop yield is kept high. However, this job requires extensive botanical knowledge and much wasted time. Therefore, this task and others similar to it have been extensively researched subjects in image classification. Regarding leaf disease classification, most approaches have used the more popular PlantVillage dataset while completely disregarding other datasets, like the Robusta Coffee Leaf (RoCoLe) dataset. As the RoCoLe dataset is imbalanced and does not have many samples, fine-tuning of pre-trained models and multiple augmentation techniques need to be used. The current paper uses the RoCoLe dataset and approaches based on deep learning for classifying coffee leaf diseases from images, incorporating the pix2pix model for segmentation and cycle-generative adversarial network (CycleGAN) for augmentation. Our study demonstrates the effectiveness of Transformer-based models, online augmentations, and CycleGAN augmentation in improving leaf disease classification. While synthetic data has limitations, it complements real data, enhancing model performance. These findings contribute to developing robust techniques for plant disease detection and classification., Comment: Accepted by ICAART 2024

The logic of bunched implications (BI) can be seen as the free combination of intuitionistic propositional logic (IPL) and intuitionistic multiplicative linear logic (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist's B-eS for IPL, deferring an analysis of proof-theoretic validity, in the sense of Dummett and Prawitz, to another occasion. Essential to BI's formulation in proof-theoretic terms is the concept of a `bunch' of hypotheses that is familiar from relevance logic. Bunches amount to trees whose internal vertices are labelled with either the IMLL context-former or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the `resource interpretation' of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the `number-of-uses' reading of the propositions of linear logic as resources. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling.

We have previously found experimental evidence for several quantum phenomena in oxygen-ion implanted of hydrogenated graphite: ferromagnetism, antiferromagnetism, paramagentism, triplet superconductivity, Andreev states, Little-Parks oscillations, Lamb shift, Casimir effect, colossal magnetoresistance, and topologically-protected flat-energy bands [1-6]. Triplet superconductivity results in the formation of Josephson junctions, thus with potential of being used for spintronics applications in the critical area of quantum computing. In this paper, we are showing new experimental evidence for the formation of two-dimensional (2D) spin waves in oxygen-ion enriched and in hydrogenated highly oriented pyrolytic graphite. The temperature evolution of the remanent magnetization Mrem(T) data confirms the formation of spin waves that follow the 2D Heisenberg model with a weak uniaxial anisotropy. In addition, the step-like features also found in the temperature dependence of the electrical resistivity between insulating and metallic states suggest several outstanding possibilities, such as a structural transition, triplet superconductivity, and chiral properties., Comment: 8 pages,7 figures, accepted by the Conference Editors for the CEC-ICMC 2023 Conference for publication in the IOP Conference Series: Materials Science and Engineering, Advances in Cryogenic Engineering

We describe a quantum algorithm for finding the smallest eigenvalue of a Hermitian matrix. This algorithm combines Quantum Phase Estimation and Quantum Amplitude Estimation to achieve a quadratic speedup with respect to the best classical algorithm in terms of matrix dimensionality, i.e., $\widetilde{\mathcal{O}}(\sqrt{N}/\epsilon)$ black-box queries to an oracle encoding the matrix, where $N$ is the matrix dimension and $\epsilon$ is the desired precision. In contrast, the best classical algorithm for the same task requires $\Omega(N)\text{polylog}(1/\epsilon)$ queries. In addition, this algorithm allows the user to select any constant success probability. We also provide a similar algorithm with the same runtime that allows us to prepare a quantum state lying mostly in the matrix's low-energy subspace. We implement simulations of both algorithms and demonstrate their application to problems in quantum chemistry and materials science., Comment: 17 pages, 6 figures, all comments are welcome, additional references added

We characterize planar graphs and graph minors among other graph theoretic notions in terms of right-angled Artin groups (RAAGs). For this, we determine all sets of elements in RAAGs with ears as underlying graphs that are exactly the sets of vertex generators. Generalizing ear decompositions of graphs to loose ear decompositions, we characterize both decompositions in terms of RAAGs. The desired results follow as applications of loose ear decompositions of RAAGs., Comment: Accepted in the "International Journal of Algebra and Computation"

This work is the first exploration of proof-theoretic semantics for a substructural logic. It focuses on the base-extension semantics (B-eS) for intuitionistic multiplicative linear logic (IMLL). The starting point is a review of Sandqvist's B-eS for intuitionistic propositional logic (IPL), for which we propose an alternative treatment of conjunction that takes the form of the generalized elimination rule for the connective. The resulting semantics is shown to be sound and complete. This motivates our main contribution, a B-eS for IMLL, in which the definitions of the logical constants all take the form of their elimination rule and for which soundness and completeness are established.

A test of quantumness is a protocol that allows a classical verifier to certify (only) that a prover is not classical. We show that tests of quantumness that follow a certain template, which captures recent proposals such as (Kalai et al., 2022), can in fact do much more. Namely, the same protocols can be used for certifying a qubit, a building-block that stands at the heart of applications such as certifiable randomness and classical delegation of quantum computation. Certifying qubits was previously only known to be possible based on the hardness of the Learning with Errors problem and the use of adaptive hardcore (Brakerski et al., 2018). Our framework allows certification of qubits based only on the existence of post-quantum trapdoor claw-free functions, or on quantum fully homomorphic encryption. These can be instantiated, for example, from Ring Learning with Errors. On the technical side, we show that the quantum soundness of any such protocol can be reduced to proving a bound on a simple algorithmic task: informally, answering ``two challenges simultaneously'' in the protocol. Our reduction formalizes the intuition that these protocols demonstrate quantumness by leveraging the impossibility of rewinding a general quantum prover. This allows us to prove tight bounds on the quantum soundness of (Kahanamoku-Meyer et al., 2021) and (Kalai et al., 2022), showing that no quantum polynomial-time prover can succeed with probability larger than $\cos^2 \frac{\pi}{8}\approx 0.853$. Previously, only an upper bound on the success probability of classical provers, and a lower bound on the success probability of quantum provers, were known. We then extend this proof of quantum soundness to show that provers that approach the quantum soundness bound must perform almost anti-commuting measurements. This certifies that the prover holds a qubit., Comment: 27 pages; small typos fixed

Experimental evidence of novel phenomena in hydrogenated graphite fibers is found. An indirect excitonic mechanism is likely leading to a SC state below the temperature Tc = 50 K, where the gap is divergent. Analysis of the gap within the framework provided by the Bardeen-Cooper-Schrieffer (BCS) theory of superconductivity shows that this is a multigap system. The energy gap data can be better explained within the framework of topologically protected flat bands applied to systems in which superconductivity occurs on the surface or at the internal interfaces of the samples. The temperature dependence of the SC gap is linear above 50 K. We use nonlocal differential conductance Gdiff(V) = dI(V)/dV experimental data to show clear evidence of topological phenomena such as interference of chiral asymmetric Andreev edge states and crossed Andreev conversion. Gdiff(V) has a negative part that results from the nonlocal coherence between electron and holes in the Andreev edge states. We conclude that hydrogenated graphite bears the marks of an unconventional high-temperature superconductor (HTSC)., Comment: 5 pages, 7 figures. arXiv admin note: substantial text overlap with arXiv:2005.05876

The use of logical systems for problem-solving may be as diverse as in proving theorems in mathematics or in figuring out how to meet up with a friend. In either case, the problem solving activity is captured by the search for an \emph{argument}, broadly conceived as a certificate for a solution to the problem. Crucially, for such a certificate to be a solution, it has be \emph{valid}, and what makes it valid is that they are well-constructed according to a notion of inference for the underlying logical system. We provide a general framework uniformly describing the use of logic as a mathematics of reasoning in the above sense. We use proof-theoretic validity in the Dummett-Prawitz tradition to define validity of arguments, and use the theory of tactical proof to relate arguments, inference, and search., Comment: submitted

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof system for a target logic by enriching a proof system for another, typically simpler, logic with an algebra of constraints that act as correctness conditions on the latter to capture the former; for example, one may use Boolean algebra to give constraints in a sequent calculus for classical propositional logic to produce a sequent calculus for intuitionistic propositional logic. The idea behind such forms of reduction is to obtain a tool for uniform and modular treatment of proof theory and provide a bridge between semantics logics and their proof theory. The article discusses the theoretical background of the project and provides several illustrations of its work in the field of intuitionistic and modal logics. The results include the following: a uniform treatment of modular and cut-free proof systems for a large class of propositional logics; a general criterion for a novel approach to soundness and completeness of a logic with respect to a model-theoretic semantics; and, a case study deriving a model-theoretic semantics from a proof-theoretic specification of a logic.

We give a comprehensive characterization of the computational power of shallow quantum circuits combined with classical computation. Specifically, for classes of search problems, we show that the following statements hold, relative to a random oracle: (a) $\mathsf{BPP}^{\mathsf{QNC}^{\mathsf{BPP}}} \neq \mathsf{BQP}$. This refutes Jozsa's conjecture [QIP 05] in the random oracle model. As a result, this gives the first instantiatable separation between the classes by replacing the oracle with a cryptographic hash function, yielding a resolution to one of Aaronson's ten semi-grand challenges in quantum computing. (b) $\mathsf{BPP}^{\mathsf{QNC}} \nsubseteq \mathsf{QNC}^{\mathsf{BPP}}$ and $\mathsf{QNC}^{\mathsf{BPP}} \nsubseteq \mathsf{BPP}^{\mathsf{QNC}}$. This shows that there is a subtle interplay between classical computation and shallow quantum computation. In fact, for the second separation, we establish that, for some problems, the ability to perform adaptive measurements in a single shallow quantum circuit, is more useful than the ability to perform polynomially many shallow quantum circuits without adaptive measurements. (c) There exists a 2-message proof of quantum depth protocol. Such a protocol allows a classical verifier to efficiently certify that a prover must be performing a computation of some minimum quantum depth. Our proof of quantum depth can be instantiated using the recent proof of quantumness construction by Yamakawa and Zhandry [STOC 22]., Comment: 104 pages (+ 9 page Appendix), 10 figures

We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with eigenworlds (i.e., generic representatives of worlds) in an arbitrary model. This reasoning is captured by a sequent calculus for a meta-logic (in this case, first-order classical logic) expressive enough to capture the semantics of the object-logic. Essentially, one has a calculus of validity for the object-logic. The method proceeds through the perspective of reductive logic (as opposed to the more traditional paradigm of deductive logic), using the space of reductions as a medium for showing the behavioural equivalence of reduction in the sequent calculus for the object-logic and in the validity calculus. Rather than study the technique in general, we illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL (without negation) are also treated. Intuitively, BI is the free combination of intuitionistic propositional logic and multiplicative intuitionistic linear logic, which renders its meta-theory is quite complex. The literature on BI contains many similar, but ultimately different, algebraic structures and satisfaction relations that either capture only fragments of the logic (albeit large ones) or have complex clauses for certain connectives (e.g., Beth's clause for disjunction instead of Kripke's). It is this complexity that motivates us to use BI as a case-study for this approach to semantics., Comment: accepted

Proof-theoretic semantics (P-tS) is the approach to meaning in logic based on 'proof' (as opposed to 'truth'). There are two major approaches to P-tS: proof-theoretic validity (P-tV) and base-extension semantics (B-eS). The former is a semantics of arguments, and the latter is a semantics of logical constants. This paper demonstrates that the B-eS for intuitionistic propositional logic (IPL) encapsulates the declarative content of a version of P-tV based on the elimination rules. This explicates how the B-eS for IPL works, and shows the completeness of this version of P-tV.

Proof-theoretic semantics (P-tS) is the paradigm of semantics in which meaning in logic is based on proof (as opposed to truth). A particular instance of P-tS for intuitionistic propositional logic (IPL) is its base-extension semantics (B-eS). This semantics is given by a relation called support, explaining the meaning of the logical constants, which is parameterized by systems of rules called bases that provide the semantics of atomic propositions. In this paper, we interpret bases as collections of definite formulae and use the operational view of the latter as provided by uniform proof-search -- the proof-theoretic foundation of logic programming (LP) -- to establish the completeness of IPL for the B-eS. This perspective allows negation, a subtle issue in P-tS, to be understood in terms of the negation-as-failure protocol in LP. Specifically, while the denial of a proposition is traditionally understood as the assertion of its negation, in B-eS we may understand the denial of a proposition as the failure to find a proof of it. In this way, assertion and denial are both prime concepts in P-tS., Comment: submitted

A test of quantumness is a protocol where a classical user issues challenges to a quantum device to determine if it exhibits non-classical behavior, under certain cryptographic assumptions. Recent attempts to implement such tests on current quantum computers rely on either interactive challenges with efficient verification, or non-interactive challenges with inefficient (exponential time) verification. In this paper, we execute an efficient non-interactive test of quantumness on an ion-trap quantum computer. Our results significantly exceed the bound for a classical device's success., Comment: 6 pages, 2 figures

Unique to certain unconventional superconductors is the coexistence of magnetism and superconductivity. We have previously found ferromagnetism and superconductivity in hydrogenated graphitic materials. Herein we present similar as well as completely new findings this time applicable to hydrogenated graphite foils. As the strength of the magnetic field is increased, the temperature-dependent magnetization shows several important transitions. From a Neel paramagnetic-antiferromagnetic transition, to a ferromagnetic superconductor state, to an orbital paramagnetic glass high-temperature superconductor with critical temperature for the dominant phase at Tc = 50 to 60 K. The ferromagnetic state is observed up to room temperature. Thus, the magnetism of hydrogenated low-density carbon graphite foils plays an important role in establishing electronic correlations of which some are superconducting in nature., Comment: 23 pages, 12 figures

In our previous work, high-temperature superconductivity (HTSC) was probed for the first time by using electrical differential conductance Gdiff(V) = dI/dV data as obtained from current-voltage V(I) measurements on a hydrogenated graphitic fiber [1]. While our nonlocal method for finding the superconducting (SC) gap was recently applied to a conventional SC (Pb [2]), the nonlocal Gdiff method was first proposed in [1]. Herein, we are bringing forth an update on the topic., Comment: 9 pages, 3 figures. arXiv admin note: text overlap with arXiv:2005.05876

Quantum mechanical effects have enabled the construction of cryptographic primitives that are impossible classically. For example, quantum copy-protection allows for a program to be encoded in a quantum state in such a way that the program can be evaluated, but not copied. Many of these cryptographic primitives are two-party protocols, where one party, Bob, has full quantum computational capabilities, and the other party, Alice, is only required to send random BB84 states to Bob. In this work, we show how such protocols can generically be converted to ones where Alice is fully classical, assuming that Bob cannot efficiently solve the LWE problem. In particular, this means that all communication between (classical) Alice and (quantum) Bob is classical, yet they can still make use of cryptographic primitives that would be impossible if both parties were classical. We apply this conversion procedure to obtain quantum cryptographic protocols with classical communication for unclonable encryption, copy-protection, computing on encrypted data, and verifiable blind delegated computation. The key technical ingredient for our result is a protocol for classically-instructed parallel remote state preparation of BB84 states. This is a multi-round protocol between (classical) Alice and (quantum polynomial-time) Bob that allows Alice to certify that Bob must have prepared $n$ uniformly random BB84 states (up to a change of basis on his space). Furthermore, Alice knows which specific BB84 states Bob has prepared, while Bob himself does not. Hence, the situation at the end of this protocol is (almost) equivalent to one where Alice sent $n$ random BB84 states to Bob. This allows us to replace the step of preparing and sending BB84 states in existing protocols by our remote-state preparation protocol in a generic and modular way., Comment: 80 pages, 7 protocols

An important theoretical problem in the study of quantum computation, that is also practically relevant in the context of near-term quantum devices, is to understand the computational power of hybrid models, that combine poly-time classical computation with short-depth quantum computation. Here, we consider two such models: CQ_d which captures the scenario of a polynomial-time classical algorithm that queries a d-depth quantum computer many times; and QC_d which is more analogous to measurement-based quantum computation and captures the scenario of a d-depth quantum computer with the ability to change the sequence of gates being applied depending on measurement outcomes processed by a classical computation. Chia, Chung & Lai (STOC 2020) and Coudron & Menda (STOC 2020) showed that these models (with d=log^O(1) (n)) are strictly weaker than BQP (the class of problems solvable by poly-time quantum computation), relative to an oracle, disproving a conjecture of Jozsa in the relativised world. We show that, despite the similarities between CQ_d and QC_d, the two models are incomparable, i.e. CQ_d $\nsubseteq$ QC_d and QC_d $\nsubseteq$ CQ_d relative to an oracle. In other words, there exist problems that one model can solve but not the other and vice versa. We do this by considering new oracle problems that capture the distinctions between the two models and by introducing the notion of an intrinsically stochastic oracle, an oracle whose responses are inherently randomised, which is used for our second result. While we leave showing the second separation relative to a standard oracle as an open problem, we believe the notion of stochastic oracles could be of independent interest for studying complexity classes which have resisted separation in the standard oracle model. Our constructions also yield simpler oracle separations between the hybrid models and BQP, compared to earlier works., Comment: 47 pages, 5 figures

We describe the design and x-ray emission properties (temporal, spatial, and spectral) of Dry Pinch I, a portable X-pinch driver developed at Imperial College London. Dry Pinch I is a direct capacitor discharge device, 300x300x700 mm3 in size and approximately 50 kg in mass, that can be used as an external driver for x-ray diagnostics in high-energy-density physics experiments. Among key findings, the device is shown to reliably produce 1.1 +- 0.3 ns long x-ray bursts that couple approximately 50 mJ of energy into photon energies from 1 to 10 keV. The average shot-to-shot jitter of these bursts is found to be 10 +- 4.6 ns using a combination of x-ray and current diagnostics. The spatial extent of the x-ray hot spot from which the radiation emanates agrees with previously published results for X-pinches suggesting a spot size of 10 +- 6 um in the soft energy region (1-10 keV) and 190 +- 100 um in the hard energy region (>10 keV). These characteristics mean that Dry Pinch I is ideally suited for use as a probe in experiments driven in the laboratory or at external facilities when more conventional sources of probing radiation are not available. At the same time, this is also the first detailed investigation of an X-pinch operating reliably at current rise rates of less than 1 kA/ns.

Achieving quantum computational advantage requires solving a classically intractable problem on a quantum device. Natural proposals rely upon the intrinsic hardness of classically simulating quantum mechanics; however, verifying the output is itself classically intractable. On the other hand, certain quantum algorithms (e.g. prime factorization via Shor's algorithm) are efficiently verifiable, but require more resources than what is available on near-term devices. One way to bridge the gap between verifiability and implementation is to use "interactions" between a prover and a verifier. By leveraging cryptographic functions, such protocols enable the classical verifier to enforce consistency in a quantum prover's responses across multiple rounds of interaction. In this work, we demonstrate the first implementation of an interactive quantum advantage protocol, using an ion trap quantum computer. We execute two complementary protocols -- one based upon the learning with errors problem and another where the cryptographic construction implements a computational Bell test. To perform multiple rounds of interaction, we implement mid-circuit measurements on a subset of trapped ion qubits, with subsequent coherent evolution. For both protocols, the performance exceeds the asymptotic bound for classical behavior; maintaining this fidelity at scale would conclusively demonstrate verifiable quantum advantage., Comment: 11 pages, 3 figures; supp. info 23 pages, 4 figures

Recently Chen and Gao~\cite{ChenGao2017} proposed a new quantum algorithm for Boolean polynomial system solving, motivated by the cryptanalysis of some post-quantum cryptosystems. The key idea of their approach is to apply a Quantum Linear System (QLS) algorithm to a Macaulay linear system over $\mathbb{C}$, which is derived from the Boolean polynomial system. The efficiency of their algorithm depends on the condition number of the Macaulay matrix. In this paper, we give a strong lower bound on the condition number as a function of the Hamming weight of the Boolean solution, and show that in many (if not all) cases a Grover-based exhaustive search algorithm outperforms their algorithm. Then, we improve upon Chen and Gao's algorithm by introducing the Boolean Macaulay linear system over $\mathbb{C}$ by reducing the original Macaulay linear system. This improved algorithm could potentially significantly outperform the brute-force algorithm, when the Hamming weight of the solution is logarithmic in the number of Boolean variables. Furthermore, we provide a simple and more elementary proof of correctness for our improved algorithm using a reduction employing the Valiant-Vazirani affine hashing method, and also extend the result to polynomial systems over $\mathbb{F}_q$ improving on subsequent work by Chen, Gao and Yuan \cite{ChenGao2018}. We also suggest a new approach for extracting the solution of the Boolean polynomial system via a generalization of the quantum coupon collector problem \cite{arunachalam2020QuantumCouponCollector}., Comment: 22 pages

While implementing a quantum algorithm it is crucial to reduce the quantum resources, in order to obtain the desired computational advantage. For most fault-tolerant quantum error-correcting codes the cost of implementing the non-Clifford gate is the highest among all the gates in a universal fault-tolerant gate set. In this paper we design provable algorithm to determine T-count of any $n$-qubit ($n\geq 1$) unitary $W$ of size $2^n\times 2^n$, over the Clifford+T gate set. The space and time complexity of our algorithm are $O\left(2^{2n}\right)$ and $O\left(2^{2n\mathcal{T}_{\epsilon}(W)+4n}\right)$ respectively. $\mathcal{T}_{\epsilon}(W)$ ($\epsilon$-T-count) is the (minimum possible) T-count of an exactly implementable unitary $U$ i.e. $\mathcal{T}(U)$, such that $d(U,W)\leq\epsilon$ and $\mathcal{T}(U)\leq\mathcal{T}(U')$ where $U'$ is any exactly implementable unitary with $d(U',W)\leq\epsilon$. $d(.,.)$ is the global phase invariant distance. Our algorithm can also be used to determine the (minimum possible) T-depth of any multi-qubit unitary and the complexity has exponential dependence on $n$ and $\epsilon$-T-depth. This is the first algorithm that gives T-count or T-depth of any multi-qubit ($n\geq 1$) unitary. For small enough $\epsilon$, we can synthesize the T-count and T-depth-optimal circuits. Our results can be used to determine the minimum count (or depth) of non-Clifford gates required to implement any multi-qubit unitary with a universal gate set consisting of Clifford and non-Clifford gates like Clifford+CS, Clifford+V, etc. To the best of our knowledge, there were no such optimal-synthesis algorithm for arbitrary multi-qubit unitaries in any universal gate set., Comment: Accepted for publication in Nature Partner Journal Quantum Information. Not structured according to the journal policies. Compared to v3 : A note about implementation of 2-qubit QFT in Table 3

In our previously published work, we have reported colossal magnetoresistance, Andreev oscillations, ferromagnetism, and granular superconductivity in oxygen-implanted carbon fibers, graphite foils, and highly oriented pyrolytic graphite. In this follow-up research, more results on these oxygen-implanted graphite samples are presented. We show results from transport measurements on oxygen-implanted diamond-like carbon thin coatings, amorphous carbon films, and highly oriented pyrolytic graphite. Significantly, a three-order magnitude drop in the electrical resistance of the oxygen-implanted diamond-like carbon films is observed at the 50 K temperature that we have previously reported for the transition to the superconducting state. Below 50 K, the films resistance oscillates between the high and low resistance states, less when the sample is under a transverse magnetic field. This metastability between the insulating and superconducting-like states possibly reflects the evolution of the amplitude for the superconducting order parameter also known as the longitudinal Higgs mode. Transitions to low resistance state and metastability are also observed for amorphous carbon films. Finally, the highly oriented pyrolytic graphite samples resistance have a thermally activated term that can be understood on the basis of the LAMH model applied to narrow SC channels in which thermal fluctuations can cause phase slips. We also find that in oxygen-implanted carbon materials, the electron charge and spin correlations do not compete and their interplay rather facilitates the emergence of high-temperature superconductivity, and thus, additional unexpected effects like Heisenberg spin waves and magneto-structural transitions are observed., Comment: 10 pages, 6 figures

A proof of quantumness is a type of challenge-response protocol in which a classical verifier can efficiently certify the quantum advantage of an untrusted prover. That is, a quantum prover can correctly answer the verifier's challenges and be accepted, while any polynomial-time classical prover will be rejected with high probability, based on plausible computational assumptions. To answer the verifier's challenges, existing proofs of quantumness typically require the quantum prover to perform a combination of polynomial-size quantum circuits and measurements. In this paper, we give two proof of quantumness constructions in which the prover need only perform constant-depth quantum circuits (and measurements) together with log-depth classical computation. Our first construction is a generic compiler that allows us to translate all existing proofs of quantumness into constant quantum depth versions. Our second construction is based around the learning with rounding problem, and yields circuits with shorter depth and requiring fewer qubits than the generic construction. In addition, the second construction also has some robustness against noise., Comment: 49 pages, 8 figures. Published in Quantum

Warning: This paper contains a mistake, rendering the proof of the main theorem invalid. The logic of Bunched Implications (BI) combines both additive and multiplicative connectives, which include two primitive intuitionistic implications. As a consequence, contexts in the sequent presentation are not lists, nor multisets, but rather tree-like structures called bunches. This additional complexity notwithstanding, the logic has a well-behaved metatheory admitting all the familiar forms of semantics and proof systems. However, the presentation of an effective proof-search procedure has been elusive since the logic's debut. We show that one can reduce the proof-search space for any given sequent to a primitive recursive set, the argument generalizing Gentzen's decidability argument for classical propositional logic and combining key features of Dyckhoff's contraction-elimination argument for intuitionistic logic. An effective proof-search procedure, and hence decidability of provability, follows as a corollary., Comment: Contains a fatal error

We investigate the problem of synthesizing T-depth optimal quantum circuits over the Clifford+T gate set. First we construct a special subset of T-depth 1 unitaries, such that it is possible to express the T-depth-optimal decomposition of any unitary as product of unitaries from this subset and a Clifford (up to global phase). The cardinality of this subset is at most $n\cdot 2^{5.6n}$. We use nested meet-in-the-middle (MITM) technique to develop algorithms for synthesizing provably \emph{depth-optimal} and \emph{T-depth-optimal} circuits for exactly implementable unitaries. Specifically, for synthesizing T-depth-optimal circuits, we get an algorithm with space and time complexity $O\left(\left(4^{n^2}\right)^{\lceil d/c\rceil}\right)$ and $O\left(\left(4^{n^2}\right)^{(c-1)\lceil d/c\rceil}\right)$ respectively, where $d$ is the minimum T-depth and $c\geq 2$ is a constant. This is much better than the complexity of the algorithm by Amy et al.(2013), the previous best with a complexity $O\left(\left(3^n\cdot 2^{kn^2}\right)^{\lceil \frac{d}{2}\rceil}\cdot 2^{kn^2}\right)$, where $k>2.5$ is a constant. We design an even more efficient algorithm for synthesizing T-depth-optimal circuits. The claimed efficiency and optimality depends on some conjectures, which have been inspired from the work of Mosca and Mukhopadhyay (2020). To the best of our knowledge, the conjectures are not related to the previous work. Our algorithm has space and time complexity $poly(n,2^{5.6n},d)$ (or $poly(n^{\log n},2^{5.6n},d)$ under some weaker assumptions)., Comment: Published in Nature Partner Journal Quantum Information. Compared to v4: Minor changes. Not the exact journal version

In this paper, we present results on magnetization properties of boron nitride-carbon (BN-C) and boron carbide-carbon (B4C-C) granular mixtures. The temperature-dependent magnetization for field-cooled during cooling and field-cooled during warming shows a kind of thermal hysteresis that is always seen around a metamagnetic phase transition from an antiferromagnetic martensite to a ferromagnetic austenite phase. The low-temperature magnetization has an upward turn that can be attributed to superparamagnetism, diamagnetic shielding, and trapped flux characteristic to high-temperature superconducting materials. After subtracting the diamagnetic background, the field-dependent magnetization loops M(B) are ferromagnetic-like, more significant for the BN-C than for the B4C-C mixture. In addition, the magnetization loops show the kink feature characteristic to granular superconductivity. The irreversibility temperature for a B4C-C mixture having 37.5 wt% B is Tc = 76 K. Combining our data with previous results on B-doped diamond and Q-carbon, we find that Tc increases linearly with the B concentration., Comment: 5 pages, 10 figures