def babbush_hw : QualtranPhysicalParameters

def babbush_shor : ShorAlgorithm

def babbush_code : QECCode

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

theorem bb18_n : bb18.n = 248

theorem bb18_k_derived : derivedK bb18 = 10

theorem bb18_k_matches_paper : derivedK bb18 = 10

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

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

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

theorem cainxu_qpe_factors_N (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits) (h_inv0 : a * ainv0 % N = 1)
    (h_setting : BasicSettingRelaxed a r N m bits)
    (hr_even : Even r) (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    factoringSuccessProb a N m bits (2 * w + 2 * bits + 3)
        (windowedModNMultiplier_verifiedModMulFamily w bits numWin N a ainv0
          hw hbits hb1 hN1 hN2 h_inv0).family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4
    ∧ ∃ d : ℕ, d ∣ N ∧ 1 < d ∧ d < N

theorem cainxu_modexp_endToEnd (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits) (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    -- (1) L1 SUCCESS: the full QPE/order-finding on the Babbush-measured modexp attains the Shor bound
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (windowedModNMultiplier_verifiedModMulFamily w bits numWin N a ainv0
          hw hbits hb1 hN1 hN2 h_inv0).family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4
    -- (2) L2 RESOURCE: the whole-ladder assembled Toffoli count over the m real iterates
    ∧ (∑ i ∈ Finset.range m,
        EGate.toffoli (babbushMeasWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)

def qianxu_RSA2048_pct_lookups : Nat

def qianxu_RSA2048_pct_adders  : Nat

def cainxu_amortized_runtime (tau_Toff n_Toff : Nat) : Nat

theorem cainxu_pbc_runtime_on_assembled_ladder (w bits numWin N a m tau_Toff : Nat) :
    cainxu_amortized_runtime tau_Toff
        (∑ i ∈ Finset.range m,
          EGate.toffoli (babbushMeasWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)
            (modInv N (a ^ (2 ^ i)))))
      = tau_Toff * (m * (2 * (numWin * (2 * (2 ^ w - 1) + 8 * bits))))

def cainxu_hw : QualtranPhysicalParameters

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) :
    ( FormalRV.SQIRPort.probability_of_success a r N m bits
          (ModMul.ancillaWidth bits) (ModMul.circuitFamily a ainv N bits)
        ≥ FormalRV.SQIRPort.κ / (Nat.log2 N : ℝ) ^ 4

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) :
    σ'.bits = Gate.applyNat g f
    ∧ ( t.bits a, t.bits b, t.bits c )
        = (s.bits a, s.bits b, xor (s.bits c) (s.bits a && s.bits b))

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

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) :
    (∀ toffCount, timeLower (naiveSequentialDepth toffCount) tau_s cycle
        = timeUpper toffCount tau_s cycle)
    ∧ naivePPMonLP_qubits 4350 894 = 5244

theorem cainxu_E3_adder_toffoli (n q_start : Nat) :
    EGate.toffoli (gidneyAdderMeasured (n + 2) q_start) = n + 2

theorem cainxu_E4_ctrl_adder_toffoli (n q_start ctrl : Nat) :
    EGate.toffoli (gidneyAdderMeasuredControlled (n + 2) q_start ctrl) = 2 * (n + 2)

theorem cainxu_E3_to_E4_factor_two (n q_start ctrl : Nat) :
    EGate.toffoli (gidneyAdderMeasuredControlled (n + 2) q_start ctrl)
      = 2 * EGate.toffoli (gidneyAdderMeasured (n + 2) q_start)

theorem cainxu_E9_lookup_read_toffoli
    (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) (addrBase ancBase d ctrl base : Nat) :
    EGate.toffoli (unaryQROMAt pos W T addrBase ancBase d ctrl base) = 2 ^ d - 1
    ∧ (∀ (f : Nat → Bool) (i : Nat), i < d →
        EGate.applyNat (unaryQROMAt pos W T addrBase ancBase d ctrl base) f (ancBase + i) = false)

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 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 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 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 cainxu_shor : ShorAlgorithm

def cainxu_code : QECCode

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

