def babbush_shor : ShorAlgorithm

def babbush_code : QECCode

def babbush_hw : QualtranPhysicalParameters

def babbush_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : babbush_instance.1.q_A = 8

example : babbush_instance.2.1.n = 425 ∧
          babbush_instance.2.1.k = 1 ∧
          babbush_instance.2.1.d = 14

example : babbush_instance.2.2 = gidney_fowler_realistic

def cainxu_shor : ShorAlgorithm

def cainxu_code : QECCode

def cainxu_hw : QualtranPhysicalParameters

def cainxu_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : cainxu_instance.1.q_A = 33

example : cainxu_instance.2.1.n = 144 ∧
          cainxu_instance.2.1.k = 12 ∧
          cainxu_instance.2.1.d = 12

example : cainxu_instance.2.2.physical_error_thousandths = 1

def makeRow (positions : List Nat) (n : Nat) : List Bool

def bb_first_x_check : List Bool

example : bb_first_x_check.length = 144

example : (bb_first_x_check.filter id).length = 6

def memoryBlocks (q_A k_m : Nat) : Nat

def qubitLower (q_A n_m k_m : Nat) : Nat

def qubitUpper (N_m N_p N_f N_A N_res : Nat) : Nat

def perToffoli (tau_s cycle : Nat) : Nat

def timeLower (depth tau_s cycle : Nat) : Nat

def timeUpper (toff tau_s cycle : Nat) : Nat

theorem qubit_lower_le_upper (q_A n_m k_m N_m N_p N_f N_A N_res : Nat)
    (hmem : qubitLower q_A n_m k_m ≤ N_m) :
    qubitLower q_A n_m k_m ≤ qubitUpper N_m N_p N_f N_A N_res

theorem time_lower_le_upper (depth toff tau_s cycle : Nat) (h : depth ≤ toff) :
    timeLower depth tau_s cycle ≤ timeUpper toff tau_s cycle

theorem time_floor_all_schedules (depth tau_s cycle : Nat) (begin_ : Nat → Nat)
    (hdep : ∀ i, begin_ i + perToffoli tau_s cycle ≤ begin_ (i + 1)) :
    begin_ 0 + timeLower depth tau_s cycle ≤ begin_ depth

def qianxu_qubit_bounds : ResourceBounds

theorem qianxu_qubit_bracketed : qianxu_qubit_bounds.bracketed = true

theorem qianxu_qubit_gap : qianxu_qubit_bounds.optimizationGap = 4_839

theorem qianxu_qubit_floor : qianxu_qubit_bounds.lower = 4350

def qianxu_time_bounds : ResourceBounds

theorem qianxu_time_bracketed : qianxu_time_bounds.bracketed = true

theorem qianxu_time_gap : qianxu_time_bounds.optimizationGap = 12_870_000_000

theorem qianxu_time_respects_floor : qianxu_time_bounds.respectsFloor = true

theorem bb18_k_derived : derivedK bb18 = 10

theorem bb18_n : bb18.n = 248

theorem bb18_k_matches_paper : derivedK bb18 = 10

theorem lp16_k_derived : lp16.n - rank lp16.hx - rank lp16.hz = 744

def lp20_n : Nat

theorem lp20_k_derived : lp20.n - rank lp20.hx - rank lp20.hz = 1224

def lp20_k : Nat

def lp20_d : Nat

def lp20_qubit_bounds : ResourceBounds

theorem lp20_qubit_bracketed : lp20_qubit_bounds.bracketed = true

theorem lp20_qubit_gap : lp20_qubit_bounds.optimizationGap = 4_961

def lp20_time_bounds : ResourceBounds

theorem lp20_time_bracketed : lp20_time_bounds.bracketed = true

theorem lp20_time_gap : lp20_time_bounds.optimizationGap = 12_987_000_000_000

theorem full_lp_report :
    lp16.n - rank lp16.hx - rank lp16.hz = 744
    ∧ lp20_qubit_bounds.bracketed = true ∧ lp20_qubit_bounds.optimizationGap = 4_961
    ∧ lp20_time_bounds.bracketed = true

def lpGadgetTauS : Nat

theorem lpGadgetTauS_eq : lpGadgetTauS = 4

theorem lpGadget_footprint : surgeryPhysQubits bb_x_surgery = 39

theorem lpGadget_total_meas : surgeryTotalMeas bb_x_surgery = 80

