arXiv subjects

Ryan Scott

Publications and source records attributed to Ryan Scott.

7 recordsLinked to original sources

arXiv2026

Strong-Drive Floquet Engineering of Interacting Qudits: From Finite-Duration Controls to Emergent Symmetry

Floquet driving uses periodic controls to tailor the behavior of quantum systems, with applications in quantum analogue simulation, sensing, and the protection of quantum information. Most approaches are designed using idealized, instantaneous pulses, even though experiments necessarily use pulses with finite duration and shape. This mismatch becomes especially challenging for interacting $d$-level systems, or qudits, because the number of possible controls grows rapidly with the number of levels. We develop a strong-drive Floquet theory that incorporates experimentally realizable pulse waveforms directly into the design of the effective interactions. The pulse duration, amplitude, and shape therefore become useful control parameters rather than sources of error. We show that systems with more than two levels offer capabilities unavailable in qubit systems: finite-duration driving can create new interactions that are absent from the original system and can substantially change its symmetries. We demonstrate these capabilities for interacting three-level systems. A single pulse transforms a diagonal interaction into a quantum spin-1 model dominated by nematic interactions, while pulse protocols motivated by trapped ultracold polar molecules produce models with enlarged $SU(2)\times U(1)$ and $SU(3)$ symmetries. Numerical tests of both short-time evolution and many-body dynamics confirm the accuracy of the resulting description. Our results provide a scalable analytical framework for designing finite-duration controls in interacting qudit platforms.

quant-ph↗

arXiv2025

Generalized pulse design in Floquet engineering: Application to interacting spin systems

Floquet engineering in quantum simulation employs externally applied high-frequency pulses to dynamically design steady-state effective Hamiltonians. Such protocols can be used to enlarge the space of Hamiltonians but approximations often limit pulse profile shapes and therefore the space of available effective Hamiltonians. We consider a nonstroboscopic high-frequency expansion formalism for Floquet engineering. We generalize the pulse profiles available by rigorously keeping all necessary terms to lowest order in inverse frequency expansions used to derive the effective Hamiltonians. Our approach allows wide tunability in application of external driving fields. We apply our method to long-range interacting XXZ spin Hamiltonians. We model an example application where we derive conditions on specific pulse shapes to engineer effective Ising models from XXZ models. Our method allows the space of continuous pulse profiles, relevant to experimental control fields, to better and more accurately explore possible effective Hamiltonians available for Floquet engineering.

quant-ph↗

arXiv2025

Microring resonator-based photonic circuit for faithfully heralding NOON states

We have designed a Micro-Ring Resonator (MRR) based device that allows for the post-selection of high order NOON states via heralding. NOON states higher than $N=2$ cannot be generated deterministically. By tuning the coupling parameters of the device we can minimize the amplitudes of the 'accidental' states to maximize the probability of obtaining the NOON state upon a successful heralding event. Our device can produce a 3-photon NOON state output with 100% certainty upon a successful heralding detection, which occurs with probability $\frac{8}{27}$ for optimal tunable device parameters. A successful heralding event allows for non-destructive time of flight tracking of the NOON state thus establishing a significantly enhanced level of engineering control for integration of the NOON state into scalable systems for quantum sensing and metrology. We further discuss extensions of our technique to even higher NOON states having $N=4,5$.

quant-ph↗

arXiv2024

Crux, a Precise Verifier for Rust and Other Languages

We present Crux, a cross-language verification tool for Rust and C/LLVM. Crux targets bounded, intricate pieces of code that are difficult for humans to get right: for example, cryptographic modules and serializer / deserializer pairs. Crux builds on the same framework as the mature SAW-Cryptol toolchain, but Crux provides an interface where proofs are phrased as symbolic unit tests. Crux is designed for use in production environments, and has already seen use in industry. In this paper, we focus on Crux-MIR, our verification tool for Rust. Crux-MIR provides a bit-precise model of safe and unsafe Rust which can be used to check both inline properties about Rust code, and extensional equality to executable specifications written in Cryptol or in the hacspec dialect of Rust. Notably, Crux-MIR supports compositional reasoning, which is necessary to scale to even moderately complex proofs. We demonstrate Crux-MIR by verifying the Ring library implementations of SHA1 and SHA2 against pre-existing functional specifications. Crux is available at https://crux.galois.com.

cs.PL↗

arXiv2023

Quantum simulation costs for Suzuki-Trotter decomposition of quantum many-body lattice models

Quantum computers offer the potential to efficiently simulate the dynamics of quantum systems, a task whose difficulty scales exponentially with system size on classical devices. To assess the potential for near-term quantum computers to simulate many-body systems we develop a formalism to straightforwardly compute bounds on the number of Trotter steps needed to accurately simulate the time evolution of fermionic lattice models based on the first-order commutator scaling. We apply this formalism to two closely related many-body models prominent in condensed matter physics, the Hubbard and t-J models. We find that, while a naive comparison of the Trotter depth first seems to favor the Hubbard model, careful consideration of the model parameters and the allowable error for accurate simulation leads to a substantial advantage in favor of the t-J model. These results and formalism set the stage for significant improvements in quantum simulation costs.

quant-ph↗

arXiv2022

Hybrid quantum gap estimation algorithm using a filtered time series

Quantum simulation advantage over classical memory limitations would allow compact quantum circuits to yield insight into intractable quantum many-body problems, but the interrelated obstacles of large circuit depth in quantum time evolution and noise seem to rule out unbiased quantum simulation in the near term. We prove that classical post-processing, i.e., long-time filtering of an offline time series, exponentially improves the circuit depth needed for quantum time evolution. We apply the filtering method to the construction of a hybrid quantum-classical algorithm to estimate energy gap, an important observable not governed by the variational theorem. We demonstrate, within an operating range of filtering, the success of the algorithm in proof-of-concept simulation for finite-size scaling of a minimal spin model. Our findings set the stage for unbiased quantum simulation to offer memory advantage in the near term.

quant-ph↗

arXiv2017

Deriving Law-Abiding Instances

Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. But many of these proofs require routine, boilerplate code that is tedious to write. Moreover, many such proofs do not scale well, as the size of proof terms can grow superlinearly with the size of the datatypes involved in the proofs. We present a technique for programming with refinement reflection which solves this problem by leveraging datatype-generic programming. Our observation is that we can take any algebraic datatype, generate an equivalent representation type, and have Liquid Haskell automatically construct (and prove) an isomorphism between the original type and the representation type. This reduces many proofs down to easy theorems over simple algebraic "building block" types, allowing programmers to write generic proofs cheaply and cheerfully.

cs.PL↗