def lp20_n : Nat

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 cainxu_modexp_ppm_realized
    (F : TFactoryContract)
    (w bits a ainv N numWin y : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits)
    (hN_pos : 0 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hy : y < N) (hainv : ainv < N) (hinv : a * ainv % N = 1) :
    (∃ σ' output,
      MagicPPMProgramRel F
        (compileArithmeticGateToMagicPPM (windowedModNMulInPlace w bits a ainv N numWin))
        (encodeWithPool (mulInputOf cuccaroAdder w bits numWin y)
          (factoryProvision F (shorMagicDemand (windowedModNMulInPlace w bits a ainv N numWin)))) σ'
      ∧ (magicBasisRefinesApplyNat F).observesBits σ' output

theorem verified_lookup_toffoli (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase q_a ctrl base : Nat) :
    EGate.toffoli (unaryQROMAt pos W T addrBase ancBase q_a ctrl base) = 2 ^ q_a - 1

theorem verified_adder_toffoli (q_A q_start : Nat) :
    EGate.toffoli (gidneyAdderMeasured (q_A + 2) q_start) = q_A + 2

theorem verified_ctrl_adder_toffoli (q_A q_start ctrl : Nat) :
    EGate.toffoli (gidneyAdderMeasuredControlled (q_A + 2) q_start ctrl) = 2 * (q_A + 2)

theorem lookup_paper_overcounts_by_one (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase q_a ctrl base : Nat) :
    EGate.toffoli (unaryQROMAt pos W T addrBase ancBase q_a ctrl base) + 1 = 2 ^ q_a

def lookupTotPerWindow (q_a : Nat) : Nat

def adderTotPerWindow (addsPerWindow q_A : Nat) : Nat

theorem split_plain_add_is_lookup_heavy :
    lookupTotPerWindow 6 = 63
    ∧ adderTotPerWindow 1 33 = 33
    ∧ 100 * lookupTotPerWindow 6 / (lookupTotPerWindow 6 + adderTotPerWindow 1 33) = 65

theorem split_modular_add_is_balanced :
    lookupTotPerWindow 6 = 63
    ∧ adderTotPerWindow 2 33 = 66
    ∧ 100 * lookupTotPerWindow 6 / (lookupTotPerWindow 6 + adderTotPerWindow 2 33) = 48

theorem fifty_fifty_split_holds_for_modular_add :
    -- balanced under a modular (2-raw-add) window, to within 3 Toffoli:
    (lookupTotPerWindow 6 ≤ adderTotPerWindow 2 33 ∧ adderTotPerWindow 2 33 ≤ lookupTotPerWindow 6 + 3)
    -- but a single plain add is far from balanced (lookup exceeds adder by 30):
    ∧ adderTotPerWindow 1 33 + 30 = lookupTotPerWindow 6

theorem cainxu_E11_tau_toff_consistent : (13 + 7) / 2 = 10

theorem cainxu_E12_tau_toff_within_rounding : 4 * 25 + 5 * 15 + 1 * 550 = 725

theorem cainxu_E13_tau_toff_within_rounding : 4 * 25 + 5 * 15 + 1 * 11 = 186

theorem cainxu_E10_tau_toff_inconsistent : (25 + 71) / 2 = 48 ∧ (25 + 71) / 2 ≠ 43

theorem cainxu_rate_lp20_rounds_to_28 :
    1224 * 10000 / 4350 = 2813 ∧ 1480 * 10000 / 5278 = 2804

theorem cainxu_zone_breakdowns_match :
    4350 + (4350 - 1224) / 2 = 5913              -- memory (lp_20 memory code)
    ∧ 7177 = 5278 + (5278 - 1480) / 2            -- memory (lp_24)
    ∧ 5 * 367 + 10 * 73 = 2565                    -- resource (magic) zone
    ∧ 342 + 200 + 189 + 104 + 39 + 20 = 894

theorem cainxu_qubit_totals_match :
    5913 + 367 + 2565 + 894 = 9739        -- space-efficient, lp_20 memory
    ∧ 7177 + 367 + 2565 + 924 = 11033     -- space-efficient, lp_24 memory
    ∧ 5913 + 1609 + 2565 + 1874 = 11961   -- balanced, lp_20
    ∧ 7177 + 1609 + 2565 + 1904 = 13255

theorem cainxu_lookup_faithful_not_overoptimistic
    (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) (addrBase ancBase d ctrl base : Nat)
    (hpos_inj : ∀ j k, j < W → k < W → pos j = pos k → j = k) (f : Nat → Bool)
    (h1 : ∀ i j, i < d → j < W → ancBase + i ≠ pos j)
    (h2 : ∀ i i', i < d → i' < d → ancBase + i ≠ addrBase + i')
    (h3 : ∀ i j, i < d → j < W → addrBase + i ≠ pos j)
    (h4 : ∀ j, j < W → ctrl ≠ pos j)
    (h5 : ∀ i, i < d → ctrl ≠ ancBase + i)
    (h6 : ∀ i, i < d → f (ancBase + i) = false) :
    (∀ j, j < W →
        EGate.applyNat (unaryQROMAt pos W T addrBase ancBase d ctrl base) f (pos j)
          = xor (f (pos j))

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 upperTimeUs (numPPMs tau_s cycle : Nat) : Nat

def upperQubits (n_LP N_A factory : Nat) : Nat

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 = 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 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

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 :
    (∀ g ∈ bbSmall.hx.map CSSCode.xStab ++ bbSmall.hz.map CSSCode.zStab,
        g ∈ measureChecks [bbSmallLogicalBasis.zbar 0, bbSmallLogicalBasis.zbar 1]
              (codeStateWithLogicals bbSmall 2 bbSmallLogicalBasis))
    ∧ upperQubits 4350 894 2565 = 7809
    ∧ upperTimeUs 1_000_000_000 13 1000 = 13_000_000_000_000

private lemma bmod_natCast_mod (a m : ℕ) :
    Int.bmod ((a : ℤ)) (2 ^ m) = Int.bmod (((a % 2 ^ m : ℕ)) : ℤ) (2 ^ m)

theorem cresid_reduction_exists (d j m ℓ : ℕ) :
    ∃ k : ℤ, 0 ≤ k ∧ k < 2 ^ ℓ ∧
      Int.bmod ((d : ℤ) * j + 2 ^ m * k) (2 ^ (ℓ + m)) = Int.bmod ((d : ℤ) * j) (2 ^ m)

theorem cresid_reduction_forward (d j m ℓ k : ℕ) (hm : 2 ≤ m)
    (hgood : |Int.bmod ((d : ℤ) * j + 2 ^ m * k) (2 ^ (ℓ + m))| ≤ 2 ^ (m - 2)) :
    Int.bmod ((d : ℤ) * j + 2 ^ m * k) (2 ^ (ℓ + m)) = Int.bmod ((d : ℤ) * j) (2 ^ m)

theorem eh_good_pair_iff (d j m ℓ : ℕ) (hm : 2 ≤ m) :
    (∃ k : ℕ, k < 2 ^ ℓ ∧ EHGoodPair m ℓ d j k) ↔ |cresid ((d : Int) * j) (2 ^ m)| ≤ 2 ^ (m - 2)

theorem exists_modinv (d m : ℕ) (hcop : Nat.Coprime d (2 ^ m)) :
    ∃ e : ℕ, ∀ s : ℕ, (d * ((e * s) % 2 ^ m)) % 2 ^ m = s % 2 ^ m

theorem count_good_residues_eq_base (d m : ℕ) (hm : 1 ≤ m) (hd : Odd d) :
    (Finset.filter (fun r : ℕ => |Int.bmod ((d : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card
      = (Finset.filter (fun s : ℕ => |Int.bmod ((s : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card

private lemma good_low (m s : ℕ) (hm : 2 ≤ m) (hs : s < 2 ^ (m - 2)) :
    |Int.bmod ((s : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2)

private lemma good_high (m s : ℕ) (hm : 2 ≤ m) (hs1 : 2 ^ m - 2 ^ (m - 2) ≤ s) (hs2 : s < 2 ^ m) :
    |Int.bmod ((s : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2)

theorem count_base_good_lower (m : ℕ) (hm : 2 ≤ m) :
    2 ^ (m - 1) ≤ (Finset.filter (fun s : ℕ => |Int.bmod ((s : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
                  (Finset.range (2 ^ m))).card

theorem periodic_shift (P : ℕ → Prop) (n : ℕ) (hper : ∀ j, P (j + n) ↔ P j) (c j : ℕ) :
    P (j + c * n) ↔ P j

theorem filter_range_mul_periodic (P : ℕ → Prop) [DecidablePred P] (n : ℕ) (c : ℕ)
    (hper : ∀ j, P (j + n) ↔ P j) :
    (Finset.filter P (Finset.range (c * n))).card
      = c * (Finset.filter P (Finset.range n)).card

theorem good_pred_periodic (d m : ℕ) (j : ℕ) :
    (|Int.bmod ((d : ℤ) * ((j + 2 ^ m : ℕ) : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
      ↔ (|Int.bmod ((d : ℤ) * (j : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))

theorem count_good_j_odd_d (d m ℓ : ℕ) :
    (Finset.filter (fun j : ℕ => |Int.bmod ((d : ℤ) * (j : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ (ℓ + m)))).card =
    2 ^ ℓ * (Finset.filter (fun r : ℕ => |Int.bmod ((d : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card

theorem count_good_j_lower_bound (d m ℓ : ℕ) (hm : 2 ≤ m) (hd : Odd d) :
    2 ^ (ℓ + m - 1) ≤
      (Finset.filter (fun j : ℕ => |Int.bmod ((d : ℤ) * (j : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
                        (Finset.range (2 ^ (ℓ + m)))).card

theorem count_good_pairs_lower_bound (d m ℓ : ℕ) (hm : 2 ≤ m) (hd : Odd d) :
    2 ^ (ℓ + m - 1) ≤
      (Finset.filter (fun j => ∃ k : ℕ, k < 2 ^ ℓ ∧ EHGoodPair m ℓ d j k)
        (Finset.range (2 ^ (ℓ + m)))).card

private lemma bmod_eq_of_nat_mod_eq {a b m : ℕ} (h : a % 2 ^ m = b % 2 ^ m) :
    Int.bmod ((a : ℤ)) (2 ^ m) = Int.bmod ((b : ℤ)) (2 ^ m)

theorem count_unit_transport (a u m : ℕ) (B : ℤ) (hcop : Nat.Coprime u (2 ^ m)) :
    (Finset.filter (fun r : ℕ => |Int.bmod (((a * u : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ B)
        (Finset.range (2 ^ m))).card
      = (Finset.filter (fun s : ℕ => |Int.bmod ((a : ℤ) * (s : ℤ)) (2 ^ m)| ≤ B)
        (Finset.range (2 ^ m))).card

private lemma good_low_scaled (κ m t : ℕ) (hm : 2 ≤ m) (ht : (2:ℕ) ^ κ * t < 2 ^ (m - 2)) :
    |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (t : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2)

theorem count_scaled_good_lower (κ n : ℕ) (hn : 2 ≤ n) :
    2 ^ (n - 1) ≤
      (Finset.filter (fun t : ℕ =>
          |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (t : ℤ)) (2 ^ (κ + n))| ≤ 2 ^ (κ + n - 2))
        (Finset.range (2 ^ n))).card

theorem scaled_good_pred_periodic (κ m : ℕ) (hκm : κ ≤ m) (r : ℕ) :
    (|Int.bmod (((2 ^ κ : ℕ) : ℤ) * ((r + 2 ^ (m - κ) : ℕ) : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
      ↔ (|Int.bmod (((2 ^ κ : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))

theorem count_scaled_periodic (κ m : ℕ) (hκm : κ ≤ m) :
    (Finset.filter (fun r : ℕ => |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card
      = 2 ^ κ *
        (Finset.filter (fun r : ℕ => |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
          (Finset.range (2 ^ (m - κ)))).card

theorem count_scaled_good_lower_one (κ m : ℕ) :
    1 ≤
      (Finset.filter (fun r : ℕ => |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range 2)).card

theorem count_scaled_residue_lower (κ m : ℕ) (hm : 2 ≤ m) (hκ : κ ≤ m - 1) :
    2 ^ (m - 1) ≤
      (Finset.filter (fun r : ℕ => |Int.bmod (((2 ^ κ : ℕ) : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card

theorem count_general_residue_lower (d m : ℕ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    2 ^ (m - 1) ≤
      (Finset.filter (fun r : ℕ => |Int.bmod ((d : ℤ) * (r : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
        (Finset.range (2 ^ m))).card

theorem count_general_j_lower_bound (d m ℓ : ℕ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    2 ^ (ℓ + m - 1) ≤
      (Finset.filter (fun j : ℕ => |Int.bmod ((d : ℤ) * (j : ℤ)) (2 ^ m)| ≤ 2 ^ (m - 2))
                        (Finset.range (2 ^ (ℓ + m)))).card

theorem count_good_pairs_lower_bound_general (d m ℓ : ℕ) (hm : 2 ≤ m)
    (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    2 ^ (ℓ + m - 1) ≤
      (Finset.filter (fun j => ∃ k : ℕ, k < 2 ^ ℓ ∧ EHGoodPair m ℓ d j k)
        (Finset.range (2 ^ (ℓ + m)))).card

noncomputable def ehProb (ℓ m d j k : ℕ) : ℝ

theorem ehProb_ge_of_good (ℓ m d j k : ℕ) (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hdlt : d < 2 ^ m)
    (hgood : EHGoodPair m ℓ d j k) :
    (2 : ℝ) ^ (-(ℓ + m + 2 : ℤ)) ≤ ehProb ℓ m d j k

noncomputable def goodOutcomes (ℓ m d : ℕ) : Finset ℕ

noncomputable def kPair (ℓ m d j : ℕ) : ℕ

theorem kPair_good (ℓ m d j : ℕ) (hj : j ∈ goodOutcomes ℓ m d) :
    EHGoodPair m ℓ d j (kPair ℓ m d j)

theorem ehShor_per_run_ge_eighth (ℓ m d : ℕ) (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    (1 / 8 : ℝ) ≤ ∑ j ∈ goodOutcomes ℓ m d, ehProb ℓ m d j (kPair ℓ m d j)

theorem ehShor_endToEnd (ℓ m d : ℕ) (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m)
    (a b N : ℕ) (hab : b ≤ a) (hd : d = a + b) (hN : N = (2 * a + 1) * (2 * b + 1)) :
    (1 / 8 : ℝ) ≤ ∑ j ∈ goodOutcomes ℓ m d, ehProb ℓ m d j (kPair ℓ m d j)
      ∧ ((d + 1) + ((d + 1) * (d + 1) - N).sqrt = 2 * a + 1
          ∧ (d + 1) - ((d + 1) * (d + 1) - N).sqrt = 2 * b + 1)

theorem ekera_congruence {p q r : Nat} (hp : 1 ≤ p) (hq : 1 ≤ q)
    (hr : r ∣ (p - 1) * (q - 1)) :
    (p * q + 1) ≡ (p + q) [MOD r]

theorem ekera_short_dl_eq {d p q r : Nat} (hcong : d ≡ (p + q) [MOD r])
    (hd_lt : d < r) (hpq_lt : p + q < r) : d = p + q

theorem ekera_recover {p q d N : Nat} (hq_le_p : q ≤ p)
    (hd : d = p + q) (hN : N = p * q) :
    (d + (d * d - 4 * N).sqrt) / 2 = p ∧ (d - (d * d - 4 * N).sqrt) / 2 = q

theorem ekera_recover_actual {a b d N : Nat} (hab : b ≤ a)
    (hd : d = a + b) (hN : N = (2 * a + 1) * (2 * b + 1)) :
    (d + 1) + ((d + 1) * (d + 1) - N).sqrt = 2 * a + 1 ∧
    (d + 1) - ((d + 1) * (d + 1) - N).sqrt = 2 * b + 1

theorem ekera_factor (p q r d N : Nat) (hp : 1 ≤ p) (hq : 1 ≤ q) (hq_le_p : q ≤ p)
    (hN : N = p * q) (h_ord : r ∣ (p - 1) * (q - 1))
    (h_dl : d ≡ (N + 1) [MOD r]) (hd_lt : d < r) (hpq_lt : p + q < r) :
    (d + (d * d - 4 * N).sqrt) / 2 = p ∧ (d - (d * d - 4 * N).sqrt) / 2 = q

def cresid (u : Int) (n : Nat) : Int

def EHGoodPair (m ℓ d j k : Nat) : Prop

theorem eh_good_vector_within_radius (m s d : Nat) (resid : Fin s → Int)
    (hm : 2 ≤ m) (hd : d < 2 ^ m) (hgood : ∀ i, |resid i| ≤ 2 ^ (m - 2)) :
    4 * ((d : Int) ^ 2 + ∑ i, (resid i) ^ 2) < ((s : Int) + 4) * 2 ^ (2 * m)

structure EHShortDLPSuccess

noncomputable def EHShortDLPSuccess.goodProb (S : EHShortDLPSuccess) : ℝ

theorem EHShortDLPSuccess.goodProb_ge (S : EHShortDLPSuccess) :
    (S.goodJ.card : ℝ) * S.p ≤ S.goodProb

theorem eh_count_times_prob (ℓ m : Nat) (h : 1 ≤ ℓ + m) :
    (2 : ℝ) ^ (ℓ + m - 1) * (2 : ℝ) ^ (-(m + ℓ + 2 : ℤ)) = 1 / 8

theorem EHShortDLPSuccess.goodProb_ge_eighth (S : EHShortDLPSuccess) (ℓ m : Nat)
    (_hℓm : S.ℓm = ℓ + m) (hge1 : 1 ≤ ℓ + m)
    (hcount : (2 : ℝ) ^ (ℓ + m - 1) ≤ (S.goodJ.card : ℝ))
    (hp : S.p = (2 : ℝ) ^ (-(m + ℓ + 2 : ℤ))) :
    (1 / 8 : ℝ) ≤ S.goodProb

noncomputable def ehInput (ℓ m : ℕ) : ℕ → ℕ → ℂ

def ehTarget (d : ℕ) : ℕ → ℕ → ℤ

noncomputable def ehCircuitMeasProb (ℓ m d j k : ℕ) : ℝ

theorem ehCircuitMeasProb_nonneg (ℓ m d j k : ℕ) : 0 ≤ ehCircuitMeasProb ℓ m d j k

theorem ehKernel_combine (ℓ m x j y k : ℕ) :
    qftKernel (ℓ + m) x j * qftKernel ℓ y k
      = Complex.exp (2 * Real.pi * Complex.I * ((x : ℂ) * j + 2 ^ m * ((y : ℂ) * k))
          / (2 ^ (ℓ + m) : ℂ))

theorem ehCircuit_fiberAmp_eq (ℓ m d j k : ℕ) (e : ℤ) :
    qft2FiberAmp (ℓ + m) ℓ (ehInput ℓ m) (ehTarget d) j k e
      = (1 / (2 ^ (2 * ℓ + m) : ℂ))
          * ∑ x ∈ Finset.range (2 ^ (ℓ + m)),
              ∑ y ∈ (Finset.range (2 ^ ℓ)).filter (fun y => ehTarget d x y = e),
                Complex.exp (2 * Real.pi * Complex.I * ((x : ℂ) * j + 2 ^ m * ((y : ℂ) * k))
                  / (2 ^ (ℓ + m) : ℂ))

private theorem sum_range_int_ite {M : Type*} [AddCommMonoid M] (N : ℕ) (w : ℤ) (h : ℕ → M) :
    (∑ x ∈ Finset.range N, if (x : ℤ) = w then h x else 0)
      = if (0 ≤ w ∧ w < (N : ℤ)) then h w.toNat else 0

theorem ehFiber_reindex {M : Type*} [AddCommMonoid M] (ℓ m d : ℕ) (e : ℤ) (g : ℕ → ℕ → M) :
    (∑ x ∈ Finset.range (2 ^ (ℓ + m)),
        ∑ y ∈ (Finset.range (2 ^ ℓ)).filter (fun y => ehTarget d x y = e), g x y)
      = ∑ b ∈ FormalRV.CFS.EkeraLemma7.ehBe ℓ m d e, g (e + (b : ℤ) * (d : ℤ)).toNat b

theorem ehFiberNormSq_raw (ℓ m d j k : ℕ) (e : ℤ) :
    Complex.normSq (qft2FiberAmp (ℓ + m) ℓ (ehInput ℓ m) (ehTarget d) j k e)
      = (1 / (2 : ℝ) ^ (2 * (2 * ℓ + m)))
          * Complex.normSq (∑ b ∈ FormalRV.CFS.EkeraLemma7.ehBe ℓ m d e,
              Complex.exp (2 * Real.pi * Complex.I
                * ((((e + (b : ℤ) * (d : ℤ)).toNat : ℕ) : ℂ) * j + 2 ^ m * ((b : ℂ) * k))
                  / (2 ^ (ℓ + m) : ℂ)))

private theorem exp_two_pi_int (z : ℤ) :
    Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (z : ℂ)) = 1

private theorem normSq_exp_ofReal_mul_I (r : ℝ) :
    Complex.normSq (Complex.exp ((r : ℂ) * Complex.I)) = 1

theorem ehPhase_normSq (ℓ m d j k : ℕ) (e : ℤ) :
    Complex.normSq (∑ b ∈ FormalRV.CFS.EkeraLemma7.ehBe ℓ m d e,
        Complex.exp (2 * Real.pi * Complex.I
          * ((((e + (b : ℤ) * (d : ℤ)).toNat : ℕ) : ℂ) * j + 2 ^ m * ((b : ℂ) * k))
            / (2 ^ (ℓ + m) : ℂ)))
      = Complex.normSq (∑ b ∈ FormalRV.CFS.EkeraLemma7.ehBe ℓ m d e,
          Complex.exp (((2 * Real.pi / (2 : ℝ) ^ (ℓ + m)) * ((b : ℝ) - (2 : ℝ) ^ (ℓ - 1))
            * ((cresid ((d : ℤ) * j + 2 ^ m * k) (2 ^ (ℓ + m)) : ℤ) : ℝ) : ℝ) * Complex.I))

theorem ehCircuitMeasProb_eq_ehProb (ℓ m d j k : ℕ) :
    ehCircuitMeasProb ℓ m d j k = FormalRV.Audit.Gidney2025.EkeraEndToEnd.ehProb ℓ m d j k

theorem ehCircuit_per_run_ge_eighth (ℓ m d : ℕ) (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    (1 / 8 : ℝ) ≤ ∑ j ∈ FormalRV.Audit.Gidney2025.EkeraEndToEnd.goodOutcomes ℓ m d,
        ehCircuitMeasProb ℓ m d j (FormalRV.Audit.Gidney2025.EkeraEndToEnd.kPair ℓ m d j)

noncomputable def ehEncZ (ℓ m : ℕ) (e : ℤ) : ℕ

noncomputable def ehEnc (ℓ m d : ℕ) : ℕ → ℕ → ℕ

theorem mem_ehE_iff (ℓ m : ℕ) (e : ℤ) :
    e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m ↔ -(2 : ℤ) ^ (ℓ + m) < e ∧ e < (2 : ℤ) ^ (ℓ + m)

theorem ehEncZ_lt (ℓ m : ℕ) (e : ℤ) (he : e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m) :
    ehEncZ ℓ m e < 2 ^ (ℓ + m + 1)

theorem ehEncZ_injOn (ℓ m : ℕ) {e e' : ℤ}
    (he : e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m) (he' : e' ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m)
    (heq : ehEncZ ℓ m e = ehEncZ ℓ m e') : e = e'

theorem ehTarget_mem_ehE (ℓ m d x y : ℕ) (hx : x < 2 ^ (ℓ + m)) (hy : y < 2 ^ ℓ) (hd : d < 2 ^ m) :
    ehTarget d x y ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m

theorem conj_qftKernel (a x j : ℕ) :
    starRingEnd ℂ (qftKernel a x j)
      = Complex.exp (-(2 * Real.pi * Complex.I) * (x : ℂ) * (j : ℂ) / (2 ^ a : ℂ))

theorem iqft_entry (a x j : ℕ) (hx : x < 2 ^ a) (hj : j < 2 ^ a) :
    (FormalRV.SQIRPort.IQFT_matrix a * FormalRV.Framework.basis_vector (2 ^ a) x)
        (⟨j, hj⟩ : Fin (2 ^ a)) 0
      = (1 / (Real.sqrt (2 ^ a : ℝ) : ℂ)) * starRingEnd ℂ (qftKernel a x j)

theorem conj_ehInput (ℓ m x y : ℕ) : starRingEnd ℂ (ehInput ℓ m x y) = ehInput ℓ m x y

theorem ehFiberCtrl_eq_conj (ℓ m d : ℕ) (e : ℤ) (he : e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m)
    (j k : ℕ) (hj : j < 2 ^ (ℓ + m)) (hk : k < 2 ^ ℓ) (hdlt : d < 2 ^ m) :
    fiberCtrl (ℓ + m) ℓ (ℓ + m + 1) (ehInput ℓ m) (ehEnc ℓ m d)
        ⟨ehEncZ ℓ m e, ehEncZ_lt ℓ m e he⟩
        (FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ (ℓ + m))) (⟨k, hk⟩ : Fin (2 ^ ℓ))) 0
      = starRingEnd ℂ (qft2FiberAmp (ℓ + m) ℓ (ehInput ℓ m) (ehTarget d) j k e)

noncomputable def encTot (ℓ m : ℕ) (e : ℤ) : Fin (2 ^ (ℓ + m + 1))

theorem encTot_eq (ℓ m : ℕ) (e : ℤ) (he : e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m) :
    encTot ℓ m e = ⟨ehEncZ ℓ m e, ehEncZ_lt ℓ m e he⟩

theorem encTot_injOn (ℓ m : ℕ) {e e' : ℤ}
    (he : e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m) (he' : e' ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m)
    (heq : encTot ℓ m e = encTot ℓ m e') : e = e'

theorem fiberCtrl_eq_zero_of_not_image (ℓ m d j k : ℕ) (hj : j < 2 ^ (ℓ + m)) (hk : k < 2 ^ ℓ)
    (hdlt : d < 2 ^ m) (i : Fin (2 ^ (ℓ + m + 1)))
    (hi : i ∉ (FormalRV.CFS.EkeraLemma7.ehE ℓ m).image (encTot ℓ m)) :
    fiberCtrl (ℓ + m) ℓ (ℓ + m + 1) (ehInput ℓ m) (ehEnc ℓ m d) i
        (FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ (ℓ + m))) (⟨k, hk⟩ : Fin (2 ^ ℓ))) 0
      = 0

theorem eh_fiber_sum_eq (ℓ m d j k : ℕ) (hj : j < 2 ^ (ℓ + m)) (hk : k < 2 ^ ℓ) (hdlt : d < 2 ^ m) :
    (∑ i : Fin (2 ^ (ℓ + m + 1)),
        Complex.normSq
          (fiberCtrl (ℓ + m) ℓ (ℓ + m + 1) (ehInput ℓ m) (ehEnc ℓ m d) i
            (FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ (ℓ + m)))
              (⟨k, hk⟩ : Fin (2 ^ ℓ))) 0))
      = ∑ e ∈ FormalRV.CFS.EkeraLemma7.ehE ℓ m,
          Complex.normSq (qft2FiberAmp (ℓ + m) ℓ (ehInput ℓ m) (ehTarget d) j k e)

theorem prob_partial_meas_eq_ehCircuitMeasProb (ℓ m d j k : ℕ) (hℓ : 1 ≤ ℓ)
    (hj : j < 2 ^ (ℓ + m)) (hk : k < 2 ^ ℓ) (hdlt : d < 2 ^ m) :
    prob_partial_meas
        (FormalRV.SQIRPort.basis_vector (2 ^ ((ℓ + m) + ℓ))
          (FormalRV.Framework.kron_vec_combine (⟨j, hj⟩ : Fin (2 ^ (ℓ + m)))
            (⟨k, hk⟩ : Fin (2 ^ ℓ))).val)
        (twoRegQFTMeasState (ℓ + m) ℓ (ℓ + m + 1) (ehInput ℓ m) (ehEnc ℓ m d))
      = ehCircuitMeasProb ℓ m d j k

theorem ehGate_per_run_ge_eighth (ℓ m d : ℕ) (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m) :
    (1 / 8 : ℝ) ≤ ∑ j ∈ goodOutcomes ℓ m d,
      prob_partial_meas
        (FormalRV.SQIRPort.basis_vector (2 ^ ((ℓ + m) + ℓ)) (j * 2 ^ ℓ + kPair ℓ m d j))
        (twoRegQFTMeasState (ℓ + m) ℓ (ℓ + m + 1) (ehInput ℓ m) (ehEnc ℓ m d))

def overlay (L : List (Nat × Bool)) (f : Nat → Bool) : Nat → Bool

theorem overlay_cons (pb : Nat × Bool) (L : List (Nat × Bool)) (f : Nat → Bool) :
    overlay (pb :: L) f = update (overlay L f) pb.1 pb.2

theorem condAdd_commute_overlay (bits q_start N flagPos : Nat) (L : List (Nat × Bool)) (f : Nat → Bool)
    (hL : ∀ pb ∈ L, (pb.1 < q_start ∨ q_start + 2 * bits + 1 ≤ pb.1) ∧ pb.1 ≠ flagPos) :
    Gate.applyNat (sqir_conditionalAddConstGate bits q_start N flagPos) (overlay L f)
      = overlay L (Gate.applyNat (sqir_conditionalAddConstGate bits q_start N flagPos) f)

theorem condSub_commute_overlay (bits q_start N flagPos : Nat) (L : List (Nat × Bool)) (f : Nat → Bool)
    (hL : ∀ pb ∈ L, (pb.1 < q_start ∨ q_start + 2 * bits + 1 ≤ pb.1) ∧ pb.1 ≠ flagPos) :
    Gate.applyNat (sqir_conditionalSubConstGate bits q_start N flagPos) (overlay L f)
      = overlay L (Gate.applyNat (sqir_conditionalSubConstGate bits q_start N flagPos) f)

theorem cuccaro_target_val_testBit (q_start : Nat) (f : Nat → Bool) :
    ∀ bits i, i < bits → (cuccaro_target_val bits q_start f).testBit i = f (q_start + 2 * i + 1)

theorem cuccaro_read_val_testBit (q_start : Nat) (f : Nat → Bool) :
    ∀ bits i, i < bits → (cuccaro_read_val bits q_start f).testBit i = f (q_start + 2 * i + 2)

theorem cuccaro_carry_congr (f f' : Nat → Bool) (q_start : Nat) :
    ∀ k, f q_start = f' q_start →
      (∀ j, j < k → f (q_start + 2 * j + 1) = f' (q_start + 2 * j + 1)) →
      (∀ j, j < k → f (q_start + 2 * j + 2) = f' (q_start + 2 * j + 2)) →
      cuccaro_carry f q_start k = cuccaro_carry f' q_start k

theorem adder_target_val_general (bits q_start : Nat) (g : Nat → Bool) :
    cuccaro_target_val bits q_start (Gate.applyNat (cuccaro_n_bit_adder_full bits q_start) g)
      = (cuccaro_target_val bits q_start g + cuccaro_read_val bits q_start g
          + (g q_start).toNat) % 2 ^ bits

theorem cuccaro_target_val_congr (q_start : Nat) (f f' : Nat → Bool) :
    ∀ bits, (∀ i, i < bits → f (q_start + 2 * i + 1) = f' (q_start + 2 * i + 1)) →
      cuccaro_target_val bits q_start f = cuccaro_target_val bits q_start f'

theorem cuccaro_read_val_congr (q_start : Nat) (f f' : Nat → Bool) :
    ∀ bits, (∀ i, i < bits → f (q_start + 2 * i + 2) = f' (q_start + 2 * i + 2)) →
      cuccaro_read_val bits q_start f = cuccaro_read_val bits q_start f'

private theorem mask_read_pos_ne (q_start i j : Nat) : q_start + 2 * i + 1 ≠ q_start + 2 * j + 2

theorem condAdd_step (bits q_start N flagPos : Nat) (f : Nat → Bool)
    (hN : N < 2 ^ bits)
    (hread : ∀ j, j < bits → f (q_start + 2 * j + 2) = false)
    (hcarry : f q_start = false)
    (hdist : ∀ i, i < bits → flagPos ≠ q_start + 2 * i + 2)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    cuccaro_target_val bits q_start
        (Gate.applyNat (sqir_conditionalAddConstGate bits q_start N flagPos) f)
      = (cuccaro_target_val bits q_start f + (if f flagPos then N else 0)) % 2 ^ bits
    ∧ (∀ j, j < bits →
        Gate.applyNat (sqir_conditionalAddConstGate bits q_start N flagPos) f (q_start + 2 * j + 2)
          = false)

theorem addConst_step (bits q_start c : Nat) (f : Nat → Bool)
    (hc : c < 2 ^ bits)
    (hread : ∀ j, j < bits → f (q_start + 2 * j + 2) = false)
    (hcarry : f q_start = false) :
    cuccaro_target_val bits q_start (Gate.applyNat (cuccaro_addConstGate bits q_start c) f)
      = (cuccaro_target_val bits q_start f + c) % 2 ^ bits
    ∧ (∀ j, j < bits → Gate.applyNat (cuccaro_addConstGate bits q_start c) f (q_start + 2 * j + 2) = false)
    ∧ Gate.applyNat (cuccaro_addConstGate bits q_start c) f q_start = false
    ∧ (∀ p, (p < q_start ∨ q_start + 2 * bits + 1 ≤ p) →
        Gate.applyNat (cuccaro_addConstGate bits q_start c) f p = f p)

theorem condSub_step (bits q_start N flagPos : Nat) (f : Nat → Bool)
    (hN0 : 0 < N) (hN : N ≤ 2 ^ bits)
    (hread : ∀ j, j < bits → f (q_start + 2 * j + 2) = false)
    (hcarry : f q_start = false)
    (hdist : ∀ i, i < bits → flagPos ≠ q_start + 2 * i + 2)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    cuccaro_target_val bits q_start
        (Gate.applyNat (sqir_conditionalSubConstGate bits q_start N flagPos) f)
      = (cuccaro_target_val bits q_start f + (if f flagPos then 2 ^ bits - N else 0)) % 2 ^ bits
    ∧ (∀ j, j < bits →
        Gate.applyNat (sqir_conditionalSubConstGate bits q_start N flagPos) f (q_start + 2 * j + 2)
          = false)

def CleanState (bits q_start : Nat) (f : Nat → Bool) : Prop

def CleanStep (bits q_start : Nat) (g : Gate) (δ : (Nat → Bool) → Nat) : Prop

def OutsideStable (bits q_start : Nat) (δ : (Nat → Bool) → Nat) : Prop

theorem condAdd_cleanStep (bits q_start N flagPos : Nat) (hN : N < 2 ^ bits)
    (hdist : ∀ i, i < bits → flagPos ≠ q_start + 2 * i + 2)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    CleanStep bits q_start (sqir_conditionalAddConstGate bits q_start N flagPos)
      (fun f => if f flagPos then N else 0)

theorem condSub_cleanStep (bits q_start N flagPos : Nat) (hN0 : 0 < N) (hN : N ≤ 2 ^ bits)
    (hdist : ∀ i, i < bits → flagPos ≠ q_start + 2 * i + 2)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    CleanStep bits q_start (sqir_conditionalSubConstGate bits q_start N flagPos)
      (fun f => if f flagPos then 2 ^ bits - N else 0)

theorem addConst_cleanStep (bits q_start c : Nat) (hc : c < 2 ^ bits) :
    CleanStep bits q_start (cuccaro_addConstGate bits q_start c) (fun _ => c)

theorem condAdd_outsideStable (bits q_start N flagPos : Nat)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    OutsideStable bits q_start (fun f => if f flagPos then N else 0)

theorem condSub_outsideStable (bits q_start N flagPos : Nat)
    (hout : flagPos < q_start ∨ q_start + 2 * bits + 1 ≤ flagPos) :
    OutsideStable bits q_start (fun f => if f flagPos then 2 ^ bits - N else 0)

theorem const_outsideStable (bits q_start c : Nat) :
    OutsideStable bits q_start (fun _ => c)

theorem cleanStep_fold (bits q_start : Nat) :
    ∀ (gds : List (Gate × ((Nat → Bool) → Nat))),
      (∀ gd ∈ gds, CleanStep bits q_start gd.1 gd.2) →
      (∀ gd ∈ gds, OutsideStable bits q_start gd.2) →
      ∀ f, CleanState bits q_start f →
        (cuccaro_target_val bits q_start
            (Gate.applyNat ((gds.map Prod.fst).foldr Gate.seq Gate.I) f)
          = (cuccaro_target_val bits q_start f + (gds.map (fun gd => gd.2 f)).sum) % 2 ^ bits)
        ∧ CleanState bits q_start (Gate.applyNat ((gds.map Prod.fst).foldr Gate.seq Gate.I) f)
        ∧ (∀ p, (p < q_start ∨ q_start + 2 * bits + 1 ≤ p) →
            Gate.applyNat ((gds.map Prod.fst).foldr Gate.seq Gate.I) f p = f p)

def ehW (ℓ m : ℕ) : ℕ

def ehQStart (ℓ m : ℕ) : ℕ

def ehGadgets (ℓ m d : ℕ) : List Gate

def ehOracleGate (ℓ m d : ℕ) : Gate

theorem tcount_sqir_prepareMaskedConstRead (bits q_start N flagPos : ℕ) :
    tcount (sqir_prepareMaskedConstRead bits q_start N flagPos) = 0

theorem tcount_condAdd (bits q_start N flagPos : ℕ) :
    tcount (sqir_conditionalAddConstGate bits q_start N flagPos) = 14 * bits

theorem tcount_condSub (bits q_start N flagPos : ℕ) :
    tcount (sqir_conditionalSubConstGate bits q_start N flagPos) = 14 * bits

theorem tcount_foldr_seq (L : List Gate) :
    tcount (L.foldr Gate.seq Gate.I) = (L.map tcount).sum

theorem tcount_ehGadgets_uniform (ℓ m d : ℕ) :
    ∀ g ∈ ehGadgets ℓ m d, tcount g = 14 * ehW ℓ m

theorem ehOracleGate_tcount (ℓ m d : ℕ) :
    tcount (ehOracleGate ℓ m d) = 14 * (ℓ + m + 1) * (2 * ℓ + m + 1)

def ehDim (ℓ m : ℕ) : ℕ

theorem wellTyped_foldr_seq (dim : ℕ) (hdim : 0 < dim) (L : List Gate)
    (h : ∀ g ∈ L, Gate.WellTyped dim g) :
    Gate.WellTyped dim (L.foldr Gate.seq Gate.I)

theorem ehOracleGate_wellTyped (ℓ m d : ℕ) :
    Gate.WellTyped (ehDim ℓ m) (ehOracleGate ℓ m d)

theorem toffoli_gcMulEncodeGate_eq_gidney2025 (w n a ainv N numWin : Nat) :
    EGate.toffoli (gcMulEncodeGate w (n + 1) a ainv N numWin)
      = 2 * (numWin * (lookupCost w + addCost (n + 1)))

theorem gidney2025_cost_optimal_canonical_shor
    (w n numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = n + 1)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ (n + 1)) (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m (n + 1)) :
    probability_of_success a r N m (n + 1) (3 * (n + 1) + w + 7)
        (gcRevFamily w (n + 1) numWin N a ainv0 hw hbits (by omega) hN1 hN2 h_inv0).family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4
    ∧ (∀ j, EGate.toffoli (gcStep w (n + 1) a N numWin j) = lookupCost w + addCost (n + 1))
    ∧ EGate.toffoli (gcMul w (n + 1) a N numWin) = numWin * (lookupCost w + addCost (n + 1))
    ∧ (∀ i, EGate.toffoli (gcMulEncodeGate w (n + 1) ((a ^ (2 ^ i)) % N) (modInv N (a ^ (2 ^ i))) N numWin)
        = 2 * (numWin * (lookupCost w + addCost (n + 1))))

def gidney2025_hw : QualtranPhysicalParameters

def gidney2025_shor : ShorAlgorithm

def gidney2025_code : QECCode

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

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

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_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

theorem tcount_gidneyModAddFixup_dvd (r p c : Nat) :
    7 ∣ EGate.tcount (gidneyModAddFixup (r + 1) p c)

theorem tcount_gidneyModAddFixup_eq (r p c : Nat) :
    EGate.tcount (gidneyModAddFixup (r + 1) p c) = 14 * (r + 2)

def addCost (r : Nat) : Nat

def lookupCost (w : Nat) : Nat

def phaseupCost (w : Nat) : Nat

theorem addCost_is_gadget_toffoli (n p c : Nat) :
    addCost (n + 1) = EGate.toffoli (gidneyModAddFixup (n + 1) p c)

theorem lookupCost_is_gadget_toffoli
    (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) (addrBase ancBase ctrl base w : Nat) :
    lookupCost w = EGate.toffoli (unaryQROMAt pos W T addrBase ancBase w ctrl base)

theorem phaseupCost_is_gadget_toffoli (w base : Nat) :
    phaseupCost w
      = EGate.toffoli (EGate.base (phaseupSkeleton ((w + 1) / 2) (w / 2) base))

def loop1Body (w reg : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) : EGate

theorem tcount_loop1Body (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) :
    EGate.tcount (loop1Body w (r + 1) T addrBase ancBase q_start p c)
      = 7 * ((2 ^ w - 1) + 2 * (r + 2))

theorem toffoli_loop1Body (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) :
    EGate.toffoli (loop1Body w (r + 1) T addrBase ancBase q_start p c)
      = lookupCost w + addCost (r + 1)

def loop2Body (reg p c : Nat) : EGate

theorem tcount_loop2Body (r p c : Nat) :
    EGate.tcount (loop2Body (r + 1) p c) = 7 * (4 * (r + 2))

theorem toffoli_loop2Body (r p c : Nat) :
    EGate.toffoli (loop2Body (r + 1) p c) = 2 * addCost (r + 1)

def loop3Body (w reg : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) : EGate

theorem tcount_loop3Body (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) :
    EGate.tcount (loop3Body w (r + 1) T addrBase ancBase q_start p c)
      = 7 * ((2 ^ w - 1) + 4 * (r + 2))

theorem toffoli_loop3Body (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start p c : Nat) :
    EGate.toffoli (loop3Body w (r + 1) T addrBase ancBase q_start p c)
      = lookupCost w + 2 * addCost (r + 1)

def addCostPlain (reg : Nat) : Nat

theorem tcount_gidneyAdderMeasured_eq (r q : Nat) :
    EGate.tcount (gidneyAdderMeasured (r + 2) q) = 7 * (r + 2)

theorem addCostPlain_is_gadget_toffoli (r q : Nat) :
    addCostPlain (r + 2) = EGate.toffoli (gidneyAdderMeasured (r + 2) q)

def loop1BodyPlain (w reg : Nat) (T : Nat → Nat) (addrBase ancBase q_start qadd : Nat) : EGate

theorem toffoli_loop1BodyPlain (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start qadd : Nat) :
    EGate.toffoli (loop1BodyPlain w (r + 2) T addrBase ancBase q_start qadd)
      = lookupCost w + addCostPlain (r + 2)

def loop2BodyPlain (reg q : Nat) : EGate

theorem toffoli_loop2BodyPlain (r q : Nat) :
    EGate.toffoli (loop2BodyPlain (r + 2) q) = 2 * addCostPlain (r + 2)

def loop3BodyPlain (w reg : Nat) (T : Nat → Nat) (addrBase ancBase q_start qadd : Nat) : EGate

theorem toffoli_loop3BodyPlain (w r : Nat) (T : Nat → Nat) (addrBase ancBase q_start qadd : Nat) :
    EGate.toffoli (loop3BodyPlain w (r + 2) T addrBase ancBase q_start qadd)
      = lookupCost w + 2 * addCostPlain (r + 2)

def rsa2048_n : Nat

def rsa2048_s : Nat

def rsa2048_ell : Nat

def rsa2048_w1 : Nat

def rsa2048_w3 : Nat

def rsa2048_w4 : Nat

def rsa2048_f : Nat

def rsa2048_m : Nat

def rsa2048_lenm : Nat

def rsa2048_W1 : Nat

def rsa2048_W3 : Nat

def rsa2048_W4 : Nat

def rsa2048_P : Nat

theorem rsa2048_W1_eq : rsa2048_W1 = 214

theorem rsa2048_W3_eq : rsa2048_W3 = 7

theorem rsa2048_W4_eq : rsa2048_W4 = 5

theorem rsa2048_P_eq : rsa2048_P = 20806

def rsa2048_P_actual : Nat

def rowCostScaled (add2 reg look2 addr phase2 paddr : Nat) : Nat

def gidney2025_perShotScaled : Nat

def gidney2025_perShot : Nat

def gidney2025_toffoli : Nat

def rowCostMixed (plainAdd : Bool) (add2 reg look2 addr phase2 paddr : Nat) : Nat

def gidney2025_perShotScaled_mixed (P : Nat) : Nat

def gidney2025_toffoli_mixed_actualP : Nat

theorem gidney2025_perShot_eq : gidney2025_perShot = 924282141

theorem gidney2025_toffoli_rsa2048 : gidney2025_toffoli = 8503395697

theorem gidney2025_ours_order_of_magnitude :
    6_000_000_000 ≤ gidney2025_toffoli ∧ gidney2025_toffoli ≤ 9_000_000_000

theorem gidney2025_toffoli_mixed_actualP_eq :
    gidney2025_toffoli_mixed_actualP = 6777242100

theorem gidney2025_reproduces_headline_within_6pct :
    6_500_000_000 ≤ gidney2025_toffoli_mixed_actualP
      ∧ gidney2025_toffoli_mixed_actualP ≤ 6_900_000_000

theorem gidney2025_mixed_actualP_close_to_headline :
    gidney2025_toffoli_mixed_actualP - 6_500_000_000 ≤ 400_000_000
      ∧ 6_500_000_000 - gidney2025_toffoli_mixed_actualP = 0

theorem gidney2025_actualP_matches_symbolic :
    rsa2048_P_actual = 21640
      ∧ rsa2048_P = 20806
      ∧ 96 * rsa2048_P_actual ≤ rsa2048_P * 100
      ∧ rsa2048_P * 100 ≤ 97 * rsa2048_P_actual

def lookupCostPaper (w : Nat) : Nat

def phaseupCostPaper (w : Nat) : Nat

def gidney2025_toffoli_paper (addNum addDen : Nat) : Nat

theorem sqrt8  : Nat.sqrt 8  = 2

theorem sqrt32 : Nat.sqrt 32 = 5

theorem sqrt64 : Nat.sqrt 64 = 8

theorem gidney2025_toffoli_paper_25 : gidney2025_toffoli_paper 25 10 = 9079906176

theorem gidney2025_toffoli_paper_2n : gidney2025_toffoli_paper 20 10 = 7773609496

theorem gidney2025_toffoli_paper_plain : gidney2025_toffoli_paper 10 10 = 5161016138

theorem gidney2025_headline_bracketed :
    gidney2025_toffoli_paper 10 10 ≤ 6_500_000_000
      ∧ 6_500_000_000 ≤ gidney2025_toffoli_paper 25 10
      ∧ 6_500_000_000 ≤ gidney2025_toffoli_paper 20 10

theorem gidney2025_reproduces_literal_oom :
    5_000_000_000 ≤ FormalRV.Audit.Gidney2025.gidney2025_work.n_toff
      ∧ FormalRV.Audit.Gidney2025.gidney2025_work.n_toff < 10_000_000_000
      ∧ 5_000_000_000 ≤ gidney2025_toffoli
      ∧ gidney2025_toffoli < 10_000_000_000

theorem gidney2025_PP_to_hit_headline :
    rsa2048_P = 20806
      ∧ 139 * 14894 ≤ rsa2048_P * 100
      ∧ rsa2048_P * 100 ≤ 140 * 14894

theorem gidney2025_resource_reproduced :
    (1280 * 430 + 131 * 1352 + 7 * 18 * 1352 = 897864)
    ∧ (897864 < 1000000 ∧ 1000000 - 897864 = 102136)
    ∧ gidney2025_work.n_logical = 1280 + 131 + 7 * 18

def colReindex {A B : Nat} (h : A = B) (v : Matrix (Fin (2 ^ A)) (Fin 1) ℂ) :
    Matrix (Fin (2 ^ B)) (Fin 1) ℂ

theorem colReindex_eq_cast {A B : Nat} (h : A = B) (v : Matrix (Fin (2 ^ A)) (Fin 1) ℂ) :
    colReindex h v = FormalRV.SQIRPort.QState.cast (congrArg (2 ^ ·) h) v

theorem uc_eval_dimcast_mul {A B : Nat} (h : A = B) (c : BaseUCom A)
    (v : Matrix (Fin (2 ^ B)) (Fin 1) ℂ) :
    uc_eval (h ▸ c) * v
      = colReindex h
          ((uc_eval c * colReindex h.symm v : Matrix (Fin (2 ^ A)) (Fin 1) ℂ))

theorem qstate_cast_comp {a b c : Nat} (h1 : a = b) (h2 : b = c)
    (v : FormalRV.SQIRPort.QState a) :
    FormalRV.SQIRPort.QState.cast h2 (FormalRV.SQIRPort.QState.cast h1 v)
      = FormalRV.SQIRPort.QState.cast (h1.trans h2) v

theorem colReindex_cast {a A B : Nat} (h1 : a = 2 ^ A) (h2 : A = B)
    (v : FormalRV.SQIRPort.QState a) :
    colReindex h2 (FormalRV.SQIRPort.QState.cast h1 v : Matrix (Fin (2 ^ A)) (Fin 1) ℂ)
      = FormalRV.SQIRPort.QState.cast (h1.trans (congrArg (2 ^ ·) h2)) v

noncomputable def cosetFullCircuit (m w rest cm N numWin : Nat)
    (TfamK TfamKinv : Nat → Nat → Nat → Nat)
    (hN : 0 < N) (h1N : 1 < N)
    (hbudget : 2 ^ cm * N ≤ 2 ^ (cm + rest)) :
    BaseUCom (m + cosetDim w (cm + rest))

theorem Shor_final_state_E2coset_eq_fullCircuit
    (m w rest cm N numWin : Nat)
    (TfamK TfamKinv : Nat → Nat → Nat → Nat)
    (hm : 0 < m) (hN : 0 < N) (h1N : 1 < N) (hcm : 0 < cm)
    (hbudget : 2 ^ cm * N ≤ 2 ^ (cm + rest)) :
    Shor_final_state_E2coset m w (cm + rest) N cm
        (physRunwayOracle m w (cm + rest) numWin TfamK TfamKinv)
      = FormalRV.SQIRPort.QState.cast (kronDim_eq m w (cm + rest))
          ((uc_eval (cosetFullCircuit m w rest cm N numWin TfamK TfamKinv hN h1N hbudget)
            * basis0 (m + cosetDim w (cm + rest))
            : Matrix (Fin (2 ^ (m + cosetDim w (cm + rest)))) (Fin 1) ℂ))

theorem gidney_inplace_coset_factoring_succeeds_circuit_prepared
    (a r N m w rest cm numWin ainv0 : Nat)
    (hm : 0 < m) (hw2 : 2 ≤ w) (hbits : numWin * w = cm + rest) (hb1 : 1 ≤ cm + rest)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ (cm + rest)) (hMN : 2 ^ cm * N ≤ 2 ^ (cm + rest))
    (h_inv0 : a * ainv0 % N = 1)
    (h_basic : FormalRV.SQIRPort.BasicSetting a r N m (cm + rest))
    (hr_even : Even r)
    (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)])
    (hcm : 0 < cm) :
    factoringSuccessProb_E2coset a N m w (cm + rest) cm
        (physRunwayOracle m w (cm + rest) numWin
          (fun k => tableValue (a ^ (2 ^ (revIndex m k)) % N) N w)

theorem orbitState_eq_stageProd_of_cast
    (m n anc : Nat) (f : Nat → BaseUCom (n + anc))
    (raw : Matrix (Fin (2 ^ (m + (n + anc)))) (Fin 1) ℂ) :
    ∀ j, orbitState (qpeStageMap m n anc f)
            (QState.cast (dim_assoc_eq m n anc) raw) j
        = QState.cast (dim_assoc_eq m n anc)
            ((stageProd m n anc f j * raw
              : Matrix (Fin (2 ^ (m + (n + anc)))) (Fin 1) ℂ))

noncomputable def composedQPECircuit (m n anc : Nat) (f : Nat → BaseUCom (n + anc)) :
    FormalRV.Framework.BaseUCom (m + (n + anc))

theorem stageProd_succ_eq_uc_eval (m n anc : Nat) (f : Nat → BaseUCom (n + anc))
    (hdim_pos : 0 < m + (n + anc)) :
    stageProd m n anc f (m + 1)
      = FormalRV.Framework.uc_eval (composedQPECircuit m n anc f)

noncomputable def E2runwayRaw (m w bits N cm : Nat) :
    Matrix (Fin (2 ^ (m + (bits + cosetAnc w bits)))) (Fin 1) ℂ

theorem shor_final_state_E2coset_eq_uc_eval
    (m w bits N cm : Nat) (hdim_pos : 0 < m + (bits + cosetAnc w bits))
    (f : Nat → FormalRV.Framework.BaseUCom (bits + cosetAnc w bits)) :
    Shor_final_state_E2coset m w bits N cm f
      = QState.cast (dim_assoc_eq m bits (cosetAnc w bits))
          ((FormalRV.Framework.uc_eval (composedQPECircuit m bits (cosetAnc w bits) f)
            * E2runwayRaw m w bits N cm
            : Matrix (Fin (2 ^ (m + (bits + cosetAnc w bits)))) (Fin 1) ℂ))

noncomputable def factoringSuccessProb_E2coset (a N m w bits cm : Nat)
    (f : Nat → FormalRV.Framework.BaseUCom (bits + cosetAnc w bits)) : ℝ

theorem factoringSuccessProb_E2coset_ge
    {a r N m w bits cm : Nat}
    (f : Nat → FormalRV.Framework.BaseUCom (bits + cosetAnc w bits))
    (hN : 1 < N) (h_ord : Order a r N) (hr_even : Even r)
    (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    factoringSuccessProb_E2coset a N m w bits cm f
      ≥ probability_of_success_E2coset a r N m w bits cm f

theorem gidney_inplace_coset_factoring_succeeds
    (a r N m w bits numWin cm ainv0 : Nat)
    (hm : 0 < m) (hw2 : 2 ≤ w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits) (hMN : 2 ^ cm * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_basic : FormalRV.SQIRPort.BasicSetting a r N m bits)
    (hr_even : Even r)
    (hgood : ¬ (a : ℤ) ^ (r / 2) ≡ -1 [ZMOD (N : ℤ)]) :
    factoringSuccessProb_E2coset a N m w bits cm
        (physRunwayOracle m w bits numWin
          (fun k => tableValue (a ^ (2 ^ (revIndex m k)) % N) N w)
          (fun k => tableValue (ainv0 ^ (2 ^ (revIndex m k)) % N) N w))

def scratchBase (w bits numWin q_start : Nat) : Nat

def isDataWire (bits p : Nat) : Prop

instance (bits p : Nat) : Decidable (isDataWire bits p)

def layoutAt (w bits numWin q_start : Nat) : Nat → Nat

theorem layoutAt_injective (w bits numWin q_start : Nat)
    (hS : q_start + 2 * bits + 1 ≤ scratchBase w bits numWin q_start) :
    Function.Injective (layoutAt w bits numWin q_start)

theorem layoutAt_data (w bits numWin q_start i : Nat) (hi : i < bits) :
    layoutAt w bits numWin q_start (2 * i + 1) = q_start + 2 * i + 1

theorem layoutAt_cin (w bits numWin q_start : Nat) :
    layoutAt w bits numWin q_start 0 = scratchBase w bits numWin q_start

theorem layoutAt_read (w bits numWin q_start i : Nat) :
    layoutAt w bits numWin q_start (2 * i + 2)
      = scratchBase w bits numWin q_start + (2 * i + 2)

theorem layoutAt_flag (w bits numWin q_start : Nat) :
    layoutAt w bits numWin q_start (flagW bits)
      = scratchBase w bits numWin q_start + flagW bits

theorem layoutAt_qbit (w bits numWin q_start k : Nat) :
    layoutAt w bits numWin q_start (qBase bits + k)
      = scratchBase w bits numWin q_start + (qBase bits + k)

theorem layoutAt_image_range (w bits numWin q_start p : Nat) :
    (q_start ≤ layoutAt w bits numWin q_start p
       ∧ layoutAt w bits numWin q_start p < q_start + 2 * bits + 1)
    ∨ scratchBase w bits numWin q_start ≤ layoutAt w bits numWin q_start p

def dimDivAt (w bits numWin cm q_start : Nat) : Nat

def divModNAt (w bits numWin cm N q_start : Nat) : Gate

theorem tcount_relabelGate (σ : Nat → Nat) (g : Gate) :
    Gate.tcount (relabelGate σ g) = Gate.tcount g

theorem divModNAt_tcount (w bits numWin cm N q_start : Nat) :
    Gate.tcount (divModNAt w bits numWin cm N q_start)
      = Gate.tcount (divModN bits cm N)

theorem wellTyped_relabelGate_src (σ : Nat → Nat) (hσ : Function.Injective σ)
    (d0 dim : Nat) (hmap : ∀ x, x < d0 → σ x < dim) :
    ∀ g, Gate.WellTyped d0 g → Gate.WellTyped dim (relabelGate σ g)
  | Gate.I,         hg => Nat.lt_of_le_of_lt (Nat.zero_le _) (hmap 0 hg)
  | Gate.X q,       hg => hmap q hg
  | Gate.CX c t,    hg => ⟨hmap c hg.1, hmap t hg.2.1, fun h => hg.2.2 (hσ h)⟩
  | Gate.CCX a b c, hg =>
      ⟨hmap a hg.1, hmap b hg.2.1, hmap c hg.2.2.1,
        fun h => hg.2.2.2.1 (hσ h), fun h => hg.2.2.2.2.1 (hσ h),
        fun h => hg.2.2.2.2.2 (hσ h)⟩
  | Gate.seq g₁ g₂, hg =>
      ⟨wellTyped_relabelGate_src σ hσ d0 dim hmap g₁ hg.1,

theorem divModNAt_wellTyped (w bits numWin cm N q_start : Nat)
    (hbits : 1 ≤ bits) (hcm : cm ≤ bits)
    (hS : q_start + 2 * bits + 1 ≤ scratchBase w bits numWin q_start) :
    Gate.WellTyped (dimDivAt w bits numWin cm q_start)
      (divModNAt w bits numWin cm N q_start)

theorem applyNat_relabelGate_frame (σ : Nat → Nat) :
    ∀ (g : Gate) (f : Nat → Bool) (p : Nat), (∀ q, σ q ≠ p) →
      Gate.applyNat (relabelGate σ g) f p = f p

theorem pullback_DivState
    (w bits numWin cm N q_start v : Nat) (f : Nat → Bool)
    (hbudget : N * 2 ^ cm ≤ 2 ^ bits) (hcm : cm ≤ bits) (hN : 0 < N)
    (hv : v < N * 2 ^ cm)
    (h_data : ∀ i, i < bits → f (q_start + 2 * i + 1) = v.testBit i)
    (h_cin : f (scratchBase w bits numWin q_start) = false)
    (h_read : ∀ i, i < bits →
        f (scratchBase w bits numWin q_start + (2 * i + 2)) = false)
    (h_flag : f (scratchBase w bits numWin q_start + flagW bits) = false)
    (h_quot : ∀ k, k < cm →
        f (scratchBase w bits numWin q_start + (qBase bits + k)) = false) :
    DivState bits cm N v (fun p => f (layoutAt w bits numWin q_start p))

theorem divModNAt_decode
    (w bits numWin cm N q_start z j : Nat) (f : Nat → Bool)
    (hbits : 1 ≤ bits) (hN : 0 < N) (hcm : cm ≤ bits)
    (hbudget : 2 ^ cm * N ≤ 2 ^ bits)
    (hz : z < N) (hj : j < 2 ^ cm)
    (hS : q_start + 2 * bits + 1 ≤ scratchBase w bits numWin q_start)
    (h_data : ∀ i, i < bits → f (q_start + 2 * i + 1) = (z + j * N).testBit i)
    (h_cin : f (scratchBase w bits numWin q_start) = false)
    (h_read : ∀ i, i < bits →
        f (scratchBase w bits numWin q_start + (2 * i + 2)) = false)
    (h_flag : f (scratchBase w bits numWin q_start + flagW bits) = false)
    (h_quot : ∀ k, k < cm →

theorem ge2021_ekera_hastad_per_run (ℓ m d : ℕ)
    (hℓ : 1 ≤ ℓ) (hm : 2 ≤ m) (hd0 : 0 < d) (hdlt : d < 2 ^ m)
    (a b N : ℕ) (hab : b ≤ a) (hd : d = a + b) (hN : N = (2 * a + 1) * (2 * b + 1)) :
    (1 / 8 : ℝ) ≤ ∑ j ∈ goodOutcomes ℓ m d, ehProb ℓ m d j (kPair ℓ m d j)
      ∧ ((d + 1) + ((d + 1) * (d + 1) - N).sqrt = 2 * a + 1
          ∧ (d + 1) - ((d + 1) * (d + 1) - N).sqrt = 2 * b + 1)

theorem ge2021_ekera_hastad_amplified (S : EkeraDLPSuccess) :
    (1 - 3 / (2 : ℝ) ^ S.τ) * ekeraBalancedFactor S.Δ S.t S.τ ≤ S.successProb

def ge2021_hw : QualtranPhysicalParameters

def yBase (w bits : Nat) : Nat

def dataSrc (bits j : Nat) : Nat

def yDst (w bits j : Nat) : Nat

private theorem mulInputOf_cuc_encodeReg (w bits numWin v p : Nat)
    (hp : p ≠ ulookup_ctrl_idx) :
    mulInputOf cuccaroAdder w bits numWin v p
      = encodeReg (1 + 2 * w + (2 * bits + 1)) (numWin * w) v p

private theorem mulInputOf_cuc_y_bit (w bits numWin v i : Nat)
    (hi : i < numWin * w) :
    mulInputOf cuccaroAdder w bits numWin v (1 + 2 * w + (2 * bits + 1) + i)
      = v.testBit i

def readyBridge (w bits : Nat) : Gate

theorem readyBridge_tcount (w bits : Nat) :
    (readyBridge w bits).tcount = 0

theorem readyBridge_wellTyped (w bits D : Nat)
    (hbits : 0 < bits) (_hsep : bits ≤ 1 + 2 * w) (hD : yBase w bits + bits < D) :
    Gate.WellTyped D (readyBridge w bits)

def DataBandReady (bits anc x : Nat) (f : Nat → Bool) : Prop

theorem readyBridge_establishes_ModNMulReady
    (w bits numWin anc x : Nat)
    (hbits : 0 < bits) (hsep : bits ≤ 1 + 2 * w) (hbw : numWin * w = bits)
    (hxbits : x < 2 ^ bits)
    (f : Nat → Bool) (hf : DataBandReady bits anc x f) :
    ModNMulReady w bits numWin x (Gate.applyNat (readyBridge w bits) f)

def inPlaceMulData (w bits N numWin c cinv : Nat) : Gate

theorem inPlaceMulData_tcount (w bits N numWin c cinv : Nat) :
    (inPlaceMulData w bits N numWin c cinv).tcount
      = (windowedModNMulInPlace w bits c cinv N numWin).tcount

theorem inPlaceMulData_wellTyped (w bits N numWin c cinv D : Nat)
    (hbits : 0 < bits) (hsep : bits ≤ 1 + 2 * w)
    (hD : yBase w bits + bits < D)
    (hmul : Gate.WellTyped D (windowedModNMulInPlace w bits c cinv N numWin)) :
    Gate.WellTyped D (inPlaceMulData w bits N numWin c cinv)

theorem ModNMulReady_rigid {w bits numWin v : Nat} {f g : Nat → Bool}
    (hf : ModNMulReady w bits numWin v f) (hg : ModNMulReady w bits numWin v g) :
    f = g

theorem inPlaceMulData_apply
    (w bits N numWin c cinv anc x D : Nat)
    (hw : 0 < w) (hbits : 0 < bits) (hsep : bits ≤ 1 + 2 * w)
    (hbw : numWin * w = bits)
    (hN_pos : 0 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hx : x < N) (hcinv : cinv < N) (hinv : c * cinv % N = 1)
    (hD : yBase w bits + bits < D)
    (f : Nat → Bool) (hf : DataBandReady bits anc x f) :
    DataBandReady bits anc ((c * x) % N)
      (Gate.applyNat (inPlaceMulData w bits N numWin c cinv) f)

def yBase (w bits : Nat) : Nat

def scratchBase (bits : Nat) : Nat

def isValWire (w bits p : Nat) : Prop

instance (w bits p : Nat) : Decidable (isValWire w bits p)

def layoutMul (w bits : Nat) : Nat → Nat

theorem layoutMul_injective (w bits : Nat) :
    Function.Injective (layoutMul w bits)

theorem layoutMul_val (w bits i : Nat) (hi : i < bits) :
    layoutMul w bits (yBase w bits + i) = bits - 1 - i

theorem layoutMul_ctrl (w bits : Nat) :
    layoutMul w bits ulookup_ctrl_idx = scratchBase bits

theorem layoutMul_nonval (w bits p : Nat) (hp : ¬ isValWire w bits p) :
    layoutMul w bits p = scratchBase bits + p

theorem layoutMul_image_range (w bits p : Nat) :
    layoutMul w bits p < bits ∨ bits ≤ layoutMul w bits p

theorem tcount_relabelGate (σ : Nat → Nat) (g : Gate) :
    Gate.tcount (relabelGate σ g) = Gate.tcount g

theorem wellTyped_relabelGate_src (σ : Nat → Nat) (hσ : Function.Injective σ)
    (d0 dim : Nat) (hmap : ∀ x, x < d0 → σ x < dim) :
    ∀ g, Gate.WellTyped d0 g → Gate.WellTyped dim (relabelGate σ g)
  | Gate.I,         hg => Nat.lt_of_le_of_lt (Nat.zero_le _) (hmap 0 hg)
  | Gate.X q,       hg => hmap q hg
  | Gate.CX c t,    hg => ⟨hmap c hg.1, hmap t hg.2.1, fun h => hg.2.2 (hσ h)⟩
  | Gate.CCX a b c, hg =>
      ⟨hmap a hg.1, hmap b hg.2.1, hmap c hg.2.2.1,
        fun h => hg.2.2.2.1 (hσ h), fun h => hg.2.2.2.2.1 (hσ h),
        fun h => hg.2.2.2.2.2 (hσ h)⟩
  | Gate.seq g₁ g₂, hg =>
      ⟨wellTyped_relabelGate_src σ hσ d0 dim hmap g₁ hg.1,

theorem applyNat_relabelGate_frame (σ : Nat → Nat) :
    ∀ (g : Gate) (f : Nat → Bool) (p : Nat), (∀ q, σ q ≠ p) →
      Gate.applyNat (relabelGate σ g) f p = f p

def dimNative (w bits : Nat) : Nat

def Dmul (w bits : Nat) : Nat

def inPlaceMulDataAt (w bits N numWin c cinv : Nat) : Gate

theorem inPlaceMulDataAt_tcount (w bits N numWin c cinv : Nat) :
    Gate.tcount (inPlaceMulDataAt w bits N numWin c cinv)
      = Gate.tcount (windowedModNMulInPlace w bits c cinv N numWin)

theorem inPlaceMulDataAt_wellTyped (w bits N numWin c cinv : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) :
    Gate.WellTyped (Dmul w bits) (inPlaceMulDataAt w bits N numWin c cinv)

theorem mulInputOf_cuc_y_bit_local (w bits numWin v i : Nat)
    (hi : i < numWin * w) :
    mulInputOf cuccaroAdder w bits numWin v (1 + 2 * w + (2 * bits + 1) + i)
      = v.testBit i

def DataMulReady (w bits anc x : Nat) (f : Nat → Bool) : Prop

theorem pullback_ModNMulReady
    (w bits numWin anc x : Nat) (f : Nat → Bool)
    (hbits : 0 < bits) (hbw : numWin * w = bits) (hxbits : x < 2 ^ bits)
    (hf : DataMulReady w bits anc x f) :
    ModNMulReady w bits numWin x (fun p => f (layoutMul w bits p))

theorem inPlaceMulDataAt_apply
    (w bits N numWin c cinv anc x : Nat) (f : Nat → Bool)
    (hw : 0 < w) (hbits : 0 < bits) (hbw : numWin * w = bits)
    (hN_pos : 0 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hx : x < N) (hcinv : cinv < N) (hinv : c * cinv % N = 1)
    (hf : DataMulReady w bits anc x f) :
    -- DATA band encodes (c·x)%N, SAME big-endian convention.
    (∀ j, j < bits →
        Gate.applyNat (inPlaceMulDataAt w bits N numWin c cinv) f j
          = encodeDataZeroAnc bits anc ((c * x) % N) j)
    -- scratch restored clean: control still set …
    ∧ Gate.applyNat (inPlaceMulDataAt w bits N numWin c cinv) f (scratchBase bits)

def ge2021_shor : ShorAlgorithm

def ge2021_code : QECCode

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

theorem decodeReg_eq_cuccaro_target_val (bits q_start : Nat) (f : Nat → Bool) :
    decodeReg (fun i => q_start + 2 * i + 1) bits f
      = cuccaro_target_val bits q_start f

theorem babbushLookupAddAt_anc_cleared
    (w W bits : Nat) (T : Nat → Nat) (addrBase ancBase q_start : Nat) (f : Nat → Bool)
    (i : Nat) (hi : i < w) (hWb : W ≤ bits)
    (hanc_hi : q_start + 2 * bits < ancBase + i) :
    EGate.applyNat (babbushLookupAddAt w W T bits addrBase ancBase q_start) f
        (ancBase + i) = false

theorem multiplyAddAt_consumed_fold
    (w bits numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (g0 : Nat → Bool)
    (haddr0 : ∀ k, k < numWin →
      decodeReg (fun i => addrBaseOf w bits q_start k + i) w g0 = window w y k) :
    ∀ n, n ≤ numWin →
      (∀ k, k < n →
          decodeReg (fun i => addrBaseOf w bits q_start k + i) w
            (EGate.applyNat (seqAll ((List.range n).map (laAt w bits bits Tfam q_start m))) g0)
          = window w y k)
      ∧ (∀ k, n ≤ k → k < numWin →

theorem multiplyAddAt_full_M1_address_preserved
    (w bits numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (g0 : Nat → Bool)
    (haddr0 : ∀ k, k < numWin →
      decodeReg (fun i => addrBaseOf w bits q_start k + i) w g0 = window w y k)
    (k : Nat) (hk : k < numWin) :
    decodeReg (fun t => addrBaseOf w bits q_start k + t) w
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0)
      = window w y k

theorem multiplyAddAt_full_M2_anc_cleared
    (w bits numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (g0 : Nat → Bool)
    (haddr0 : ∀ k, k < numWin →
      decodeReg (fun i => addrBaseOf w bits q_start k + i) w g0 = window w y k)
    (k : Nat) (hk : k < numWin) (t : Nat) (ht : t < w) :
    EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0
        (ancBaseOf w bits q_start k + t) = false

theorem multiplyAddAt_full_M3_frame
    (w bits numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (g0 : Nat → Bool)
    (haddr0 : ∀ k, k < numWin →
      decodeReg (fun i => addrBaseOf w bits q_start k + i) w g0 = window w y k)
    (p : Nat)
    (hp : p < q_start ∨ p ≥ q_start + 2 * bits + 1 + numWin * (2 * w)) :
    EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0 p = g0 p

theorem multiplyAddAt_full_output
    (w bits numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0)
    (out : Nat → Bool)
    (hout : out = EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0) :
    -- M1 ADDRESS-PRESERVED
    (∀ k, k < numWin →
        decodeReg (fun t => addrBaseOf w bits q_start k + t) w out = window w y k)
    -- M2 PER-WINDOW-ANCILLA-CLEARED
    ∧ (∀ k, k < numWin → ∀ t, t < w → out (ancBaseOf w bits q_start k + t) = false)
    -- M3 FRAME

def scatterAddr (w bits q_start j : Nat) : Nat

def ge2021_adaptIn (w bits q_start : Nat) (_i : Nat) : Gate

theorem ge2021_adaptIn_tfree (w bits q_start i : Nat) :
    Gate.tcount (ge2021_adaptIn w bits q_start i) = 0

theorem scatterAddr_inj (w bits q_start : Nat) (hw : 0 < w)
    (j k : Nat) (_hj : j < bits) (_hk : k < bits) (hne : j ≠ k) :
    scatterAddr w bits q_start j ≠ scatterAddr w bits q_start k

theorem ge2021_adaptIn_clean
    (w bits anc numWin N _a q_start : Nat)
    (hw : 0 < w) (hq : 0 < q_start) (hanc : 0 < anc)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N) :
    CountGateMulInput w bits numWin x q_start
      (Gate.applyNat (ge2021_adaptIn w bits q_start i)
        (encodeDataZeroAnc bits anc x))

private theorem wellTyped_foldl_seq_aux (dim : Nat) (G : Nat → Gate) :
    ∀ (l : List Nat) (init : Gate), Gate.WellTyped dim init →
      (∀ k ∈ l, Gate.WellTyped dim (G k)) →
      Gate.WellTyped dim (l.foldl (fun g i => Gate.seq g (G i)) init)

private theorem cxCascade_wellTyped_aux (ctrl tgt : Nat → Nat) (n dim : Nat)
    (h0 : 0 < dim)
    (h : ∀ i, i < n → ctrl i < dim ∧ tgt i < dim ∧ ctrl i ≠ tgt i) :
    Gate.WellTyped dim (cxCascade ctrl tgt n)

private theorem swapCascade_wellTyped_aux (u v : Nat → Nat) (n dim : Nat)
    (h0 : 0 < dim)
    (h : ∀ i, i < n → u i < dim ∧ v i < dim ∧ u i ≠ v i) :
    Gate.WellTyped dim (swapCascade u v n)

theorem ge2021_adaptIn_wellTyped
    (w bits anc q_start : Nat) (hbpos : 0 < bits)
    (hfit : ∀ j, j < bits → scatterAddr w bits q_start j < bits + anc)
    (i : Nat) :
    Gate.WellTyped (bits + anc) (ge2021_adaptIn w bits q_start i)

def ge2021_modExpAtLayoutAdapter
    (w bits numWin N a q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start) (hbpos : 0 < bits)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    -- table family realises the per-iterate windowed modular product:
    (mblkOf : Nat → Nat)
    (htable : ∀ i k v,
      Tfam (mblkOf i) k v = ((a ^ (2 ^ i)) * (2 ^ w) ^ k * v) % 2 ^ bits)
    -- the IN-adapter address registers fit the canonical dimension:
    (hfit : ∀ j, j < bits →
      scatterAddr w bits q_start j < bits + (2 * w + 2 * bits + 3))
    -- RESIDUAL (B): the deferred stacked-region block width is well-typed:

theorem ge2021_modExpAt_shor_succeeds_given_out_readout
    {w bits numWin N a ainv0 r m q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (h_setting : ShorSetting a r N m bits)
    (mblkOf : Nat → Nat)
    (htable : ∀ i k v,
      Tfam (mblkOf i) k v = ((a ^ (2 ^ i)) * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hfit : ∀ j, j < bits →

def ancBig (w bits numWin cm : Nat) : Nat

theorem ancBig_pad (w bits numWin cm : Nat) :
    2 * w + 2 * bits + 3 ≤ ancBig w bits numWin cm

theorem D_ge_dimDivAt (w bits numWin cm : Nat) :
    dimDivAt w bits numWin cm 1 ≤ bits + ancBig w bits numWin cm

theorem D_ge_Dmul (w bits : Nat) (numWin cm : Nat) :
    Dmul w bits ≤ bits + ancBig w bits numWin cm

theorem D_ge_dimRadd (w bits numWin cm : Nat) :
    dimRadd w bits numWin ≤ bits + ancBig w bits numWin cm

theorem unaryQROMAt_wellTypedAt (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase dim : Nat) (hdim : 0 < dim) :
    ∀ (d ctrl base : Nat), QROMRevWT pos W addrBase ancBase d ctrl dim →
      EGate.WellTypedAt dim (unaryQROMAt pos W T addrBase ancBase d ctrl base)
  | 0, ctrl, base, H =>

theorem babbushLookupAddAt_wellTypedAt (w W : Nat) (T : Nat → Nat)
    (bits addrBase ancBase q_start dim : Nat) (hdim : 0 < dim) (hW : W ≤ bits)
    (hQ : QROMRevWT (addendIdx q_start) W addrBase ancBase w 0 dim)
    (hacc : q_start + 2 * bits + 1 ≤ dim) :
    EGate.WellTypedAt dim (babbushLookupAddAt w W T bits addrBase ancBase q_start)

theorem seqAll_foldl_wellTypedAt (dim : Nat) :
    ∀ (gs : List EGate) (seed : EGate),
      EGate.WellTypedAt dim seed → (∀ g ∈ gs, EGate.WellTypedAt dim g) →
      EGate.WellTypedAt dim (gs.foldl EGate.seq seed)
  | [], seed, hseed, _ => hseed
  | g :: rest, seed, hseed, h =>
      seqAll_foldl_wellTypedAt dim rest (EGate.seq seed g)
        ⟨hseed, h g (List.mem_cons_self ..)⟩
        (fun x hx => h x (List.mem_cons_of_mem g hx))

theorem seqAll_wellTypedAt (dim : Nat) (h0 : 0 < dim) (gs : List EGate)
    (h : ∀ g ∈ gs, EGate.WellTypedAt dim g) :
    EGate.WellTypedAt dim (seqAll gs)

theorem multiplyAddAt_wellTypedAt (w bits numWin a i : Nat) (hw : 0 < w) (hbits : 1 ≤ bits) :
    EGate.WellTypedAt (dimRadd w bits numWin) (egG2 w bits numWin a i)

theorem egRfree_wellTyped
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hcm : cm ≤ bits)
    (i : Nat) :
    EGate.WellTypedAt (bits + ancBig w bits numWin cm)
      (egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)

theorem encodeDataZeroAnc_anc_irrel {n anc anc' x : Nat}
    (hx : x < 2 ^ n) (h1 : 0 < anc) (h1' : 0 < anc') :
    encodeDataZeroAnc n anc x = encodeDataZeroAnc n anc' x

theorem egRfree_residue_ancBig
    (w bits numWin cm N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    ModExpAtEncodedMatchesResidue a N bits (ancBig w bits numWin cm)
      (fun i => egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)
      (fun _ x => encodeDataZeroAnc bits (ancBig w bits numWin cm) x)

def egRfree_measuredEqRev
    (w bits numWin cm N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    MeasuredEqualsReversibleOnEncoded a N bits (ancBig w bits numWin cm)
      (fun i => egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)
      (fun _ x => encodeDataZeroAnc bits (ancBig w bits numWin cm) x)

theorem egRfree_shor_succeeds
    (w bits numWin cm N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (ancBig w bits numWin cm)
        (egRfree_measuredEqRev w bits numWin cm N a ainv0
          hw hbits hb1 hN1 hN2 hcm h_inv0).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem egRfree_tcount (w bits numWin cm N a : Nat) (unmul : Nat → Gate) (i : Nat) :
    EGate.tcount (egRfree w bits numWin cm N a unmul i)
      = EGate.tcount (multiplyAddAt w bits bits (tableFam w bits a) 1 i numWin)
        + 2 * Gate.tcount (divModNAt w bits numWin cm N 1)
        + Gate.tcount (unmul i)
        + Gate.tcount (inPlaceMulDataAt w bits N numWin (a ^ (2 ^ i)) (modInv N (a ^ (2 ^ i))))

theorem egRfree_shor_AND_count
    (w bits numWin cm N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (ancBig w bits numWin cm)
        (egRfree_measuredEqRev w bits numWin cm N a ainv0
          hw hbits hb1 hN1 hN2 hcm h_inv0).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4
    ∧ ∀ i, EGate.tcount (egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)

theorem tcount_reverse (g : Gate) : Gate.tcount (Gate.reverse g) = Gate.tcount g

def copyBand (src dst : Nat → Nat) (n : Nat) : Gate

theorem copyBand_tcount (src dst : Nat → Nat) (n : Nat) :
    Gate.tcount (copyBand src dst n) = 0

theorem copyBand_at (src dst : Nat → Nat) (n : Nat) (f : Nat → Bool)
    (hdst_inj : ∀ i k, i < n → k < n → i ≠ k → dst i ≠ dst k)
    (hsd : ∀ i k, i < n → k < n → src i ≠ dst k)
    (i : Nat) (hi : i < n) :
    Gate.applyNat (copyBand src dst n) f (dst i)
      = xor (f (dst i)) (f (src i))

theorem copyBand_frame (src dst : Nat → Nat) (n : Nat) (f : Nat → Bool)
    (p : Nat) (hp : ∀ i, i < n → p ≠ dst i) :
    Gate.applyNat (copyBand src dst n) f p = f p

theorem copyBand_wellTyped (src dst : Nat → Nat) (n dim : Nat) (h0 : 0 < dim)
    (h : ∀ i, i < n → src i < dim ∧ dst i < dim ∧ src i ≠ dst i) :
    Gate.WellTyped dim (copyBand src dst n)

def tableFam (w bits a : Nat) : Nat → Nat → Nat → Nat

def Rbase (w bits numWin cm : Nat) : Nat

def Rwire (w bits numWin cm i : Nat) : Nat

def egG1 (w bits i : Nat) : Gate

def egG2 (w bits numWin a i : Nat) : EGate

def egG3 (w bits numWin cm N : Nat) : Gate

def egG4 (w bits numWin cm : Nat) : Gate

def egG5 (w bits numWin cm N : Nat) : Gate

def egG7 (w bits i : Nat) : Gate

def egG8 (w bits numWin N a i : Nat) : Gate

def egG9 (w bits numWin cm : Nat) : Gate

def eg (w bits numWin cm N a : Nat) (unmul : Nat → Gate) (i : Nat) : EGate

theorem eg_contains_multiplyAddAt (w bits numWin cm N a : Nat) (unmul : Nat → Gate) (i : Nat) :
    egG2 w bits numWin a i = multiplyAddAt w bits bits (tableFam w bits a) 1 i numWin

theorem eg_tcount (w bits numWin cm N a : Nat) (unmul : Nat → Gate) (i : Nat) :
    EGate.tcount (eg w bits numWin cm N a unmul i)
      = EGate.tcount (multiplyAddAt w bits bits (tableFam w bits a) 1 i numWin)
        + 2 * Gate.tcount (divModNAt w bits numWin cm N 1)
        + Gate.tcount (unmul i)
        + Gate.tcount (inPlaceMulDataAt w bits N numWin (a ^ (2 ^ i)) (modInv N (a ^ (2 ^ i))))

theorem s1_countGateMulInput
    (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N) :
    CountGateMulInput w bits numWin x 1
      (Gate.applyNat (egG1 w bits i)
        (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x))

theorem tableFam_spec (w bits a i k v : Nat) :
    tableFam w bits a i k v = (a ^ (2 ^ i) * (2 ^ w) ^ k * v) % 2 ^ bits

theorem pow_w_numWin (w bits numWin : Nat) (hbits : numWin * w = bits) :
    (2 ^ w) ^ numWin = 2 ^ bits

theorem s2_acc_value
    (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (hnowrap : a ^ (2 ^ i) * x < 2 ^ bits) :
    decodeReg (fun j => 1 + 2 * j + 1) bits
        (EGate.applyNat (egG2 w bits numWin a i)
          (Gate.applyNat (egG1 w bits i)
            (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)))
      = a ^ (2 ^ i) * x

theorem egG1_frame_high
    (w bits numWin : Nat) (hw : 0 < w) (hbits : numWin * w = bits)
    (i p : Nat) (hp : DivModNAt.scratchBase w bits numWin 1 ≤ p) (f : Nat → Bool) :
    Gate.applyNat (egG1 w bits i) f p = f p

theorem s2_acc_bits
    (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (hnowrap : a ^ (2 ^ i) * x < 2 ^ bits)
    (j : Nat) (hj : j < bits) :
    (EGate.applyNat (egG2 w bits numWin a i)
        (Gate.applyNat (egG1 w bits i)
          (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x))) (1 + 2 * j + 1)
      = (a ^ (2 ^ i) * x).testBit j

theorem s2_high_clean
    (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (p : Nat) (hp : DivModNAt.scratchBase w bits numWin 1 ≤ p) :
    (EGate.applyNat (egG2 w bits numWin a i)
        (Gate.applyNat (egG1 w bits i)
          (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x))) p = false

def s2State (w bits numWin a i x : Nat) : Nat → Bool

theorem s3_divMod
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits) (hbudget : 2 ^ cm * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (hbudget_nowrap : a ^ (2 ^ i) * x < N * 2 ^ cm) :
    -- REMAINDER in place: ACC band decodes to z = v % N.
    decodeReg (fun j => 1 + 2 * j + 1) bits
        (Gate.applyNat (egG3 w bits numWin cm N) (s2State w bits numWin a i x))
      = (a ^ (2 ^ i) * x) % N
    -- QUOTIENT band: bit k of j = v / N, on the fresh quotient wires.

theorem egG3_frame_above
    (w bits numWin cm N : Nat)
    (hbits : 1 ≤ bits) (hcm : cm ≤ bits)
    (p : Nat) (hp : dimDivAt w bits numWin cm 1 ≤ p) (f : Nat → Bool) :
    Gate.applyNat (egG3 w bits numWin cm N) f p = f p

theorem s3_acc_bit
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits) (hbudget : 2 ^ cm * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (hbudget_nowrap : a ^ (2 ^ i) * x < N * 2 ^ cm)
    (k : Nat) (hk : k < bits) :
    Gate.applyNat (egG3 w bits numWin cm N) (s2State w bits numWin a i x) (1 + 2 * k + 1)
      = ((a ^ (2 ^ i) * x) % N).testBit k

theorem s3_R_clean
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (i x : Nat) (hx : x < N) (k : Nat) (hk : k < bits) :
    Gate.applyNat (egG3 w bits numWin cm N) (s2State w bits numWin a i x)
        (Rwire w bits numWin cm k) = false

theorem Rwire_inj (w bits numWin cm : Nat) (k k' : Nat) (h : k ≠ k') :
    Rwire w bits numWin cm k ≠ Rwire w bits numWin cm k'

theorem acc_ne_Rwire (w bits numWin cm : Nat) (hb1 : 1 ≤ bits)
    (k k' : Nat) (hk : k < bits) :
    1 + 2 * k + 1 ≠ Rwire w bits numWin cm k'

theorem egG4_wellTyped (w bits numWin cm : Nat) (hb1 : 1 ≤ bits) :
    Gate.WellTyped (Rbase w bits numWin cm + bits) (egG4 w bits numWin cm)

def s5State (w bits numWin cm N a i x : Nat) : Nat → Bool

theorem s5_collapse
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits) (hbudget : 2 ^ cm * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N)
    (hbudget_nowrap : a ^ (2 ^ i) * x < N * 2 ^ cm) :
    -- (A) on [0, dimDivAt): identity, back to s2.
    (∀ p, p < dimDivAt w bits numWin cm 1 →
        s5State w bits numWin cm N a i x p = s2State w bits numWin a i x p)
    -- (B) on the R band: z.testBit k.
    ∧ (∀ k, k < bits →

def t6State (w bits numWin cm N a i x : Nat) : Nat → Bool

def UnmulSpec (w bits numWin cm N a : Nat) (unmul : Nat → Gate) : Prop

theorem Rbase_ge_Dmul (w bits numWin cm : Nat) :
    Dmul w bits ≤ Rbase w bits numWin cm

theorem Dmul_ge_encDim (w bits : Nat) : bits + (2 * w + 2 * bits + 3) ≤ Dmul w bits

theorem Rwire_ge_encDim (w bits numWin cm : Nat) (k : Nat) :
    bits + (2 * w + 2 * bits + 3) ≤ Rwire w bits numWin cm k

theorem Rwire_ge_Dmul (w bits numWin cm : Nat) (k : Nat) :
    Dmul w bits ≤ Rwire w bits numWin cm k

theorem egG1_wellTyped_Rbase (w bits numWin cm : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (i : Nat) :
    Gate.WellTyped (Rbase w bits numWin cm) (egG1 w bits i)

theorem mem_Rband_iff (w bits numWin cm p : Nat) :
    (∃ k, k < bits ∧ p = Rwire w bits numWin cm k)
      ↔ (Rbase w bits numWin cm ≤ p ∧ p < Rbase w bits numWin cm + bits)

theorem t7_unscatter
    (w bits numWin cm N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (i x : Nat) (hx : x < N) :
    (∀ p, p < Rbase w bits numWin cm →
        Gate.applyNat (egG7 w bits i) (t6State w bits numWin cm N a i x) p
          = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x p)
    ∧ (∀ k, k < bits →
        Gate.applyNat (egG7 w bits i) (t6State w bits numWin cm N a i x)
            (Rwire w bits numWin cm k)
          = ((a ^ (2 ^ i) * x) % N).testBit k)

theorem inv_exists (N a ainv0 i : Nat) (hN1 : 1 < N) (h_inv0 : a * ainv0 % N = 1) :
    ∃ d, (a ^ (2 ^ i) * d) % N = 1

def egRfree (w bits numWin cm N a : Nat) (unmul : Nat → Gate) (i : Nat) : EGate

theorem egRfree_contains_multiplyAddAt (w bits numWin cm N a : Nat) (_unmul : Nat → Gate) (i : Nat) :
    egG2 w bits numWin a i = multiplyAddAt w bits bits (tableFam w bits a) 1 i numWin

def UnmulSpecRfree (w bits numWin N a : Nat) (unmul : Nat → Gate) : Prop

theorem s2_restored_after_G3G5
    (w bits numWin cm N a : Nat)
    (hbits : 1 ≤ bits) (hcm : cm ≤ bits)
    (i x : Nat) :
    Gate.applyNat (egG5 w bits numWin cm N)
        (Gate.applyNat (egG3 w bits numWin cm N) (s2State w bits numWin a i x))
      = s2State w bits numWin a i x

theorem block_matches_residue_direct
    (w bits numWin cm N a ainv0 : Nat) (unmul : Nat → Gate)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hunmul : UnmulSpecRfree w bits numWin N a unmul)
    (i x : Nat) (hx : x < N) :
    EGate.applyNat (egRfree w bits numWin cm N a unmul i)
        (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)
      = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) ((a ^ (2 ^ i) * x) % N)

theorem egRfree_matchesResidue
    (w bits numWin cm N a ainv0 : Nat) (unmul : Nat → Gate)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hunmul : UnmulSpecRfree w bits numWin N a unmul) :
    ShorComposedFinal.ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3)
      (fun i => egRfree w bits numWin cm N a unmul i)
      (fun _ x => encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem step0_block_is_unreduced_product
    (w bits a numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0) :
    decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0)
      = (a * y) % 2 ^ bits

structure ModExpAtReductionAdapter
    (w bits anc numWin N a q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)

def ModExpAtReductionAdapter.conjugatedReductionBlock
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits anc numWin N a q_start Tfam) (i : Nat) : EGate

theorem ModExpAtReductionAdapter.conjugatedReductionBlock_toffoli_decompose
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits anc numWin N a q_start Tfam) (i : Nat) :
    EGate.toffoli (L.conjugatedReductionBlock i)
      = (Gate.tcount (L.adaptIn i)
          + EGate.tcount (multiplyAddAt w bits bits Tfam q_start (L.mblkOf i) numWin)
          + Gate.tcount (L.adaptOutReduce i)) / 7

theorem ModExpAtReductionAdapter.conjugatedReductionBlock_tcount
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits anc numWin N a q_start Tfam) (i : Nat) :
    EGate.tcount (L.conjugatedReductionBlock i)
      = EGate.tcount (multiplyAddAt w bits bits Tfam q_start (L.mblkOf i) numWin)
        + Gate.tcount (L.adaptOutReduce i)

theorem modExpAtReductionBlock_matches_residue
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits anc numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (i x : Nat) (hx : x < N) :
    EGate.applyNat (L.conjugatedReductionBlock i)
        (FormalRV.BQAlgo.encodeDataZeroAnc bits anc x)
      = FormalRV.BQAlgo.encodeDataZeroAnc bits anc (((a ^ (2 ^ i)) * x) % N)

def modExpAtEncodedMatchesResidue_of_reductionAdapter
    {w bits numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits) :
    ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3)
      (fun i => L.conjugatedReductionBlock i)
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

def ge2021_modExpAtReduction_measuredEqRev
    {w bits numWin N a ainv0 q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits) :
    MeasuredEqualsReversibleOnEncoded a N bits (2 * w + 2 * bits + 3)
      (fun i => L.conjugatedReductionBlock i)
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem ge2021_modExpAtReduction_shor_succeeds
    {w bits numWin N a ainv0 r m q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_modExpAtReduction_measuredEqRev L hw hq hbits hb1 hN1 hN2 h_inv0 hnowrap).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem ge2021_modExpAtReduction_bound_AND_honest_count
    {w bits numWin N a ainv0 r m q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtReductionAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_modExpAtReduction_measuredEqRev L hw hq hbits hb1 hN1 hN2 h_inv0 hnowrap).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem measEncode_block_matches_residue
    (w bits numWin N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (i x : Nat) (hx : x < N) :
    EGate.applyNat
        (measWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)
          (modInv N (a ^ (2 ^ i))))
        (FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)
      = FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3)
          ((a ^ (2 ^ i) * x) % N)

def ge2021_modExpAtResidue
    (w bits numWin N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3)
      (fun i => measWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)
        (modInv N (a ^ (2 ^ i))))
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

def ge2021_measEncode_measuredEqRev
    (w bits numWin N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    MeasuredEqualsReversibleOnEncoded a N bits (2 * w + 2 * bits + 3)
      (fun i => measWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)
        (modInv N (a ^ (2 ^ i))))
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem ge2021_measEncode_shor_succeeds
    (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_measEncode_measuredEqRev w bits numWin N a ainv0
          hw hbits hb1 hN1 hN2 h_inv0).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem ge2021_measEncode_shor_AND_count
    (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_measEncode_measuredEqRev w bits numWin N a ainv0
          hw hbits hb1 hN1 hN2 h_inv0).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4
    ∧ ∀ i, EGate.toffoli
        (measWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)

theorem ge2021_oracle_correct_AND_counted_AND_bound
    (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    (∀ i x, x < N →
        EGate.applyNat
            (measWindowedModNEncodeGate w bits N numWin ((a ^ (2 ^ i)) % N)
              (modInv N (a ^ (2 ^ i))))
            (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)
          = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) ((a ^ (2 ^ i) * x) % N))

def unaryQROMAtRev (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) (addrBase ancBase : Nat) :
    Nat → Nat → Nat → Gate
  | 0,     ctrl, base =>
      cx_gates_from_indices ctrl (wordCnotsAt pos W (T base))
  | d + 1, ctrl, base =>
      Gate.seq (Gate.seq (Gate.seq (Gate.seq (Gate.seq
        (Gate.CCX ctrl (addrBase + d) (ancBase + d))                                  -- anc ← ctrl∧bit_d
        (unaryQROMAtRev pos W T addrBase ancBase d (ancBase + d) (base + 2 ^ d)))     -- bit_d = 1 half
        (Gate.CX ctrl (ancBase + d)))                                                 -- anc ← ctrl∧¬bit_d
        (unaryQROMAtRev pos W T addrBase ancBase d (ancBase + d) base))               -- bit_d = 0 half
        (Gate.CX ctrl (ancBase + d)))                                                 -- restore anc
        (Gate.CCX ctrl (addrBase + d) (ancBase + d))                                  -- reversible-uncompute anc

theorem tcount_unaryQROMAtRev (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase : Nat) :
    ∀ (d ctrl base : Nat),
      Gate.tcount (unaryQROMAtRev pos W T addrBase ancBase d ctrl base)
        = 7 * (2 ^ (d + 1) - 2)
  | 0, ctrl, base =>

structure QROMRevWT (pos : Nat → Nat) (W addrBase ancBase d ctrl dim : Nat) : Prop

theorem cxGates_wellTyped_local (dim c : Nat) (xs : List Nat)
    (hdim : 0 < dim) (hc : c < dim) (hxs : ∀ t ∈ xs, t < dim ∧ c ≠ t) :
    Gate.WellTyped dim (cx_gates_from_indices c xs)

theorem unaryQROMAtRev_wellTyped (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase dim : Nat) (hdim : 0 < dim) :
    ∀ (d ctrl base : Nat), QROMRevWT pos W addrBase ancBase d ctrl dim →
      Gate.WellTyped dim (unaryQROMAtRev pos W T addrBase ancBase d ctrl base)
  | 0, ctrl, base, H =>

theorem unaryQROMAtRev_agrees (pos : Nat → Nat) (W : Nat) (T : Nat → Nat)
    (addrBase ancBase : Nat) :
    ∀ (d ctrl base : Nat) (f : Nat → Bool),
      (∀ i, i < d → ctrl ≠ ancBase + i) →
      (∀ i, i < d → ctrl ≠ addrBase + i) →
      (∀ i i', i < d → i' < d → addrBase + i ≠ ancBase + i') →
      (∀ j, j < W → ctrl ≠ pos j) →
      (∀ i j, i < d → j < W → addrBase + i ≠ pos j) →
      (∀ i j, i < d → j < W → ancBase + i ≠ pos j) →
      (∀ i, i < d → f (ancBase + i) = false) →
      Gate.applyNat (unaryQROMAtRev pos W T addrBase ancBase d ctrl base) f
        = EGate.applyNat (unaryQROMAt pos W T addrBase ancBase d ctrl base) f

def babbushLookupAddAtRev (w W : Nat) (T : Nat → Nat) (bits addrBase ancBase q_start : Nat) :
    Gate

def laAtRev (w W bits : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start m k : Nat) : Gate

def seqAllG (gs : List Gate) : Gate

theorem applyNat_seqAllG_range_succ (step : Nat → Gate) (n : Nat) (g0 : Nat → Bool) :
    Gate.applyNat (seqAllG ((List.range (n + 1)).map step)) g0
      = Gate.applyNat (step n)
          (Gate.applyNat (seqAllG ((List.range n).map step)) g0)

def multiplyAddAtRev (w W bits : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start m numWin : Nat) :
    Gate

def radd (w bits numWin a i : Nat) : Gate

theorem seqAllG_foldl_wellTyped (dim : Nat) :
    ∀ (gs : List Gate) (seed : Gate),
      Gate.WellTyped dim seed → (∀ g ∈ gs, Gate.WellTyped dim g) →
      Gate.WellTyped dim (gs.foldl Gate.seq seed)
  | [], seed, hseed, _ => hseed
  | g :: rest, seed, hseed, h =>
      seqAllG_foldl_wellTyped dim rest (Gate.seq seed g)
        ⟨hseed, h g (List.mem_cons_self ..)⟩
        (fun x hx => h x (List.mem_cons_of_mem g hx))

theorem seqAllG_wellTyped (dim : Nat) (h0 : 0 < dim) (gs : List Gate)
    (h : ∀ g ∈ gs, Gate.WellTyped dim g) :
    Gate.WellTyped dim (seqAllG gs)

theorem babbushLookupAddAtRev_wellTyped (w W : Nat) (T : Nat → Nat)
    (bits addrBase ancBase q_start dim : Nat) (hdim : 0 < dim)
    (hQ : QROMRevWT (addendIdx q_start) W addrBase ancBase w 0 dim)
    (hacc : q_start + 2 * bits + 1 ≤ dim) :
    Gate.WellTyped dim (babbushLookupAddAtRev w W T bits addrBase ancBase q_start)

def dimRadd (w bits numWin : Nat) : Nat

theorem radd_window_QROMRevWT (w bits numWin : Nat) (hw : 0 < w)
    (k : Nat) (hk : k < numWin) :
    QROMRevWT (addendIdx 1) bits
      (addrBaseOf w bits 1 k) (ancBaseOf w bits 1 k) w 0 (dimRadd w bits numWin)

theorem radd_wellTyped (w bits numWin a i : Nat) (hw : 0 < w) (hbits : 1 ≤ bits) :
    Gate.WellTyped (dimRadd w bits numWin) (radd w bits numWin a i)

theorem babbushLookupAddAtRev_agrees
    (w W bits : Nat) (T : Nat → Nat) (addrBase ancBase q_start : Nat)
    (hW : W ≤ bits) (h_addr_pos : 0 < addrBase) (h_anc_pos : 0 < ancBase)
    (h_anc_addr : ∀ i i', i < w → i' < w → ancBase + i ≠ addrBase + i')
    (h_anc_blk : ∀ i, i < w →
      ¬ (q_start ≤ ancBase + i ∧ ancBase + i ≤ q_start + 2 * bits))
    (h_addr_blk : ∀ i, i < w →
      ¬ (q_start ≤ addrBase + i ∧ addrBase + i ≤ q_start + 2 * bits))
    (f : Nat → Bool) (hf : CleanInputModFree w W bits addrBase ancBase q_start T f) :
    Gate.applyNat (babbushLookupAddAtRev w W T bits addrBase ancBase q_start) f
      = EGate.applyNat (babbushLookupAddAt w W T bits addrBase ancBase q_start) f

theorem multiplyAddAtRev_agrees_fold
    (w bits a numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0) :
    ∀ n, n ≤ numWin →
      Gate.applyNat (seqAllG ((List.range n).map (laAtRev w bits bits Tfam q_start m))) g0
        = EGate.applyNat (seqAll ((List.range n).map (laAt w bits bits Tfam q_start m))) g0

theorem radd_agrees
    (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (i x : Nat) (hx : x < N) :
    Gate.applyNat (radd w bits numWin a i)
        (Gate.applyNat (egG1 w bits i)
          (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x))
      = s2State w bits numWin a i x

def unmulConcrete (w bits numWin a : Nat) : Nat → Gate

theorem unmulConcrete_spec (w bits numWin N a : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits) (hN2 : 2 * N ≤ 2 ^ bits) :
    UnmulSpecRfree w bits numWin N a (unmulConcrete w bits numWin a)

theorem block_matches_residue_direct_unconditional
    (w bits numWin cm N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (i x : Nat) (hx : x < N) :
    EGate.applyNat (egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)
        (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)
      = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) ((a ^ (2 ^ i) * x) % N)

theorem egRfree_matchesResidue_unconditional
    (w bits numWin cm N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hcm : cm ≤ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    ShorComposedFinal.ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3)
      (fun i => egRfree w bits numWin cm N a (unmulConcrete w bits numWin a) i)
      (fun _ x => encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem unmulConcrete_tcount (w bits numWin a i : Nat) :
    Gate.tcount (unmulConcrete w bits numWin a i)
      = Gate.tcount (radd w bits numWin a i)

theorem encodeDataZeroAnc_low_agree
    (w bits : Nat) {ancBig x : Nat}
    (hxbits : x < 2 ^ bits)
    (hpad : 2 * w + 2 * bits + 3 ≤ ancBig) :
    ∀ p, p < bits + (2 * w + 2 * bits + 3) →
      encodeDataZeroAnc bits ancBig x p
        = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x p

theorem windowedModNEncodeGate_roundTrip_pad
    (w bits numWin N c cinv : Nat) {ancBig x : Nat}
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN_pos : 0 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hx : x < N) (hcinv : cinv < N) (hinv : c * cinv % N = 1)
    (hpad : 2 * w + 2 * bits + 3 ≤ ancBig) :
    Gate.applyNat (windowedModNEncodeGate w bits N numWin c cinv)
        (encodeDataZeroAnc bits ancBig x)
      = encodeDataZeroAnc bits ancBig (c * x % N)

noncomputable def paddedRevFamily
    (w bits numWin N : Nat) {ancBig : Nat}
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hpad : 2 * w + 2 * bits + 3 ≤ ancBig) :
    EncodeRoundTripModMul N bits ancBig

noncomputable def paddedRevFamily_verifiedModMulFamily
    (w bits numWin N a ainv0 : Nat) {ancBig : Nat}
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hpad : 2 * w + 2 * bits + 3 ≤ ancBig) :
    VerifiedModMulFamily a N bits ancBig

theorem egate_matches_rev_of_modExpAtResidue_pad
    (w bits numWin N a ainv0 : Nat) {ancBig : Nat}
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hpad : 2 * w + 2 * bits + 3 ≤ ancBig)
    (eg : Nat → EGate)
    (H : FormalRV.Audit.GidneyEkera2021.ShorComposedFinal.ModExpAtEncodedMatchesResidue
          a N bits ancBig eg
          (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits ancBig x)) :
    ∀ i x, x < N →
      Framework.uc_eval

theorem windowedModNEncodeGate_roundTrip_pad_native
    (w bits numWin N c cinv x : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN_pos : 0 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (hx : x < N) (hcinv : cinv < N) (hinv : c * cinv % N = 1) :
    Gate.applyNat (windowedModNEncodeGate w bits N numWin c cinv)
        (encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)
      = encodeDataZeroAnc bits (2 * w + 2 * bits + 3) (c * x % N)

theorem kron_length (A B : BoolMat) :
    (kron A B).length = A.length * B.length

theorem identMat_length (n : Nat) : (identMat n).length = n

theorem repCode_length (d : Nat) : (repCode d).length = d - 1

theorem transpose_length (h : BoolMat) (n : Nat) :
    (transpose h n).length = n

theorem hcat_length (L R : BoolMat) :
    (hcat L R).length = min L.length R.length

theorem surfaceHGP_hx_length (d : Nat) :
    (surfaceHGP d).hx.length = (d - 1) * d

theorem surfaceHGP_hz_length (d : Nat) :
    (surfaceHGP d).hz.length = (d - 1) * d

def syndromeAncillas (d : Nat) : Nat

theorem syndromeAncillas_eq (d : Nat) :
    (surfaceHGP d).hx.length + (surfaceHGP d).hz.length = syndromeAncillas d

def extractionPhysicalQubits (d : Nat) : Nat

private theorem surfaceHGP_rows_le (d : Nat)
    (hws : (surfaceHGP d).well_shaped = true) :
    (∀ row ∈ (surfaceHGP d).hx, row.length ≤ (surfaceHGP d).n)
      ∧ (∀ row ∈ (surfaceHGP d).hz, row.length ≤ (surfaceHGP d).n)

theorem widthC_ge2021_extraction (d : Nat)
    (hws : (surfaceHGP d).well_shaped = true)
    (hnz : (surfaceHGP d).hz ≠ []) :
    widthC (Round.ops (CSSCode.extractionRound (surfaceHGP d)))
      = extractionPhysicalQubits d

def ge2021Distance : Nat

abbrev ge2021DataCode : CSSCode

theorem ge2021_data_qubits : ge2021DataCode.n = 1405

theorem ge2021_x_syndrome : ge2021DataCode.hx.length = 702

theorem ge2021_z_syndrome : ge2021DataCode.hz.length = 702

theorem ge2021_syndrome_ancillas : syndromeAncillas ge2021Distance = 1404

theorem ge2021_extraction_physical : extractionPhysicalQubits ge2021Distance = 2809

def paperPatchFootprint (d : Nat) : Nat

theorem paper_patch_1568 : paperPatchFootprint ge2021Distance = 1568

theorem rotated_patch_accounting :
    27 * 27 = 729                          -- rotated data qubits
      ∧ 27 * 27 - 1 = 728                   -- rotated measure (syndrome) qubits
      ∧ 27 * 27 + (27 * 27 - 1) = 1457      -- rotated data + measure
      ∧ paperPatchFootprint 27 = 1568       -- + spacing (the paper's figure)
      ∧ 1568 - 1457 = 111

theorem ge2021_footprint_exact :
    (FormalRV.QEC.Codes.Surface.rotatedSurface 27).valid = true   -- verified rotated patch
      ∧ FormalRV.QEC.Codes.Surface.rotatedPhysicalQubits 27 = 1457  -- data + syndrome
      ∧ paperPatchFootprint ge2021Distance = 1568                  -- paper (+ spacing)
      ∧ 1568 - 1457 = 111

theorem ge2021_extraction_measures_code
    (hws : ge2021DataCode.well_shaped = true) :
    Round.measuredDataObs
        (ge2021DataCode.n + ge2021DataCode.hx.length + ge2021DataCode.hz.length)
        ge2021DataCode.n (Surface.extractionRound ge2021Distance)
      = ge2021DataCode.toStabilizers

theorem babbushLookupAddAt_valueSpec_discharged
    (w W bits : Nat) (T : Nat → Nat) (addrBase ancBase q_start : Nat)
    (hW : W ≤ bits) (h_anc_pos : 0 < ancBase)
    (h_anc_addr : ∀ i i', i < w → i' < w → ancBase + i ≠ addrBase + i')
    (h_anc_blk : ∀ i, i < w →
      ¬ (q_start ≤ ancBase + i ∧ ancBase + i ≤ q_start + 2 * bits))
    (h_addr_blk : ∀ i, i < w →
      ¬ (q_start ≤ addrBase + i ∧ addrBase + i ≤ q_start + 2 * bits))
    (f : Nat → Bool)
    (hf : CleanLookupAddAtInput w W bits addrBase ancBase q_start T f) :
    decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (babbushLookupAddAt w W T bits addrBase ancBase q_start) f)

structure CountGateMulInput (w bits numWin y q_start : Nat) (g0 : Nat → Bool) : Prop

theorem countOptimal_multiplyAdd_value
    (w bits a numWin y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0) :
    decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0)
      = (a * y) % 2 ^ bits

theorem countOptimal_multiplyAdd_coset
    (w bits a numWin N y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0)
    (hnowrap : a * y < 2 ^ bits) :
    IsCosetRep bits N
      (decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0))
      (a * y)

theorem countOptimal_multiplyAdd_readout
    (w bits a numWin N y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0)
    (hnowrap : a * y < 2 ^ bits) :
    cosetValue N
      (decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0))
      = (a * y) % N

theorem countGateMulInput_nonempty
    (w bits numWin q_start : Nat) (hq : 0 < q_start) :
    CountGateMulInput w bits numWin 0 q_start (fun p => decide (p = 0))

theorem multiplyAddAt_is_inner_block_of_modExpAt
    (w W bits : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start j numWin : Nat) :
    multiplicationAt w W bits Tfam q_start j numWin
      = EGate.seq (multiplyAddAt w W bits Tfam q_start (2 * j) numWin)
                  (multiplyAddAt w W bits Tfam q_start (2 * j + 1) numWin)

theorem countOptimal_value_and_count_rsa2048
    (a N y m q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hq : 0 < q_start)
    (hT : ∀ k v, Tfam m k v = (a * (2 ^ 10) ^ k * v) % 2 ^ 2048)
    (hy : y < (2 ^ 10) ^ 1024)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput 10 2048 1024 y q_start g0)
    (hnowrap : a * y < 2 ^ 2048) :
    EGate.toffoli (modExpAt 10 2048 2048 Tfam q_start
        (numMultsOf 3072 5 5) (numWinOf 2048 5 1024)) = 2578993152
    ∧ IsCosetRep 2048 N
        (decodeReg (fun i => q_start + 2 * i + 1) 2048
          (EGate.applyNat (multiplyAddAt 10 2048 2048 Tfam q_start m 1024) g0))

structure CountGateShorBridge
    (w bits a numWin N anc q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)

theorem countGateShorBridge_coset_value_discharged
    (w bits a numWin N q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start) :
    ∀ (m y : Nat) (g0 : Nat → Bool),
      CountGateMulInput w bits numWin y q_start g0 →
      (∀ k v, Tfam m k v = (a * (2 ^ w) ^ k * v) % 2 ^ bits) →
      y < (2 ^ w) ^ numWin → a * y < 2 ^ bits →
      IsCosetRep bits N
        (decodeReg (fun i => q_start + 2 * i + 1) bits
          (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start m numWin) g0))
        (a * y)

theorem countOptimal_shor_succeeds
    {w bits a numWin N anc q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (B : CountGateShorBridge w bits a numWin N anc q_start Tfam)
    (r m : Nat) (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits anc B.eGate_to_family.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

def countGateShorBridge_of_measuredEqRev
    {w bits a numWin N anc q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    {eg : Nat → EGate} {encode : Nat → Nat → (Nat → Bool)}
    (hw : 0 < w) (hq : 0 < q_start)
    (Wit : MeasuredEqualsReversibleOnEncoded a N bits anc eg encode) :
    CountGateShorBridge w bits a numWin N anc q_start Tfam

theorem countOptimal_shor_succeeds_constrained
    {w bits a numWin N anc q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    {eg : Nat → EGate} {encode : Nat → Nat → (Nat → Bool)}
    (hw : 0 < w) (hq : 0 < q_start)
    (Wit : MeasuredEqualsReversibleOnEncoded a N bits anc eg encode)
    (r m : Nat) (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits anc Wit.rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

def measuredEqRev_of_encodeRoundTrip
    {N bits anc : Nat} (W : EncodeRoundTripModMul N bits anc)
    (a : Nat) (hN : N ≤ 2 ^ bits) (ainv0 : Nat) (hN1 : 1 < N)
    (h_inv0 : a * ainv0 % N = 1) :
    MeasuredEqualsReversibleOnEncoded a N bits anc
      (fun i => EGate.base (W.gate (a ^ (2 ^ i))))
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits anc x)

def ge2021_measuredEqRev
    (w bits numWin N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1) :
    MeasuredEqualsReversibleOnEncoded a N bits (2 * w + 2 * bits + 3)
      (fun i => EGate.base
        ((windowedModNMultiplier w bits numWin N hw hbits hb1 hN1 hN2).gate (a ^ (2 ^ i))))
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem ge2021_exactMultiplier_shor_bound
    (w bits numWin N a ainv0 r m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_measuredEqRev w bits numWin N a ainv0 hw hbits hb1 hN1 hN2 h_inv0).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem ge2021_count_on_modExpAt_AND_bound_on_DIFFERENT_exact_multiplier
    (W : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start : Nat)
    (numWin N a ainv0 r m : Nat)
    (hbits : numWin * 10 = 2048)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ 2048)
    (h_inv0 : a * ainv0 % N = 1)
    (h_setting : ShorSetting a r N m 2048) :
    EGate.toffoli (modExpAt 10 W 2048 Tfam q_start
        (numMultsOf 3072 5 5) (numWinOf 2048 5 1024)) = 2578993152
    ∧ probability_of_success a r N m 2048 (2 * 10 + 2 * 2048 + 3)
        (ge2021_measuredEqRev 10 2048 numWin N a ainv0
          (by norm_num) hbits (by norm_num) hN1 hN2 h_inv0).rev.family

structure ModExpAtEncodedMatchesResidue
    (a N bits anc : Nat) (eg : Nat → EGate)
    (encode : Nat → Nat → (Nat → Bool)) : Prop

theorem egate_matches_rev_of_modExpAtResidue
    (w bits numWin N a ainv0 : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (eg : Nat → EGate)
    (H : ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3) eg
          (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)) :
    ∀ i x, x < N →
      Framework.uc_eval
          ((windowedModNMultiplier_verifiedModMulFamily w bits numWin N a ainv0
              hw hbits hb1 hN1 hN2 h_inv0).family i)

theorem multiplyAddAt_block_residue_value
    (w bits c numWin N y mblk q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam mblk k v = (c * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0)
    (hnowrap : c * y < 2 ^ bits) :
    cosetValue N
      (decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start mblk numWin) g0))
      = (c * y) % N

theorem multiplyAddAt_block_isCosetRep
    (w bits c numWin N y mblk q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)
    (hw : 0 < w) (hq : 0 < q_start)
    (hT : ∀ k v, Tfam mblk k v = (c * (2 ^ w) ^ k * v) % 2 ^ bits)
    (hy : y < (2 ^ w) ^ numWin)
    (g0 : Nat → Bool) (hg0 : CountGateMulInput w bits numWin y q_start g0)
    (hnowrap : c * y < 2 ^ bits) :
    IsCosetRep bits N
      (decodeReg (fun i => q_start + 2 * i + 1) bits
        (EGate.applyNat (multiplyAddAt w bits bits Tfam q_start mblk numWin) g0))
      (c * y)

structure ModExpAtLayoutAdapter
    (w bits anc numWin N a q_start : Nat) (Tfam : Nat → Nat → Nat → Nat)

def ModExpAtLayoutAdapter.conjugatedBlock
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits anc numWin N a q_start Tfam) (i : Nat) : EGate

theorem ModExpAtLayoutAdapter.conjugatedBlock_toffoli
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits anc numWin N a q_start Tfam) (i : Nat) :
    EGate.toffoli (L.conjugatedBlock i)
      = EGate.toffoli (multiplyAddAt w bits bits Tfam q_start (L.mblkOf i) numWin)

theorem modExpAtBlock_matches_residue
    {w bits anc numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits anc numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (i x : Nat) (hx : x < N) :
    EGate.applyNat (L.conjugatedBlock i)
        (FormalRV.BQAlgo.encodeDataZeroAnc bits anc x)
      = FormalRV.BQAlgo.encodeDataZeroAnc bits anc (((a ^ (2 ^ i)) * x) % N)

def modExpAtEncodedMatchesResidue_of_layoutAdapter
    {w bits numWin N a q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hN2 : 2 * N ≤ 2 ^ bits)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits) :
    ModExpAtEncodedMatchesResidue a N bits (2 * w + 2 * bits + 3)
      (fun i => L.conjugatedBlock i)
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

def ge2021_modExpAt_measuredEqRev
    {w bits numWin N a ainv0 q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits) :
    MeasuredEqualsReversibleOnEncoded a N bits (2 * w + 2 * bits + 3)
      (fun i => L.conjugatedBlock i)
      (fun _ x => FormalRV.BQAlgo.encodeDataZeroAnc bits (2 * w + 2 * bits + 3) x)

theorem ge2021_modExpAt_shor_succeeds
    {w bits numWin N a ainv0 r m q_start : Nat} {Tfam : Nat → Nat → Nat → Nat}
    (L : ModExpAtLayoutAdapter w bits (2 * w + 2 * bits + 3) numWin N a q_start Tfam)
    (hw : 0 < w) (hq : 0 < q_start)
    (hbits : numWin * w = bits) (hb1 : 1 ≤ bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ bits)
    (h_setting : ShorSetting a r N m bits) :
    probability_of_success a r N m bits (2 * w + 2 * bits + 3)
        (ge2021_modExpAt_measuredEqRev L hw hq hbits hb1 hN1 hN2 h_inv0 hnowrap).rev.family
      ≥ κ / (Nat.log2 N : ℝ) ^ 4

theorem ge2021_modExpAt_count_AND_bound_SAME_gate
    (W : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start : Nat)
    {numWin N a ainv0 r m : Nat}
    (L : ModExpAtLayoutAdapter 10 2048 (2 * 10 + 2 * 2048 + 3) numWin N a q_start Tfam)
    (hq : 0 < q_start)
    (hbits : numWin * 10 = 2048)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ 2048)
    (h_inv0 : a * ainv0 % N = 1)
    (hnowrap : ∀ i x, x < N → (a ^ (2 ^ i)) * x < 2 ^ 2048)
    (h_setting : ShorSetting a r N m 2048) :
    EGate.toffoli (modExpAt 10 W 2048 Tfam q_start
        (numMultsOf 3072 5 5) (numWinOf 2048 5 1024)) = 2578993152

abbrev ge2021_distance        : Nat

abbrev ge2021_tile_qubits     : Nat

abbrev ge2021_logical_qubits  : Nat

abbrev ge2021_cycle_us        : Nat

abbrev 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

theorem catalog_ge2021_arch_eq :
    FormalRV.System.HardwareCatalog.ge2021_physical.toZonedArch = ge2021Arch

def ge2021_overflow_sched : List SysCall

def ge2021_overflow_ctx : SystemCtx

theorem ge2021_overflow_rejected :
    checkAll baseInvariants ge2021_overflow_ctx = false

def decoderBacklogInv (patches decodeLatency lanes : Nat) : SpaceTimeInvariant

def ge2021DecoderInv (lanes : Nat) : SpaceTimeInvariant

def ge2021_probe_ctx : SystemCtx

theorem ge2021_probe_resource_ok :
    checkAll baseInvariants ge2021_probe_ctx = true

theorem ge2021_fully_valid_with_decoder :
    checkAll (baseInvariants ++ [ge2021DecoderInv 62_000]) ge2021_probe_ctx = true

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

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

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

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 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
    ∧ windowedPhysicalDataQubits_rsa2048 = 9633792

def transcodeBand (src dst : Nat → Nat) (len : Nat) : Gate

theorem transcodeBand_tcount (src dst : Nat → Nat) (len : Nat) :
    (transcodeBand src dst len).tcount = 0

theorem transcodeBand_wellTyped (src dst : Nat → Nat) (len D : Nat)
    (hD : 0 < D)
    (hfit : ∀ k, k < len → src k < D ∧ dst k < D)
    (hne : ∀ k, k < len → src k ≠ dst k) :
    Gate.WellTyped D (transcodeBand src dst len)

theorem transcodeBand_apply (src dst : Nat → Nat) (len : Nat) (f : Nat → Bool)
    (hsrc_inj : ∀ i k, i < len → k < len → i ≠ k → src i ≠ src k)
    (hdst_inj : ∀ i k, i < len → k < len → i ≠ k → dst i ≠ dst k)
    (hdisj : ∀ i k, i < len → k < len → src i ≠ dst k)
    (hdst_false : ∀ k, k < len → f (dst k) = false) :
    (∀ k, k < len → Gate.applyNat (transcodeBand src dst len) f (dst k) = f (src k))
    ∧ (∀ k, k < len → Gate.applyNat (transcodeBand src dst len) f (src k) = false)
    ∧ (∀ p, (∀ k, k < len → p ≠ src k ∧ p ≠ dst k) →
        Gate.applyNat (transcodeBand src dst len) f p = f p)

def transcodeAccToData (w bits q_start : Nat) : Gate

theorem transcodeAccToData_tcount (w bits q_start : Nat) :
    (transcodeAccToData w bits q_start).tcount = 0

theorem transcodeAccToData_wellTyped (w bits q_start D : Nat)
    (hbits : 0 < bits) (hq : bits ≤ q_start)
    (hD : q_start + 2 * bits < D) :
    Gate.WellTyped D (transcodeAccToData w bits q_start)

theorem transcodeAccToData_apply (w bits q_start anc : Nat) (f : Nat → Bool)
    (v : Nat) (_hbits : 0 < bits) (hq : bits ≤ q_start)
    (hv : decodeReg (fun j => q_start + 2 * j + 1) bits f = v)
    (hvlt : v < 2 ^ bits)
    (hdata0 : ∀ i, i < bits → f i = false) :
    (∀ i, i < bits →
        Gate.applyNat (transcodeAccToData w bits q_start) f i
          = encodeDataZeroAnc bits anc v i)
    ∧ (∀ j, j < bits →
        Gate.applyNat (transcodeAccToData w bits q_start) f (q_start + 2 * j + 1)
          = false)
    ∧ (∀ p, (∀ j, j < bits → p ≠ q_start + 2 * j + 1 ∧ p ≠ bits - 1 - j) →

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)

theorem audit_toffoli_literal_eq_cost_model :
    (toffoliCount : ℚ) = Shor.WindowedCostModel.toffoliCount 2048 3072 11

theorem audit_magic_budget_eq :
    System.MagicScheduleComplete.rsa2048_magic_budget = toffoliCount
    ∧ (System.MagicScheduleComplete.rsa2048_magic_budget : ℚ)
        = Shor.WindowedCostModel.toffoliCount 2048 3072 11

theorem audit_data_qubit_literal_eq_derived :
    System.MagicScheduleComplete.rsa2048_data_qubits = windowedPhysicalDataQubits_rsa2048

theorem audit_toffoli_realized_by_circuit
    (W : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start : Nat) :
    EGate.toffoli (Shor.WindowedComposedAt.modExpAt 10 W 2048 Tfam q_start
        (Shor.WindowedComposedAt.numMultsOf 3072 5 5)
        (Shor.WindowedComposedAt.numWinOf 2048 5 1024)) = 2578993152
    ∧ (EGate.toffoli (Shor.WindowedComposedAt.modExpAt 10 W 2048 Tfam q_start
        (Shor.WindowedComposedAt.numMultsOf 3072 5 5)
        (Shor.WindowedComposedAt.numWinOf 2048 5 1024)) : ℚ)
        = Shor.WindowedComposedCost.structToffoliCount 2048 3072
    ∧ toffoliCount - EGate.toffoli (Shor.WindowedComposedAt.modExpAt 10 W 2048 Tfam q_start
        (Shor.WindowedComposedAt.numMultsOf 3072 5 5)
        (Shor.WindowedComposedAt.numWinOf 2048 5 1024)) = 43831296

theorem audit_n_toff_upper_bounds_circuit
    (W : Nat) (Tfam : Nat → Nat → Nat → Nat) (q_start : Nat) :
    EGate.toffoli (Shor.WindowedComposedAt.modExpAt 10 W 2048 Tfam q_start
        (Shor.WindowedComposedAt.numMultsOf 3072 5 5)
        (Shor.WindowedComposedAt.numWinOf 2048 5 1024))
      ≤ (System.NaiveUpperBound.ge2021_work).n_toff
    ∧ toffoliCount ≤ (System.NaiveUpperBound.ge2021_work).n_toff
    ∧ Shor.WindowedCostModel.toffoliCount 2048 3072 11
        ≤ ((System.NaiveUpperBound.ge2021_work).n_toff : ℚ)

theorem audit_per_lookup_add (W : Nat) (T : Nat → Nat) (addrBase ancBase q_start : Nat) :
    EGate.toffoli
        (Shor.MeasUncomputeAt.babbushLookupAddAt 10 W T (2048 + 43) addrBase ancBase q_start)
      = 5205
    ∧ Shor.WindowedCostModel.perLookupToffoli 2048 11 = 5206
    ∧ ((5205 : Nat) : ℚ) + 1 = Shor.WindowedCostModel.perLookupToffoli 2048 11
    ∧ Shor.WindowedCostModel.perLookupToffoli 2048 11
        - Shor.WindowedComposedCost.structPerLookup 2048 = 87

theorem audit_value_semantics_witness
    (T : Nat → Nat) (addrBase ancBase q_start : Nat)
    (h_anc_pos : 0 < ancBase)
    (h_anc_addr : ∀ i i', i < 10 → i' < 10 → ancBase + i ≠ addrBase + i')
    (h_anc_blk : ∀ i, i < 10 →
      ¬ (q_start ≤ ancBase + i ∧ ancBase + i ≤ q_start + 2 * 2048))
    (h_addr_blk : ∀ i, i < 10 →
      ¬ (q_start ≤ addrBase + i ∧ addrBase + i ≤ q_start + 2 * 2048))
    (f : Nat → Bool)
    (hf : Shor.WindowedComposedAt.CleanInputModFree 10 2048 2048
            addrBase ancBase q_start T f) :
    decodeReg (fun i => q_start + 2 * i + 1) 2048

theorem audit_qubit_count_realized_by_circuit (wE g e : Nat) (ainvs : Nat → Nat) :
    ge2021_logical_qubits = 6200
    ∧ Shor.WindowedWidthAudit.paperWidthFigure 2048 11 = 6189
    ∧ ge2021_logical_qubits = Shor.WindowedWidthAudit.paperWidthFigure 2048 11 + 11
    ∧ Shor.WindowedCircuit.width
        (Shor.WindowedCircuit.windowedExpInPlace BQAlgo.cuccaroAdder 8 2048 256 wE 3072 g e ainvs)
        = 6162
    ∧ Shor.WindowedCircuit.width
        (Shor.WindowedCircuit.windowedExpInPlace BQAlgo.cuccaroAdder 8 2048 256 wE 3072 g e ainvs)
        + 27 = Shor.WindowedWidthAudit.paperWidthFigure 2048 11

theorem audit_modexp_value_witness
    (w bits numWin N wE nE a ainv e : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits)
    (hN1 : 1 < N) (hN2 : 2 * N ≤ 2 ^ bits)
    (he : e < (2 ^ wE) ^ nE) (hinv : a * ainv % N = 1) :
    decodeReg (fun i => 1 + 2 * w + (2 * bits + 1) + i) bits
        (BQAlgo.Gate.applyNat
          (Shor.WindowedModExpValue.windowedModNExpInPlace w bits numWin N wE nE a ainv e)
          (Shor.WindowedCircuit.mulInputOf BQAlgo.cuccaroAdder w bits numWin 1))
      = a ^ e % N

theorem audit_optimal_count_is_modN_correct
    (A : BQAlgo.Adder) (w bits a numWin N y : Nat)
    (hw : 0 < w) (hy : y < 2 ^ (w * numWin))
    (hclean : A.ancClean (Shor.WindowedCircuit.mulInputOf A w bits numWin y) bits (1 + 2 * w))
    (hnowrap : a * y < 2 ^ bits) :
    Shor.WindowedCoset.IsCosetRep bits N
      (Shor.WindowedCircuit.decodeAccOf A
        (BQAlgo.Gate.applyNat (Shor.WindowedCircuit.windowedMulCircuitOf A w bits a numWin)
          (Shor.WindowedCircuit.mulInputOf A w bits numWin y)) (1 + 2 * w) bits)
      (a * y)
    ∧ Shor.WindowedCoset.cosetValue N
        (Shor.WindowedCircuit.decodeAccOf A

theorem audit_coset_deviation_reduced (gpad numAdds adv : Nat) (n n_e : ℚ)
    (hn : n ≠ 0) (hne : n_e ≠ 0) :
    Arithmetic.Windowed.WindowedCosetDeviation.wrapProbCount gpad numAdds adv
        ≤ Arithmetic.Windowed.WindowedCosetDeviation.countingBoundQ
            (numAdds : ℚ) (adv : ℚ) ((2 : ℚ) ^ gpad)
    ∧ Arithmetic.Windowed.WindowedCosetDeviation.countingBoundQ
        (Shor.WindowedCostModel.lookupAdditionCount n n_e) (n / 1024) (n ^ 2 * n_e * 1024)
        = Shor.WindowedCostModel.totalDeviation n n_e

example : Arithmetic.Windowed.WindowedCosetDeviation.cosetDeviationBound_rsa2048.wrapProb
    ≤ 1 / 10000000

def peng_hw : QualtranPhysicalParameters

def peng_shor : ShorAlgorithm

def peng_code : QECCode

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

theorem pinnacle_modexp_endToEnd
    (P : Nat → Nat) (ainvss : Nat → Nat → Nat) (numP w bits numWin g N e m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits)
    (hPok : ∀ j, j < numP → 1 < P j ∧ 2 * P j ≤ 2 ^ bits ∧
      ∀ k, k < m → ainvss j k < P j ∧ residueConst g N (P j) e k * ainvss j k % (P j) = 1)
    (hN : 2 ≤ N) (hm : 1 ≤ m) (he : e < 2 ^ m)
    (hco : ∀ i j : Fin numP, i ≠ j → Nat.Coprime (P i.val) (P j.val))
    (hL : N ^ m ≤ ∏ i : Fin numP, P i.val)
    (S : EkeraDLPSuccess)
    (p q d : Nat) (hd : d = p + q - 2) (hNpq : N = p * q) (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hphi : g ^ ((p - 1) * (q - 1)) ≡ 1 [MOD p * q])
    (s : Nat → Nat) (chunk ρ : Nat) :

theorem pinnacle_eh_rns_shor_succeeds
    -- (EH measurement) register/parameter sizes + the short discrete log `ehD`
    (ehL ehM ehD : ℕ) (hℓ : 1 ≤ ehL) (hm : 2 ≤ ehM) (hd0 : 0 < ehD) (hdlt : ehD < 2 ^ ehM)
    -- (RNS arithmetic) the residue circuit computing the one-shot modexp `g^e mod N`
    (P : Nat → Nat) (ainvss : Nat → Nat → Nat) (numP w bits numWin g N e steps : ℕ)
    (hw : 0 < w) (hbits : numWin * w = bits)
    (hPok : ∀ j, j < numP → 1 < P j ∧ 2 * P j ≤ 2 ^ bits ∧
      ∀ k, k < steps → ainvss j k < P j ∧ residueConst g N (P j) e k * ainvss j k % (P j) = 1)
    (hN : 2 ≤ N) (hsteps : 1 ≤ steps) (he : e < 2 ^ steps)
    (hco : ∀ i j : Fin numP, i ≠ j → Nat.Coprime (P i.val) (P j.val))
    (hLprod : N ^ steps ≤ ∏ i : Fin numP, P i.val)
    -- (factoring) Ekerå–Håstad factorisation data: `ehD = p+q-2`, `N = p·q`

def pinnacle_hw : QualtranPhysicalParameters

def pinnacle_shor : ShorAlgorithm

theorem pinnacle_dlog_recovery_succeeds (S : EkeraDLPSuccess) :
    ekeraGoodFactor S.τ * ekeraBalancedFactor S.Δ S.t S.τ ≤ S.successProb

theorem pinnacle_addition_toffoli (n q_start : Nat) :
    EGate.toffoli (gidneyAdderMeasured (n + 2) q_start)
      = FormalRV.Audit.Gidney2025.g2025_add_toffoli (n + 2) + 1

theorem pinnacle_lookup_toffoli
    (pos : Nat → Nat) (W : Nat) (T : Nat → Nat) (addrBase ancBase d ctrl base : Nat) :
    EGate.toffoli (unaryQROMAt pos W T addrBase ancBase d ctrl base)
      = FormalRV.Audit.Gidney2025.g2025_lookup_toffoli d + d

def gbXbar (i : Nat) : PauliString

def gbZbar (i : Nat) : PauliString

def gbCodeState : StabilizerState

theorem gb_numLogicals : numLogicals pinnacle_gb_72 = 12

theorem gbCodeState_valid : StabilizerState.valid gbCodeState pinnacle_gb_72.n = true

theorem gb_single_ppm_records_observable :
    gbZbar 0 ∈ apply_PPM_pos gbCodeState (gbZbar 0)

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

def gbCodeStabs : List PauliString

theorem gbCodeStabs_sub_state (g : PauliString) (hg : g ∈ gbCodeStabs) : g ∈ gbCodeState

theorem gbCodeStabs_commute_logZ :
    ∀ g ∈ gbCodeStabs, ∀ i ∈ List.range 12, g.commutes (gbZbar i) = true

theorem gb_logical_computation_preserves_code
    (ps : List PauliString)
    (hlog : ∀ P ∈ ps, ∀ g ∈ gbCodeStabs, g.commutes P = true)
    (g : PauliString) (hg : g ∈ gbCodeStabs) :
    g ∈ runGBPPMs ps gbCodeState

theorem gb_modexp_preserves_code
    (ps : List PauliString)
    (halpha : ∀ P ∈ ps, ∃ i ∈ List.range 12, P = gbZbar i)
    (g : PauliString) (hg : g ∈ gbCodeStabs) :
    g ∈ runGBPPMs ps gbCodeState

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

def pinnacle_code : QECCode

def pinnacle_n_pb : Nat

def pinnacle_instance : ShorAlgorithm × QECCode × QualtranPhysicalParameters

theorem pinnacle_rsa_code_recorded :
    pinnacle_code.n = 510 ∧
    pinnacle_code.k = 16 ∧
    pinnacle_code.d = 24 ∧
    pinnacle_n_pb = 1620

example : pinnacle_instance.1.q_A = 3072

example : pinnacle_instance.2.1.n = 510 ∧
          pinnacle_instance.2.1.k = 16 ∧
          pinnacle_instance.2.1.d = 24

example : pinnacle_instance.2.2.physical_error_thousandths = 1

theorem pinnacle_modexp_ppm_realized
    (F : TFactoryContract)
    (P : Nat → Nat) (ainvss : Nat → Nat → Nat) (numP w bits numWin g N e m : Nat)
    (hw : 0 < w) (hbits : numWin * w = bits)
    (hPok : ∀ j, j < numP → 1 < P j ∧ 2 * P j ≤ 2 ^ bits ∧
      ∀ k, k < m → ainvss j k < P j ∧ residueConst g N (P j) e k * ainvss j k % (P j) = 1)
    (hN : 2 ≤ N) (hm : 1 ≤ m) (he : e < 2 ^ m)
    (hco : ∀ i j : Fin numP, i ≠ j → Nat.Coprime (P i.val) (P j.val))
    (hL : N ^ m ≤ ∏ i : Fin numP, P i.val) :
    (∃ σ' output,
      MagicPPMProgramRel F
        (compileArithmeticGateToMagicPPM (residueFold P ainvss numP w bits numWin g N e m))

theorem exactAcc_add (s : ℕ → ℕ) (a c : ℕ) :
    exactAcc s (a + c) = exactAcc s a + exactAcc (fun k => s (a + k)) c

def chunkAcc (s : ℕ → ℕ) (c j : ℕ) : ℕ

def parAcc (s : ℕ → ℕ) (c : ℕ) : ℕ → ℕ
  | 0 => 0
  | ρ + 1 => parAcc s c ρ + chunkAcc s c ρ

theorem parallelReduction_eq_serial (s : ℕ → ℕ) (c ρ : ℕ) :
    parAcc s c ρ = exactAcc s (ρ * c)

theorem parallelReduction_modDev (N : ℕ) (hN : 0 < N) (s : ℕ → ℕ) (t f c ρ : ℕ)
    (htf : 2 ^ (t + f) ≤ N) :
    (modDev N (parAcc s c ρ) (apprAcc s t (ρ * c)) : ℚ) / N
      ≤ (ρ * c : ℕ) / 2 ^ f

theorem modDev_add_add (N a a' b b' : ℕ) (hN : 0 < N) :
    modDev N (a + a') (b + b') ≤ modDev N a b + modDev N a' b'

def chunkApprAcc (s : ℕ → ℕ) (t c j : ℕ) : ℕ

def parApprAcc (s : ℕ → ℕ) (t c : ℕ) : ℕ → ℕ
  | 0 => 0
  | ρ + 1 => parApprAcc s t c ρ + chunkApprAcc s t c ρ

theorem truncShift_add_multiple (x t M : ℕ) :
    truncShift (2 ^ t * M + x) t = 2 ^ t * M + truncShift x t

theorem apprAcc_dvd (s : ℕ → ℕ) (t A : ℕ) : 2 ^ t ∣ apprAcc s t A

theorem apprAcc_add (s : ℕ → ℕ) (t A c : ℕ) :
    apprAcc s t (A + c) = apprAcc s t A + apprAcc (fun k => s (A + k)) t c

theorem parApprAcc_eq_serial (s : ℕ → ℕ) (t c ρ : ℕ) :
    parApprAcc s t c ρ = apprAcc s t (ρ * c)

theorem parallelSchedule_apprAcc_deviation (N : ℕ) (hN : 0 < N) (s : ℕ → ℕ) (t c : ℕ) :
    ∀ ρ, modDev N (exactAcc s (ρ * c)) (parApprAcc s t c ρ) ≤ (ρ * c) * 2 ^ t

theorem parallelSchedule_apprAcc_modDev (N : ℕ) (hN : 0 < N) (s : ℕ → ℕ) (t f c ρ : ℕ)
    (htf : 2 ^ (t + f) ≤ N) :
    (modDev N (exactAcc s (ρ * c)) (parApprAcc s t c ρ) : ℚ) / N ≤ (ρ * c : ℕ) / 2 ^ f

theorem lookupL1_consistency (inst base w1 : Nat) :
    2 * (inst * (6 * base + 2 * w1)) = 3 * (4 * inst * base) + 4 * w1 * inst

theorem addL1_consistency (inst A : Nat) :
    2 * (6 * inst * A) = 3 * (4 * inst * A)

theorem addL2_consistency (len S : Nat) :
    2 * (12 * len * S) = 3 * (8 * len * S)

theorem lookupL3_consistency (inst L3 : Nat) :
    2 * (6 * inst * L3) = 3 * (4 * inst * L3)

theorem addL3_consistency (Q e1 : Nat) :
    2 * (42 * Q * e1) = 3 * (28 * Q * e1)

theorem lookupL4_consistency (c4 L4 : Nat) :
    2 * (9 * c4 * L4) = 3 * (6 * c4 * L4)

theorem addL4_consistency (f1 c4 : Nat) :
    2 * (15 * f1 * c4) = 3 * (10 * f1 * c4)

theorem phaseupL4_consistency (c4 P : Nat) :
    2 * (6 * c4 * P) = 3 * (4 * c4 * P)

theorem phaseupL32_consistency (Q P3 : Nat) :
    2 * (9 * Q * P3) = 3 * (6 * Q * P3)

theorem phaseupL31_consistency (P31 : Nat) :
    2 * (6 * P31) = 3 * (4 * P31)

theorem addL3_T_eq_4_toffoli (Q e1 : Nat) : 28 * Q * e1 = 4 * (7 * Q * e1)

theorem upsilon_assembly (inst1 Lbase A w1 : Nat) :
    inst1 * ((6 * Lbase + 2 * w1) + 6 * A) = inst1 * (6 * (Lbase + A) + 2 * w1)

theorem lambda_serial_is_zero (f : Nat) :
    27 * f * 0 - 4 * f * 0 = 0

theorem tau_consistency (totalT totalLC : Nat) (h : 2 * totalLC = 3 * totalT) :
    3 * totalT = 2 * totalLC

theorem pinnacle_kappa_components (f ell lenm mx : Nat) :
    f + (ell + lenm) + 2 * mx + ell + 1 = f + 2 * ell + lenm + 2 * mx + 1

theorem pinnacle_magic_reject_tension : 15 * 3 + 4 = 49 ∧ (15 * 3 + 4 : Nat) ≠ 19

theorem pinnacle_FH_eq_constant_overcount : 1807 - 592 = 1215

theorem pinnacle_phaseup_general_vs_specialized :
    (4 * (2 ^ 2 - 1) + 2 * (2 ^ 2 - 1) = 18)     -- our verified GENERAL √-phaseup at w=4 (w1=w2=2)
    ∧ (2 ^ 2 + 2 ^ 2 - 4 - 2 = 2)

def xu2024_hw : QualtranPhysicalParameters

example : xu2024_hw.cycle_time_us_tenths = 24000 * gidney_fowler_realistic.cycle_time_us_tenths

def xu2024_shor : ShorAlgorithm

def xu2024_code : QECCode

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 : FormalRV.Audit.Xu2024.xu2024_hw.cycle_time_us_tenths = 24000 * 10