theorem perPPM_time_from_verified_gadget (cycle : Nat) :
    perToffoli (surgeryRounds bb_x_surgery) cycle = bb_x_surgery.tau_s * cycle

theorem lpGadget_tau_is_verified :
    SurgeryGadget.verify_surgery_gadget bb_x_surgery = true
    ∧ surgeryRounds bb_x_surgery = bb_x_surgery.tau_s

theorem resource_grounded_in_verified_gadget (cycle : Nat) :
    SurgeryGadget.verify_surgery_gadget bb_x_surgery = true
    ∧ perToffoli (surgeryRounds bb_x_surgery) cycle = bb_x_surgery.tau_s * cycle
    ∧ surgeryPhysQubits bb_x_surgery = 39

def runPPMs (ps : List PauliString) (s : StabilizerState) : StabilizerState

def afterBothMeasured : StabilizerState

theorem computation_measures_both : runPPMs [zbar 0, zbar 1] bbCodeState = afterBothMeasured

theorem computation_order_independent :
    runPPMs [zbar 0, zbar 1] bbCodeState = runPPMs [zbar 1, zbar 0] bbCodeState

def computationTimeUs (numPPMs tau_s cycle : Nat) : Nat

def computationQubits (n_m N_A factory : Nat) : Nat

theorem computationTime_mono (p p' tau_s cycle : Nat) (h : p ≤ p') :
    computationTimeUs p tau_s cycle ≤ computationTimeUs p' tau_s cycle

theorem lp20_computation_time : computationTimeUs 1_000_000_000 13 1000 = 13_000_000_000_000

theorem lp20_computation_qubits : computationQubits 4350 894 2565 = 7809

theorem lp20_computation_resource :
    runPPMs [zbar 0, zbar 1] bbCodeState = afterBothMeasured
    ∧ computationTimeUs 1_000_000_000 13 1000 = 13_000_000_000_000
    ∧ computationQubits 4350 894 2565 = 7809

def lpBlock : List SysCall

def lpFullSched (N : Nat) : List SysCall

theorem lpBlock_capacity      : capacity_in_arch_ok lpArch lpBlock = true

theorem lpBlock_capacityCycle : capacity_per_cycle_ok lpArch lpBlock = true

theorem lpBlock_exclusive     : exclusivity_ok lpBlock = true

theorem lpBlock_decoder       : decoder_react_ok 10 lpBlock = true

theorem lpBlock_within        : scheduleWithinWallclock lpBlock = true

theorem lpBlock_magicfree :
    (lpBlock.filter (fun sc => kindIsMagicReq sc.kind)).length = 0

theorem full_modexp_schedule_valid (N : Nat) :
    capacity_in_arch_ok lpArch (lpFullSched N) = true
    ∧ capacity_per_cycle_ok lpArch (lpFullSched N) = true
    ∧ exclusivity_ok (lpFullSched N) = true
    ∧ decoder_react_ok 10 (lpFullSched N) = true
    ∧ window_throughput_ok (lpFullSched N) 12000 1 = true

theorem full_modexp_10e9_schedule_valid :
    capacity_in_arch_ok lpArch (lpFullSched 1_000_000_000) = true
    ∧ capacity_per_cycle_ok lpArch (lpFullSched 1_000_000_000) = true
    ∧ exclusivity_ok (lpFullSched 1_000_000_000) = true
    ∧ decoder_react_ok 10 (lpFullSched 1_000_000_000) = true
    ∧ window_throughput_ok (lpFullSched 1_000_000_000) 12000 1 = true

theorem full_modexp_schedule_conflict_free (N : Nat) :
    exclusivity_ok (lpFullSched N) = true
    ∧ capacity_in_arch_ok lpArch (lpFullSched N) = true
    ∧ (lp_runtime_us / lp_factory_window_us) * lp_factory_per_window ≥ lp_magic_demand

def bbLogX0 : BoolVec

def bb_x_surgery : SurgeryGadget

theorem bb_x_surgery_dimensions :
    SurgeryGadget.dimensions_consistent bb_x_surgery = true

theorem bb_x_surgery_tau_s :
    SurgeryGadget.tau_s_sufficient bb_x_surgery = true

theorem bb_x_surgery_qldpc :
    SurgeryGadget.merged_is_qldpc bb_x_surgery = true

theorem bb_x_surgery_targets_correctly :
    SurgeryGadget.targets_logical_correctly bb_x_surgery = true

