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 csv
import pathlib
import time
from dataclasses import dataclass
from typing import Callable, List, Dict, Any, Set, FrozenSet, Iterable, Tuple
import math
import pymatching
import networkx as nx
import stim
import matplotlib.pyplot as plt

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