Strilanc

import collections

import numpy as np
import sinter
import stim
import pathlib

from matplotlib import pyplot as plt

workspace = pathlib.Path("google_qec3v5_experiment_data")

Strilanc

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith

----------------- DEFINE PROBABILITY --------------------
structure Chance where
  p : Rat
  v : (p >= 0) ∧ (p <= 1)

def Chance.le (a b : Chance) : Bool := a.p <= b.p
infixl:45 " ≤ " => Chance.le

Strilanc

import Mathlib
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Rat.Basic
import Mathlib.Data.Rat.Order

theorem le_pin (a b : Nat) (h1 : a <= b) (h2 : b <= a)
  : a = b
  := by
  apply Nat.eq_or_lt_of_le at h1
  cases h : (decide (a = b))

Strilanc

import Mathlib
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Rat.Basic
import Mathlib.Data.Rat.Order

----------------- BASIC DATA TYPES AND COMBINATORS --------------------
structure Odds where
  lose : Nat
  win : Nat
  valid : (lose != 0) ∨ (win != 0)

Strilanc

import math
from typing import Union
from typing import Tuple


def zalka_imul_mod_low_workspace(*, dst: 'Quint', factor: int, modulus: int) -> None:
    """Performs an inplace modular multiplication using n/2 + O(1) workspace."""
    assert factor < modulus
    assert math.gcd(factor, modulus) == 1
    assert len(dst) >= modulus.bit_length() * 3 // 2 + 2

Strilanc

import math
from numpy import array, hstack, vstack
import numpy as np
from PIL import Image


# these two methods were copied from https://github.com/dmishin/fft-image-experiments
def hilbert_indices(N):
    """Genrate 2^N x 2^N integer array, filled with values from 0 to 4^N along hilbert curve"""
    m = array([[0]], dtype=np.int)

Strilanc

from manim import *


class SquareToCircle(Scene):
    def construct(self):
        n = 5
        h = n // 2
        bits = [MathTex("0") for k in range(n)]
        bits2 = [MathTex(f"b_{{{k+1}}}") for k in range(n)]
        dt = 20

Strilanc

from typing import Optional, Dict

import stim

q2_gates = {
    'CNOT',
    'CX',
    'CY',
    'CZ',
    'ISWAP',

Strilanc

{
  "name": "Virtual Lab: New Experiment",
  "grid": {
    "width": 13,
    "height": 10,
    "pieces": [
      {
        "coord": {
          "x": 0,
          "y": 1

Strilanc

import random

import cirq
import numpy as np


def fresh_attempt() -> int:
    a, b = cirq.LineQubit.range(2)
    h_cx_cs_h = cirq.unitary(cirq.Circuit(cirq.H(b), cirq.X(a).controlled_by(b), cirq.S(a).controlled_by(b), cirq.H(b)))
    check_output_tdag_h = cirq.unitary(cirq.Circuit(cirq.T(a) ** -1, cirq.H(a)))