theorem bb_x_surgery_verifies :
    SurgeryGadget.verify_surgery_gadget bb_x_surgery = true

theorem bb_surgery_target_is_logical :
    (bbSmall.hz.all (fun r => ! gf2dot r bbLogX0) && ! inRowspace bbSmall.hx bbLogX0) = true

theorem bb_LP_surgery_implements_logical_X
    (signs : List Bool) (hsig : signs.length = bb_x_surgery.merged_hx.length) :
    (selectedSignedProduct bb_x_surgery.span_witness bb_x_surgery.merged_hx signs
        = signedXRow (selectedParity bb_x_surgery.span_witness signs) bb_x_surgery.target_pauli)
    ∧ (∀ (L : PauliString) (s : StabilizerState), L ∈ s →
        (∀ P ∈ merged_stabilizers_X bb_x_surgery, L.commutes P = true) →
        L ∈ measureChecks (merged_stabilizers_X bb_x_surgery) s)
    ∧ (∀ p ∈ merged_stabilizers_X bb_x_surgery, ∀ q ∈ merged_stabilizers_X bb_x_surgery,
        p.commutes q = true)

theorem LP_code_has_verified_surgery :
    SurgeryGadget.verify_surgery_gadget bb_x_surgery = true
    ∧ (bbSmall.hz.all (fun r => ! gf2dot r bbLogX0) && ! inRowspace bbSmall.hx bbLogX0) = true

def lp_memory : ArchZone

def lp_operation : ArchZone

def lp_factory : ArchZone

def lpArch : ZonedArch

theorem lp_zones_partition :
    lp_memory.capacity + lp_operation.capacity + lp_factory.capacity = 7809

theorem lp_total_is_upper_bound :
    lpArch.total_sites
      = FormalRV.Audit.CainXu2026.QianxuVerifiedUpperBound.upperQubits 4350 894 2565

def lp_factory_window_us : Nat

def lp_factory_per_window : Nat

def lp_magic_demand : Nat

def lp_runtime_us   : Nat

theorem lp_factory_throughput_adequate :
    (lp_runtime_us / lp_factory_window_us) * lp_factory_per_window ≥ lp_magic_demand

def lpSched : List SysCall

def lpCtx : SystemCtx

theorem lpCtx_all_invariants : checkAll baseInvariants lpCtx = true

theorem lp_atoms_exclusive : exclusivity_ok lpSched = true

theorem lp_capacity_ok :
    capacity_in_arch_ok lpArch lpSched = true
    ∧ capacity_per_cycle_ok lpArch lpSched = true

def lp_overflow_sched : List SysCall

def lp_overflow_ctx : SystemCtx

theorem lp_overflow_rejected : checkAll baseInvariants lp_overflow_ctx = false

theorem lp_system_realises_upper_bound :
    lp_memory.capacity + lp_operation.capacity + lp_factory.capacity = 7809
    ∧ (lp_runtime_us / lp_factory_window_us) * lp_factory_per_window ≥ lp_magic_demand
    ∧ checkAll baseInvariants lpCtx = true
    ∧ checkAll baseInvariants lp_overflow_ctx = false

def codeStabs : List PauliString

theorem codeStabs_sub_state (g : PauliString) (hg : g ∈ codeStabs) : g ∈ bbCodeState

theorem codeStabs_commute_logZ :
    ∀ g ∈ codeStabs, g.commutes (zbar 0) = true ∧ g.commutes (zbar 1) = true

theorem modexp_preserves_code
    (ps : List PauliString)
    (halpha : ∀ P ∈ ps, P = zbar 0 ∨ P = zbar 1)
    (g : PauliString) (hg : g ∈ codeStabs) :
    g ∈ runPPMs ps bbCodeState

theorem logical_computation_preserves_code
    (ps : List PauliString)
    (hlog : ∀ P ∈ ps, ∀ g ∈ codeStabs, g.commutes P = true)
    (g : PauliString) (hg : g ∈ codeStabs) :
    g ∈ runPPMs ps bbCodeState

theorem modexp_preserves_code'
    (ps : List PauliString) (halpha : ∀ P ∈ ps, P = zbar 0 ∨ P = zbar 1)
    (g : PauliString) (hg : g ∈ codeStabs) :
    g ∈ runPPMs ps bbCodeState

theorem modexp_preserves_Xchecks
    (ps : List PauliString) (halpha : ∀ P ∈ ps, P = zbar 0 ∨ P = zbar 1)
    (r : BoolVec) (hr : r ∈ bbSmall.hx) :
    xRow r ∈ runPPMs ps bbCodeState

def modexpPPMs (numToffoli ppmPerToffoli : Nat) : Nat

theorem modexpPPMs_mono (t t' p : Nat) (h : t ≤ t') :
    modexpPPMs t p ≤ modexpPPMs t' p

def modexpTimeUs (numToffoli ppmPerToffoli tau_s cycle : Nat) : Nat

theorem lp20_modexp_time :
    modexpTimeUs 1_000_000_000 1 13 1000 = 13_000_000_000_000

theorem full_modexp_on_LP :
    (∀ (ps : List PauliString), (∀ P ∈ ps, P = zbar 0 ∨ P = zbar 1) →
        ∀ g ∈ codeStabs, g ∈ runPPMs ps bbCodeState)
    ∧ apply_PPM_pos bbCodeState (zbar 0) = afterMeasureZ0
    ∧ modexpTimeUs 1_000_000_000 1 13 1000 = 13_000_000_000_000
    ∧ computationQubits 4350 894 2565 = 7809

def naivePPMonLP_qubits (data_n ancilla_n : Nat) : Nat

theorem naivePPMonLP_within_upper (data_n ancilla_n N_m N_p N_f N_A N_res : Nat)
    (hd : data_n ≤ N_m) (ha : ancilla_n ≤ N_A) :
    naivePPMonLP_qubits data_n ancilla_n ≤ qubitUpper N_m N_p N_f N_A N_res

theorem qianxu_naivePPM_footprint : naivePPMonLP_qubits 4350 894 = 5244

def naiveSequentialDepth (toffCount : Nat) : Nat

theorem naiveSequential_is_timeUpper (toffCount tau_s cycle : Nat) :
    timeLower (naiveSequentialDepth toffCount) tau_s cycle = timeUpper toffCount tau_s cycle

def parallelSpeedup (toffCount D_par : Nat) : Nat

theorem qianxu_parallel_speedup : parallelSpeedup 1_000_000 10_000 = 100

theorem naive_constructions_justify_upper_bounds (tau_s cycle : Nat) :
    -- (b) the sequential construction = the time upper bound, for any count:
    (∀ toffCount, timeLower (naiveSequentialDepth toffCount) tau_s cycle
        = timeUpper toffCount tau_s cycle)
    -- (a) the qianxu naive PPM footprint is the memory+ancilla contribution:
    ∧ naivePPMonLP_qubits 4350 894 = 5244

def xbar (i : Nat) : PauliString

def zbar (i : Nat) : PauliString

def bbCodeState : StabilizerState

def afterMeasureZ0 : StabilizerState

theorem bbCodeState_valid : StabilizerState.valid bbCodeState bbSmall.n = true

theorem naive_PPM_measures_logical_Z0 :
    apply_PPM_pos bbCodeState (zbar 0) = afterMeasureZ0

theorem naive_PPM_preserves_others :
    (afterMeasureZ0.drop 0).take (bbSmall.hx.length + bbSmall.hz.length)
      = bbCodeState.take (bbSmall.hx.length + bbSmall.hz.length)
    ∧ xbar 1 ∈ afterMeasureZ0

theorem ppm_on_LP_is_verified :
    StabilizerState.valid bbCodeState bbSmall.n = true
    ∧ apply_PPM_pos bbCodeState (zbar 0) = afterMeasureZ0

def upperTimeUs (numPPMs tau_s cycle : Nat) : Nat

def upperQubits (n_LP N_A factory : Nat) : Nat

theorem upperTime_dominates (depth numPPMs tau_s cycle : Nat) (h : depth ≤ numPPMs) :
    depth * tau_s * cycle ≤ upperTimeUs numPPMs tau_s cycle

theorem qianxu_upper_bound_verified
    (c : CSSCode) (k : Nat) (L : LogicalBasis c k) (hv : L.valid = true)
    (ps : List PauliString) (hps : ∀ P ∈ ps, ∃ i : Fin k, P = L.zbar i)
    (tau_s cycle : Nat) :
    (∀ g ∈ c.hx.map CSSCode.xStab ++ c.hz.map CSSCode.zStab,
        g ∈ measureChecks ps (codeStateWithLogicals c k L))
    ∧ (∀ depth, depth ≤ ps.length →
        depth * tau_s * cycle ≤ upperTimeUs ps.length tau_s cycle)

theorem bb_ps_are_logicalZ :
    ∀ P ∈ [bbSmallLogicalBasis.zbar 0, bbSmallLogicalBasis.zbar 1],
      ∃ i : Fin 2, P = bbSmallLogicalBasis.zbar i

theorem bbSmall_upper_bound_verified (tau_s cycle : Nat) :
    (∀ g ∈ bbSmall.hx.map CSSCode.xStab ++ bbSmall.hz.map CSSCode.zStab,
        g ∈ measureChecks [bbSmallLogicalBasis.zbar 0, bbSmallLogicalBasis.zbar 1]
              (codeStateWithLogicals bbSmall 2 bbSmallLogicalBasis))
    ∧ (∀ depth, depth ≤ 2 → depth * tau_s * cycle ≤ upperTimeUs 2 tau_s cycle)

theorem lp20_qubit_upper : upperQubits 4350 894 2565 = 7809

theorem lp20_time_upper : upperTimeUs 1_000_000_000 13 1000 = 13_000_000_000_000

theorem qianxu_verified_upper_bound :
    -- semantics on the real code (instantiated, decide @18q)
    (∀ g ∈ bbSmall.hx.map CSSCode.xStab ++ bbSmall.hz.map CSSCode.zStab,
        g ∈ measureChecks [bbSmallLogicalBasis.zbar 0, bbSmallLogicalBasis.zbar 1]
              (codeStateWithLogicals bbSmall 2 bbSmallLogicalBasis))
    -- the lp_20 upper-bound figures
    ∧ upperQubits 4350 894 2565 = 7809
    ∧ upperTimeUs 1_000_000_000 13 1000 = 13_000_000_000_000

def pauliSupport (P : PauliString) : BoolVec

structure Certificate (code : CSSCode)

def acceptsCore (code : CSSCode) (k : Nat) (basis : LogicalBasis code k) : Bool

theorem acceptsCore_iff (code : CSSCode) (cert : Certificate code) :
    acceptsCore code cert.k cert.basis = true

theorem bbSmall_core_accepted :
    acceptsCore bbSmall 2 bbSmallLogicalBasis = true

def bogusBasis : LogicalBasis bbSmall 2

theorem bogus_rejected : acceptsCore bbSmall 2 bogusBasis = false

theorem bogus_basis_invalid : bogusBasis.valid = false

theorem shor_on_LP_code
    (F : TFactoryContract)
    (a r N m bits ainv x : Nat)
    (h_setting : ShorSetting a r N m bits)
    (h_sizing : CircuitSizing N bits)
    (h_inv : a * ainv % N = 1)
    (h_ainv_le : ainv ≤ N) (hx : x < N)
    (ps : List PauliString)
    (hlog : ∀ P ∈ ps, ∀ g ∈ codeStabs, g.commutes P = true) :
    -- (A) ALGORITHM SUCCESS + a^x-mod-N ARITHMETIC (the modular multiplier PPM-realised):
    ( FormalRV.SQIRPort.probability_of_success a r N m bits
          (ModMul.ancillaWidth bits) (ModMul.circuitFamily a ainv N bits)

theorem multiplier_gateset_bridges_to_LP
    (F : TFactoryContract) (g : Gate) (hICX : isICXGate g = true) (f : Nat → Bool)
    (σ' : MagicBasisPPMState)
    (hrun : PPMProgramRel
              (magicBasisPPMSemanticsModel F)
              (compileArithmeticGateToPPM g)
              (magicBasisEncodeBits F f) σ')
    (a b c : Nat) (hac : a ≠ c) (hbc : b ≠ c)
    (s t : MagicBasisPPMState) (h : teleportCCXRel F a b c s t) :
    -- Clifford fragment reduces to the Boolean PPM run (seam 6):
    σ'.bits = Gate.applyNat g f
    -- Toffoli grounded in the verified 8T→CCZ→Toffoli circuit (seam 5):

def gidney2025_shor : ShorAlgorithm

def gidney2025_code : QECCode

def gidney2025_hw : QualtranPhysicalParameters

def gidney2025_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : gidney2025_instance.1.q_A = 8

example : gidney2025_instance.2.1.n = 1352 ∧
          gidney2025_instance.2.1.k = 1 ∧
          gidney2025_instance.2.1.d = 25

example : gidney2025_instance.2.2 = gidney_fowler_realistic

def gidney2025_work : Workload

def gidney2025_cold_physical_per_logical : Nat

theorem gidney2025_logical_tally : 1280 + 131 + 7 * 18 = 1537

theorem gidney2025_input_qubits : 2048 / 2 + 2048 / 8 = 1280

theorem gidney2025_window_counts :
    (1280 + 6 - 1) / 6 = 214 ∧ (21 + 3 - 1) / 3 = 7 ∧ (21 + 5 - 1) / 5 = 5

theorem gidney2025_physical_tally :
    1280 * 430 + 131 * 1352 + 7 * 18 * 1352 = 897864

theorem gidney2025_hot_patch_size : 2 * (25 + 1) ^ 2 = 1352

theorem gidney2025_work_consistent :
    gidney2025_work.n_logical = 1280 + 131 + 7 * 18

theorem gidney2025_lookup_ccz : 2 ^ 6 - 6 - 1 = 57

theorem gidney2025_ccz_period : 150 / 6 = 25

theorem gidney2025_slack : 897864 < 1000000 ∧ 1000000 - 897864 = 102136

theorem gidney2025_vs_ge2021_qubit_cut : 897864 * 22 < 20000000

theorem gidney2025_vs_ge2021_toffoli : 2_700_000_000 * 2 < 6_500_000_000

theorem gidney2025_vs_cfs24_toffoli : 300 * 6_500_000_000 < 2_000_000_000_000

def g2025_add_toffoli (n : Nat) : Nat

def g2025_lookup_toffoli (n : Nat) : Nat

def g2025_modadd_toffoli_halves (n : Nat) : Nat

theorem g2025_loop4_add_ccz : g2025_add_toffoli 33 = 32

theorem g2025_loop1_lookup_ccz : g2025_lookup_toffoli 6 = 57

theorem g2025_modadd_beats_berry (n : Nat) (hn : 0 < n) :
    g2025_modadd_toffoli_halves n < 7 * n

def decoderBacklogInv (patches decodeLatency lanes : Nat) : SpaceTimeInvariant

def ge2021DecoderInv (lanes : Nat) : SpaceTimeInvariant

theorem ge2021_fully_valid_with_decoder :
    checkAll (baseInvariants ++ [causalityInv shorDeps, ge2021DecoderInv 62_000]) ge2021Ctx = true

theorem ge2021_underprovisioned_decoder_rejected :
    checkAll (baseInvariants ++ [ge2021DecoderInv 6200]) ge2021Ctx = false

theorem ge2021_decoder_is_the_culprit :
    checkAll baseInvariants ge2021Ctx = true
    ∧ (ge2021DecoderInv 6200).check ge2021Ctx = false

theorem decoder_inv_composes (lanes : Nat) :
    checkAll (baseInvariants ++ [ge2021DecoderInv lanes]) ge2021Ctx
      = (checkAll baseInvariants ge2021Ctx && (ge2021DecoderInv lanes).check ge2021Ctx)

def ge2021_shor : ShorAlgorithm

def ge2021_code : QECCode

def ge2021_hw : QualtranPhysicalParameters

def ge2021_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : ge2021_instance.1.q_A = 3072

example : ge2021_instance.2.1.n = 1568 ∧
          ge2021_instance.2.1.k = 1 ∧
          ge2021_instance.2.1.d = 27

example : ge2021_instance.2.2 = gidney_fowler_realistic

def ge2021_distance        : Nat

def ge2021_tile_qubits     : Nat

def ge2021_logical_qubits  : Nat

def ge2021_cycle_us        : Nat

def ge2021_total_budget    : Nat

def ge2021_computation_size : Nat

def ge2021_factory_size     : Nat

def ge2021_computation : ArchZone

def ge2021_factory : ArchZone

def ge2021Arch : ZonedArch

theorem computation_capacity : ge2021_computation.capacity = 9_721_600

theorem factory_capacity : ge2021_factory.capacity = 10_278_400

theorem zones_partition_budget :
    ge2021_computation.capacity + ge2021_factory.capacity = ge2021_total_budget

theorem total_is_reported : ge2021Arch.total_sites = 20_000_000

theorem data_block_fits :
    ge2021_logical_qubits * ge2021_tile_qubits ≤ ge2021_computation.capacity

theorem budget_matches_reproduction :
    ge2021Arch.total_sites = FormalRV.System.NaiveUpperBound.ge2021_reported_qubits

def ge2021Ctx : SystemCtx

theorem ge2021Ctx_resource_ok : checkAll baseInvariants ge2021Ctx = true

theorem ge2021Ctx_fully_valid :
    checkAll (baseInvariants ++ [causalityInv shorDeps]) ge2021Ctx = true

def ge2021_overflow_sched : List SysCall

def ge2021_overflow_ctx : SystemCtx

theorem ge2021_overflow_rejected :
    checkAll baseInvariants ge2021_overflow_ctx = false

theorem ge2021_distance_is_verified_code :
    (surfaceCodeD 27).d = 27 ∧ (surfaceCodeD 27).k = 1 ∧ (surfaceCodeD 27).n = 1405

theorem ge2021_qubits_derived : ge2021_naive.qubits = 19_443_200

theorem ge2021_qubits_reproduce_reported :
    ge2021_naive.qubits ≤ ge2021_reported_qubits
    ∧ ge2021_reported_qubits - ge2021_naive.qubits ≤ 600_000

theorem ge2021_time_ceiling : ge2021_naive.time_us_tenths = 729_000_000_000

theorem ge2021_time_gap_2_to_3x :
    2 * ge2021_reported_time_us_tenths ≤ ge2021_naive.time_us_tenths
    ∧ ge2021_naive.time_us_tenths ≤ 3 * ge2021_reported_time_us_tenths

theorem gidney_ekera_2021_reproduced :
    (ge2021_naive.qubits ≤ ge2021_reported_qubits
      ∧ ge2021_reported_qubits - ge2021_naive.qubits ≤ 600_000)
    ∧ (2 * ge2021_reported_time_us_tenths ≤ ge2021_naive.time_us_tenths
      ∧ ge2021_naive.time_us_tenths ≤ 3 * ge2021_reported_time_us_tenths)

def toffoliCount : Nat

def perToffoliUs : Nat

theorem perToffoliUs_value : perToffoliUs = 12054

def naiveWallclockUs : Nat

def naiveWallclockHours : Nat

theorem naiveWallclockHours_value : naiveWallclockHours = 8782

def naiveQubits : Nat

theorem naiveQubits_value : naiveQubits = 9636357

theorem time_gap :
    1097 * gidney_ekera_2021_rsa2048_wallclock_hours ≤ naiveWallclockHours
    ∧ naiveWallclockHours ≤ 1098 * gidney_ekera_2021_rsa2048_wallclock_hours

theorem qubit_gap :
    naiveQubits < gidney_ekera_2021_rsa2048_physical_qubits
    ∧ 2 * naiveQubits ≤ gidney_ekera_2021_rsa2048_physical_qubits

theorem spacetime_gap :
    528 * (gidney_ekera_2021_rsa2048_physical_qubits * gidney_ekera_2021_rsa2048_wallclock_hours)
        ≤ naiveQubits * naiveWallclockHours
    ∧ naiveQubits * naiveWallclockHours
        ≤ 530 * (gidney_ekera_2021_rsa2048_physical_qubits * gidney_ekera_2021_rsa2048_wallclock_hours)

def dev : Device

def shorFragment : DSchedule

theorem shorFragment_valid : scheduleValid dev shorFragment = true

theorem shorFragment_parallel :
    (opsTimeOverlap shorFragment[0]! shorFragment[1]! = true)        -- preps overlap in time
    ∧ (opsTimeOverlap shorFragment[2]! shorFragment[3]! = true)      -- teleports overlap in time
    ∧ conflictFree shorFragment = true

theorem reject_consume_before_ready :
    scheduleValid dev
      (shorFragment.set 2 { shorFragment[2]! with begin_t

theorem reject_overlapping_ancilla :
    scheduleValid dev
      (shorFragment.set 3 { shorFragment[3]! with footprint

theorem reject_decoder_oversubscribed :
    scheduleValid dev
      (shorFragment ++ [{ id

theorem reject_reaction_exceeded :
    scheduleValid dev
      (shorFragment.set 4 { shorFragment[4]! with dur_t

theorem shorFragment_preserves_placement (p0 : Placement) :
    evolvePlacement shorFragment p0 = p0

def magicOpCount (sched : DSchedule) : Nat

theorem shorFragment_magicOpCount : magicOpCount shorFragment = 2

theorem rsa2048_schedule_budget :
    FormalRV.System.MagicScheduleComplete.rsa2048_magic_budget = 2622824448
    ∧ FormalRV.System.MagicScheduleComplete.rsa2048_factories = 1093
    ∧ FormalRV.Audit.GidneyEkera2021.WindowedShorPhysicalEstimate.windowedPhysicalDataQubits_rsa2048 = 9633792

def surfaceCodePatchQubits (d : Nat) : Nat

theorem surfaceCodePatchQubits_ge2021 :
    surfaceCodePatchQubits ge2021_code.d = ge2021_code.n

def physicalDataQubits (logicalQubits d : Nat) : Nat

abbrev windowedLogicalQubits (n : Nat) : Nat

theorem windowedLogicalQubits_rsa2048 : windowedLogicalQubits 2048 = 6144

def windowedPhysicalDataQubits_rsa2048 : Nat

theorem windowedPhysicalDataQubits_rsa2048_value :
    windowedPhysicalDataQubits_rsa2048 = 9633792

theorem windowedPhysicalDataQubits_rsa2048_within_paper :
    windowedPhysicalDataQubits_rsa2048 ≤ gidney_ekera_2021_rsa2048_physical_qubits
    ∧ gidney_ekera_2021_rsa2048_physical_qubits ≤ 3 * windowedPhysicalDataQubits_rsa2048

def ge2021_cycle_time_us : Nat

theorem ge2021_cycle_time_us_value : ge2021_cycle_time_us = 1

def windowedMeasLayers_rsa2048 : Nat

theorem windowedMeasLayers_rsa2048_value : windowedMeasLayers_rsa2048 = 2143289344

def runtimeHours (measLayers reactionTimeUs : Nat) : Nat

theorem windowedRuntime_rsa2048_brackets_paper :
    runtimeHours windowedMeasLayers_rsa2048 13 ≤ gidney_ekera_2021_rsa2048_wallclock_hours
    ∧ gidney_ekera_2021_rsa2048_wallclock_hours ≤ runtimeHours windowedMeasLayers_rsa2048 15

def ge2021_arch : ZonedArch

theorem ge2021_arch_cycle_matches_hw :
    ge2021_arch.t_cycle_us = ge2021_cycle_time_us

theorem windowed_magic_schedule_invariants_ge2021 :
    all_invariants_ok ge2021_arch (factoryRequestSchedule 0 2 16) 1000 1000 (fun _ => 0) = true

def peng_shor : ShorAlgorithm

def peng_code : QECCode

def peng_hw : QualtranPhysicalParameters

def peng_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : peng_instance.1.q_A = 1

example : peng_instance.2.1.n = 1 ∧
          peng_instance.2.1.k = 1 ∧
          peng_instance.2.1.d = 1

example : peng_instance.2.2 = default_params

def pinnacle_gb_72 : FormalRV.QEC.CSSCode

theorem pinnacle_gb_72_n : pinnacle_gb_72.n = 72

theorem pinnacle_gb_72_css : pinnacle_gb_72.css_condition = true

theorem pinnacle_gb_72_k_derived : derivedK pinnacle_gb_72 = 12

theorem pinnacle_rsa_code_recorded :
    FormalRV.Audit.Pinnacle.Webster2026.webster_code.n = 1620 ∧
    FormalRV.Audit.Pinnacle.Webster2026.webster_code.k = 16 ∧
    FormalRV.Audit.Pinnacle.Webster2026.webster_code.d = 24

def webster_shor : ShorAlgorithm

def webster_code : QECCode

def webster_hw : QualtranPhysicalParameters

def webster_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : webster_instance.1.q_A = 3072

example : webster_instance.2.1.n = 1620 ∧
          webster_instance.2.1.k = 16 ∧
          webster_instance.2.1.d = 24

example : webster_instance.2.2.physical_error_thousandths = 1

example : FormalRV.Audit.Xu2024.Xu2024.xu2024_hw.cycle_time_us_tenths = 24000 * 10

def xu2024_shor : ShorAlgorithm

def xu2024_code : QECCode

def xu2024_hw : QualtranPhysicalParameters

def xu2024_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

example : xu2024_instance.1.q_A = 8

example : xu2024_instance.2.1.n = 544 ∧
          xu2024_instance.2.1.k = 80 ∧
          xu2024_instance.2.1.d = 12

example : xu2024_instance.2.2.cycle_time_us_tenths = 240000

example : xu2024_hw.cycle_time_us_tenths = 24000 * gidney_fowler_realistic.cycle_time_us_tenths