Framework 270 declarations in 10 modules

FormalRV.Framework.Contracts

FormalRV/Framework/Contracts.lean

FormalRV.Framework.Contracts — inter-layer contract theorems. Phase A.5 of the paper plan (`PAPER_PLAN.md`). The four-layer software stack is glued together by three contracts (paper §2): L4 → L3 : cycle_logical_error_rate ≤ f_code (p_g) d L3 → L2 : per_op_error ≤ c · cycle_logical_error_rate L2 → L1 : gadget-by-gadget semantic correctness + T-count This tick states ONLY the first contract as a sorry-stubbed theorem and defines its left-hand-side stub. The remaining two contracts are future ticks. The proof body is `sorry` because the actual error-rate model (surface-code analytic ansatz vs. qLDPC numerical fit) will be supplied per-code by Phase-C corpus files; the contract statement freezes the L4→L3 interface so every L4 code instance in `Phase B/C` ships with a proof obligation of this exact shape. Hardware-parameters bundle lives in `HardwareParams.lean` (separate tick); this file imports it.

structureHardwareParamsStub

structure HardwareParamsStub

Placeholder hardware-parameter bundle used by the L4→L3 contract until `HardwareParams.lean` lands in a later tick.

defcycle_logical_error_rate

def cycle_logical_error_rate (qec : QECCode) (hw : HardwareParamsStub) : Nat

The cycle-level logical-error rate of a QEC code on given hardware. Placeholder: returns `hw.p_g_thousandths` directly (a trivial upper bound, true for `d = 1`). A later tick refines per-code using the analytic surface-code ansatz or qLDPC numerical fit.

theoremL4_to_L3_contract

theorem L4_to_L3_contract (qec : QECCode) (hw : HardwareParamsStub) :
    cycle_logical_error_rate qec hw ≤ f_code hw.p_g_thousandths qec.d

L4 → L3 contract: the per-cycle logical error rate of any QEC code on any hardware is bounded by the code's subthreshold ansatz `f_code` evaluated at the hardware's physical gate-error rate and the code's distance. Trivially holds for the current stub definitions (both sides reduce to `hw.p_g_thousandths`). This proof will need to be re-derived when `cycle_logical_error_rate` becomes a real per-code model and `f_code` becomes the genuine `a · (p_g / p_star)^{(d+1)/2}` ansatz.

FormalRV.Framework.CostModel

FormalRV/Framework/CostModel.lean

FormalRV.Framework.CostModel — the resource COST RULE as a first-class, PLUGGABLE component INSIDE the framework, with PURPOSE-TAGGED ancilla. Why this file exists (John, 2026-06-02). An earlier version hardcoded the surface-code routing-ancilla rule directly inside the naive schedule and waved at qLDPC "as future work outside the framework". That is wrong on principle: verification should live at the GENERAL level, and any code/hardware-specific rule must be modelled AS A FRAMEWORK INSTANCE — never special-cased outside. Same extensibility discipline as `System/InvariantFramework.lean` (a general `SpaceTimeInvariant` type + instances, the theorem proven once `∀`). The *general* `estimate` (`ResourceEstimate.lean`) already takes the architecture numbers as free inputs. Here we add the abstraction that PRODUCES those numbers from a code: a `CostModel` (a named bundle of pluggable rules), with `surfaceModel` and `qldpcModel` as two INSTANCES. The composition theorem `estimateWith_{time,qubits}` is proven ONCE over `∀ m : CostModel` (by `rfl`); swapping surface ↔ qLDPC is a parameter change, not a code change. PURPOSE-TAGGED ANCILLA (John, 2026-06-02). At the SYSTEM level every ancilla qubit is the SAME thing — a qubit handed out by the `RequestFreshAncilla` syscall, which is purpose-agnostic and provisions the untagged `.total`. The purpose tags are NOT a system-level distinction; they exist for VERIFICATION: (1) to check the compiler allocated the right count for each purpose, and (2) to FORCE us to remember to add ancilla qubits at the physical level during QEC (syndrome extraction) and lattice-surgery compilation — a purpose left untagged is a purpose easy to forget to allocate. After deciding the taxonomy from qianxu's qubit budget (App. E / Extended Data Tables) we keep exactly TWO purposes: • SYNDROME — syndrome-extraction (check) ancilla; the always-on QEC cost (≈ one per parity check; qLDPC counts these separately from data qubits). • SURGERY — lattice-surgery ancilla = the operation-zone N_A. NOTE "measuring a logical Pauli operator" IS lattice surgery (a logical Pauli-PRODUCT measurement), so it shares this ancilla — it is NOT a separate purpose. ROUTING is deliberately NOT a tag: on qianxu's reconfigurable neutral-atom array, qubit "routing" is ATOM TRANSPORT — a TIME cost in the schedule (the `Transport` / latency-invariant layer), not dedicated ancilla qubits. Surface code's standing routing area IS a real cost, but it is a PER-LOGICAL LAYOUT cost and lives in `physPer` (the ~2× patch), not in the operation-ancilla budget. WHERE THE SURFACE ↔ qLDPC DIFFERENCE LIVES (now inspectable): • surface — SURGERY/SYNDROME are bundled into the standing ~2× patch (`physPer`); the operation-ancilla tags are 0. Footprint scales with DATA AREA, INDEPENDENT of the measured operator (gidney-ekera-2021 §2.14: 2(d+1)² per logical). • qLDPC — SURGERY scales with the measured operator's PHYSICAL WEIGHT (Θ(w)·parallel; qianxu p.5 verbatim: "the ancilla qubit count scales with the maximum physical weight of the target logical operators"; Cross et al. 2024, arXiv:2407.18393), INDEPENDENT of block area; SYNDROME = the explicit parity-check count `|hx| + |hz|`. No Mathlib. Pure Nat / String / List.length. No `sorry`, no `axiom`.

structureAncillaBudget

structure AncillaBudget

Ancilla qubits broken down by PURPOSE, for verification. `total` is the flat count the system actually requests (purpose-agnostic); the two tags attribute it so the compiler's allocation can be checked per purpose and no purpose is forgotten.

defAncillaBudget.total

def AncillaBudget.total (a : AncillaBudget) : Nat

The total ancilla the system requests = sum over purposes. This is what the purpose-agnostic `RequestFreshAncilla` syscall provisions.

structureCostModel

structure CostModel

A resource cost model: the pluggable rules that turn a code (+ workload + measured-operator weight + parallel-PPM count) into the architecture numbers the general `estimate` consumes. `ancilla c w op_weight parallel : AncillaBudget` is the purpose-tagged rule that differs between code families. `op_weight` is the measured logical operator's PHYSICAL Hamming weight `w` (in the repo, `rowWeight (L.selectZ S)`); `parallel` is the number of PPMs run simultaneously; `w : Workload` supplies `n_logical` where a rule needs it. (Surface's per-logical routing area lives in `physPer`, NOT here — see the module header.)

defCostModel.toArch

def CostModel.toArch (m : CostModel) (w : Workload) (c : QECCode)
    (op_weight parallel : Nat) : Architecture

Build the existing `Architecture` record from a model + workload + code + the measured operator's weight + the parallel-PPM count. The flat `ancilla_qubits` field — what the purpose-agnostic syscall sees — receives the budget's `total`; everything downstream is reused unchanged.

theoremtoArch_ancilla_total

theorem toArch_ancilla_total (m : CostModel) (w : Workload) (c : QECCode)
    (op_weight parallel : Nat) :
    (m.toArch w c op_weight parallel).ancilla_qubits
      = (m.ancilla c w op_weight parallel).total

SYSTEM-LEVEL view: the architecture's flat `ancilla_qubits` (what `RequestFreshAncilla` provisions) is exactly the budget `total` — the purpose tags do not change the system interface; they are a verification aid.

defestimateWith

def estimateWith (m : CostModel) (hw : Hardware) (w : Workload) (c : QECCode)
    (op_weight parallel : Nat) : ResourceEstimate

THE ENTRY POINT: estimate resources under a plugged-in cost model.

theoremestimateWith_time

theorem estimateWith_time (m : CostModel) (hw : Hardware) (w : Workload)
    (c : QECCode) (op_weight parallel : Nat) :
    (estimateWith m hw w c op_weight parallel).time_us_tenths
      = w.n_toff * m.tauToff c * hw.cycle_time_us_tenths

For EVERY cost model, the wallclock is the explicit composition of the model's own `tauToff` rule with the workload and hardware.

theoremestimateWith_qubits

theorem estimateWith_qubits (m : CostModel) (hw : Hardware) (w : Workload)
    (c : QECCode) (op_weight parallel : Nat) :
    (estimateWith m hw w c op_weight parallel).qubits
      = w.n_logical * m.physPer c
        + (m.ancilla c w op_weight parallel).total
        + m.factory c

For EVERY cost model, the physical-qubit count is the explicit composition of `physPer` / the ancilla budget `total` / `factory`.

theoremestimateWith_qubits_tagged

theorem estimateWith_qubits_tagged (m : CostModel) (hw : Hardware) (w : Workload)
    (c : QECCode) (op_weight parallel : Nat) :
    (estimateWith m hw w c op_weight parallel).qubits
      = w.n_logical * m.physPer c
        + (m.ancilla c w op_weight parallel).syndrome
        + (m.ancilla c w op_weight parallel).surgery
        + m.factory c

The SAME count, with the ancilla expanded BY PURPOSE — the audit view: data + syndrome + surgery + factory.

theoremestimateWith_eq_estimate

theorem estimateWith_eq_estimate (m : CostModel) (hw : Hardware) (w : Workload)
    (c : QECCode) (op_weight parallel : Nat) :
    estimateWith m hw w c op_weight parallel
      = estimate hw w (m.toArch w c op_weight parallel)

Monotonicity carries over for free: `estimateWith m …` is *definitionally* an `estimate` call, so the sensitivity lemmas (`time_mono_*`, `qubits_mono_*`) apply to every plugged-in model without re-proof.

defsurfaceModel

def surfaceModel (factory : Nat) : CostModel

defqldpcModel

def qldpcModel (factory : Nat) : CostModel

theoremqldpc_surgery_area_independent

theorem qldpc_surgery_area_independent (factory : Nat) (c c' : QECCode)
    (w : Workload) (op_weight parallel : Nat) :
    ((qldpcModel factory).ancilla c w op_weight parallel).surgery
      = ((qldpcModel factory).ancilla c' w op_weight parallel).surgery

qLDPC SURGERY ancilla is INDEPENDENT of the code (its data-block size `n`): it depends only on the measured operator's weight and the parallel count.

theoremqldpc_surgery_eq

theorem qldpc_surgery_eq (factory : Nat) (c : QECCode) (w : Workload)
    (op_weight parallel : Nat) :
    ((qldpcModel factory).ancilla c w op_weight parallel).surgery = parallel * op_weight

qLDPC SURGERY ancilla in closed form: `parallel · op_weight`.

theoremqldpc_syndrome_eq

theorem qldpc_syndrome_eq (factory : Nat) (c : QECCode) (w : Workload)
    (op_weight parallel : Nat) :
    ((qldpcModel factory).ancilla c w op_weight parallel).syndrome
      = (c.n - c.k) / 2

qLDPC SYNDROME ancilla = qianxu's one-basis count `(n-k)/2`, consistent with the per-zone footprint `N = n + (n-k)/2`.

theoremsurface_phys_area_scaling

theorem surface_phys_area_scaling (factory : Nat) (c : QECCode) :
    (surfaceModel factory).physPer c = 2 * physPerLogical c

Surface footprint scales with DATA AREA: per-logical cost is `2 · physPerLogical c`, proportional to the patch size — and INDEPENDENT of the measured operator's weight (this is where surface routing-area lives).

theoremsurface_surgery_zero

theorem surface_surgery_zero (factory : Nat) (c : QECCode) (w : Workload)
    (op_weight parallel : Nat) :
    ((surfaceModel factory).ancilla c w op_weight parallel).surgery = 0

Surface has NO per-operation surgery ancilla (it is 0 — bundled in physPer).

theoremsurface_syndrome_zero

theorem surface_syndrome_zero (factory : Nat) (c : QECCode) (w : Workload)
    (op_weight parallel : Nat) :
    ((surfaceModel factory).ancilla c w op_weight parallel).syndrome = 0

Surface has NO separate syndrome ancilla tag (it is 0 — bundled in physPer).

defw0

private def w0 : Workload

Dummy workload (the surgery term ignores it).

example(example)

example : ((qldpcModel 0).ancilla { n

Processor bb18, physical weight 104 ⇒ 104 surgery ancilla qubits (Table 189 total = 104 surgery + 85 checks).

example(example)

example : ((qldpcModel 0).ancilla { n

Processor lp_20^{3,5}, physical weight 460 ⇒ 460 surgery ancilla (Table 813 = 460+353).

example(example)

example : ((qldpcModel 0).ancilla { n

High-rate / parallel: 8 simultaneous weight-104 PPMs ⇒ 8·104 = 832 surgery ancilla (the Õ(k·ω) parallel family).

example(example)

example (hw : Hardware) (w : Workload) (c : QECCode) (ow p : Nat) :
    (estimateWith (qldpcModel 2565) hw w c ow p).qubits
      = w.n_logical * physPerLogical c + (c.n - c.k) / 2 + p * ow + 2565

qLDPC end-to-end qubit composition, tagged by purpose (instance of `estimateWith_qubits_tagged`): data + syndrome(=(n-k)/2) + Θ(w)·p + factory.

example(example)

example (hw : Hardware) (w : Workload) (c : QECCode) (ow p : Nat) :
    (estimateWith (surfaceModel 2565) hw w c ow p).qubits
      = w.n_logical * (2 * physPerLogical c) + 2565

Surface end-to-end qubit composition: data area `2 · physPerLogical c` per logical, with BOTH operation-ancilla tags 0 (bundled in the standing patch).

FormalRV.Framework.Errors

FormalRV/Framework/Errors.lean

FormalRV.Framework.Errors — three error-mechanism definitions. Phase A.7 of the paper plan (`PAPER_PLAN.md`). The paper §2 splits end-to-end error into three mechanisms: (i) Logical (random): physical Pauli errors that escape the L4 decoder, producing an undetected logical Pauli on the protected data. Bounded by `logical_error_budget`. (ii) Approximation (deterministic): finite-precision synthesis of continuous rotations (T-decompositions of `R_z(θ)`, Solovay– Kitaev tails) and finite truncation of QFT phase registers. Bounded by `approximation_error`. (iii) Algorithmic uncertainty: even with perfect logical gates, the Ekerå–Håstad post-processor only succeeds with the lattice- good-region probability bound. Lower-bounded by `algorithmic_success_prob`. All three are Nat-valued placeholders in this tick (numerators per 10^k; the k is encoded by the caller). A later tick refines to `Real` once mathlib is imported.

deflogical_error_budget

def logical_error_budget (n_cycles : Nat) (d : Nat) : Nat

Total logical-Pauli error budget across `n_cycles` cycles on an L4 code of distance `d`. Placeholder: returns `n_cycles` directly, which a future tick will refine to `a · n_cycles · (p_g / p_star)^{(d+1)/2}` once mathlib supplies `Real.pow`.

defapproximation_error

def approximation_error (n_rotations : Nat) (eps_thousandths : Nat) : Nat

Deterministic synthesis-and-truncation error budget for an algorithm of `n_rotations` continuous rotations, each compiled at synthesis precision `eps_thousandths` (per 1000). Placeholder: returns the product; future tick refines to `n_rotations · eps`.

defalgorithmic_success_prob

def algorithmic_success_prob (q_A : Nat) (precision_thousandths : Nat) : Nat

Lower bound on Ekerå–Håstad post-processing success probability, in 1/1000-of-100% units (so a "success probability of 0.99" reads as 99/100, or the Nat value 99 in this stand-in). Placeholder formula: `q_A · 100 / (q_A + 1)`. This is monotone in `q_A` (more windows ⇒ higher success bound), gives 0 at `q_A = 0` (no measurement ⇒ no signal), 50 at `q_A = 1` (single-window ⇒ 50% ceiling under this placeholder), and approaches 100 as `q_A → ∞`. A faithful Ekerå–Håstad lattice-good-region bound will replace this once mathlib `Real` enters the project.

example(example)

example : logical_error_budget 100 5 = 100

Smoke checks: each `def` is callable.

example(example)

example : approximation_error 2 3 = 6

example(example)

example : algorithmic_success_prob 0 0 = 0

Monotonicity is visible: 0 windows ⇒ 0; 1 window ⇒ 50; 3 ⇒ 75; 33 ⇒ 97.

example(example)

example : algorithmic_success_prob 1 0 = 50

example(example)

example : algorithmic_success_prob 3 0 = 75

example(example)

example : algorithmic_success_prob 33 999 = 97

FormalRV.Framework.L1_Algorithm

FormalRV/Framework/L1_Algorithm.lean

FormalRV.Framework.L1_Algorithm — Layer 1 (algorithm) interface. Phase A.4 of the paper plan (`PAPER_PLAN.md`). This is the top layer of the four-layer software-stack framework: Shor's order-finding algorithm wrapped in the Ekerå–Håstad post-processor that recovers a non-trivial factor of an RSA modulus `N` from the windowed phase- estimation output. L1 consumes the L2 → L1 contract supplied by `L2_Gadgets.lean` (per-gadget semantic correctness + T-count) and produces the end-to-end algorithm-correctness theorem at the top of the stack. This tick declares only the `structure ShorAlgorithm` and the statement-only `theorem rsa_correct`. The semantic content of the theorem (the actual Ekerå–Håstad / continued-fractions success guarantee) is `sorry`-stubbed and will be filled by later ticks, most likely by re-exporting the SQIR / Coq Shor proof under an axiom block as a first iteration. The signature here freezes the L1 contract surface so Phase B can wire the toy N=15 instance against a stable theorem statement. *Tier 1 SQIR port now exists** at `FormalRV/SQIRPort/Shor.lean` (2026-05-15, John's direction): `Shor_correct_var` and `Shor_correct` ported with proofs as `sorry` and QuantumLib primitives as `axiom`. Future ticks will refine `rsa_correct` below into the `Shor_correct` body so the framework's L1 anchor binds to the SQIR theorem directly.

structureShorAlgorithm

structure ShorAlgorithm

The Shor + Ekerå–Håstad parametric algorithm instance. `N` is the composite integer to factor (e.g., RSA-2048 has `N` 2048-bit). `q_A` is the window parameter from Ekerå–Håstad: with `q_A` independent runs of windowed phase estimation, the post-processor succeeds with probability at least `algorithmic_success_prob`. For RSA-2048, qianxu (p. 5) takes `q_A = 33`.

theoremrsa_correct

theorem rsa_correct (alg : ShorAlgorithm) : True

The top-level algorithm-correctness theorem. Statement-only at this tick: "for the parametric Shor + Ekerå–Håstad instance, the post-processor recovers a non-trivial factor of `N` whenever the underlying phase-estimation outputs land inside the post-processor's lattice-good region." A later tick will refine the conclusion to a probability bound that consumes `algorithmic_success_prob` from `Errors.lean`.

defrsa2048_instance

def rsa2048_instance : ShorAlgorithm

Smoke check: a concrete instance at qianxu's RSA-2048 parameters.

example(example)

example : rsa2048_instance.q_A = 33

FormalRV.Framework.L2_Gadgets

FormalRV/Framework/L2_Gadgets.lean

FormalRV.Framework.L2_Gadgets — Layer 2 (logical arithmetic gadgets) interface. Phase A.3 of the paper plan (`PAPER_PLAN.md`). This file is the uniform re-export point for the verified-tier L2 gadgets the framework supplies: the Gidney ripple-carry adder and the single-iteration unary lookup. Both semantic-correctness theorems already exist in the project (`BQAlgo/RippleCarryAdder.lean` Iter 213; `BQAlgo/UnaryLookup.lean` Iter 241), but they were proven before the four-layer framework was formalised. Future Phase-A ticks will add controlled adder, modular reduction, and QFT to this namespace. L2 supplies the L2 → L1 contract: For each gadget, a per-gadget semantic-correctness theorem paired with a `T`-count theorem on the same construction.

abbrevgidney_adder_correct

abbrev gidney_adder_correct

Re-export: the Gidney ripple-carry adder's parametric semantic- correctness theorem. Closed at Iter 213 (2026-05-14) in `BQAlgo/RippleCarryAdder.lean`.

abbrevunary_lookup_iteration_correct

abbrev unary_lookup_iteration_correct

Re-export: the unary-lookup single-iteration semantic-correctness theorem. Closed at Iter 241 (2026-05-14) in `BQAlgo/UnaryLookup.lean`.

FormalRV.Framework.L3_PPM

FormalRV/Framework/L3_PPM.lean

FormalRV.Framework.L3_PPM — Layer 3 (Pauli-product measurement / logical operations) interface. Phase A.2 of the paper plan (`PAPER_PLAN.md`). This is the layer between L4 (QEC code) and L2 (logical arithmetic gadgets): the PPM gadget set + Clifford + T-injection that together form a complete logical gate set on top of an L4 code. L3 supplies the L3 → L2 contract: per_op_error (g : LogicalGate) (qec : QECCode) (hw : HardwareParams) : Nat bounded by `c · L4_cycle_logical_error_rate` for an explicit cycle-cost constant `c` derived from the gadget structure. This tick creates only the two top-level structures; magic-state cultivation, distillation factories, and the contract theorem are future ticks.

structurePPMGadget

structure PPMGadget

A PPM gadget: a protocol that performs one logical Pauli-product measurement on the data qubits of an L4 code, at a stated cycle cost. `operator_weight` is the maximum weight of the logical Pauli product the gadget supports. `tau_s` is the cycle count per measurement — for standard surface-code lattice surgery this is `d`; for qLDPC surgery it is generally `2 d / 3` (paper-cited, Layer-3 derivable from a concrete surgery construction).

structureLogicalGateSet

structure LogicalGateSet

A complete logical gate set on top of an L4 code: the Pauli / Clifford generators that surface-code or qLDPC surgery makes available natively, plus a `T`-state injection primitive that closes the gate set to universal computation via the magic-state factory of L3. The `ppm` field links back to the PPM gadget that implements joint logical measurements; `magic_factory_qubit_cost` is a coarse placeholder for the per-T-state qubit-rounds overhead — the L2 contract consumes this directly.

example(example)

example : (LogicalGateSet.mk
            { target

Smoke check: a trivial gate set on a trivial code builds.

deftau_s_cost

def tau_s_cost (g : PPMGadget) : Nat

Canonical cycle-cost projection on a PPM gadget: the number of L4 cycles per logical Pauli-product measurement. Phase-C corpus instances will read off paper-stated `τ_s` values through this projection so the derivation chain is uniform.

FormalRV.Framework.L4_QECCode

FormalRV/Framework/L4_QECCode.lean

FormalRV.Framework.L4_QECCode — Layer 4 (QEC code) interface. Phase A.1 of the paper plan (`PAPER_PLAN.md`). This is the bottom layer of the four-layer software-stack framework: parity-check matrices + code parameters + a placeholder for the subthreshold logical-error-rate ansatz. Layer-4 supplies the L4 → L3 contract: cycle_logical_error_rate (qec : QECCode) (hw : HardwareParams) : Nat bounded by `f_code (hw.p_g_thousandths) qec.d`. This tick creates only the `structure QECCode` declaration and a stub `f_code`. Mathematical content (surface-code analytic ansatz, qLDPC numerical fit) is the job of future ticks.

structureQECCode

structure QECCode

A quantum LDPC code, given by its parity-check matrices and code parameters. `(n, k, d)` are the standard `[[n, k, d]]` code parameters: `n` physical data qubits, `k` logical qubits encoded, `d` minimum-weight stabilizer distance. `hx` and `hz` are the X- and Z-stabilizer parity-check matrices, represented as lists of rows of bits. A row `[true, false, false, true]` encodes a stabilizer acting nontrivially on qubits 0 and 3.

deff_code

def f_code (p_g_thousandths : Nat) (d : Nat) : Nat

Subthreshold logical-error-rate ansatz `p_L = a (p_g / p_star)^{(d+1)/2}`, held here as a placeholder Nat-domain stub. Future ticks will refine to `Real` and supply explicit coefficients for the surface code and qLDPC families considered by the paper. The current stub returns the physical error rate unchanged — a trivial upper bound (true for `d = 1`) that lets the file build dependency-free.

example(example)

example : f_code 1 5 = 1

Smoke check: the stub builds and `f_code` is callable.

FormalRV.Framework.PaperClaims

FormalRV/Framework/PaperClaims.lean

FormalRV.PaperClaims — canonical index of every major resource claim in the papers under review. Per CLAUDE.md "Paper-claim-first workflow", each `paper_claim_*` is the paper's stated number (with citation). Verification modules import from here and prove `*_meets_paper_claim` (or fail to). This file is data only — no theorems. If a number is wrong here, fix it; the verification cascade will re-run. Naming convention: `<bibkey>_<what>_<units>`. Always carry units in the identifier (`_qubits`, `_toffolis`, `_cycles`, `_microseconds`, `_milliseconds`, `_days`). Approximations: where the paper writes "≈" we record the central value and note the approximation in the docstring. Where the paper writes "≤" we record the upper bound and the docstring carries that.

defqianxu_bb18_n_qubits

def qianxu_bb18_n_qubits         : Nat

bb18 bivariate-bicycle code — [[n, k, d]] = [[248, 10, ≤18]], rate 0.04.

defqianxu_bb18_k_logical_qubits

def qianxu_bb18_k_logical_qubits : Nat

defqianxu_bb18_d_distance_upper

def qianxu_bb18_d_distance_upper : Nat

defqianxu_lp_20_3_5_n_qubits

def qianxu_lp_20_3_5_n_qubits         : Nat

lp_20^{3,5} processor code (balanced-arch processor) — [[1122, 148, ≤20]].

defqianxu_lp_20_3_5_k_logical_qubits

def qianxu_lp_20_3_5_k_logical_qubits : Nat

defqianxu_lp_20_3_5_d_distance_upper

def qianxu_lp_20_3_5_d_distance_upper : Nat

defqianxu_lp_16_3_7_n_qubits

def qianxu_lp_16_3_7_n_qubits         : Nat

lp_16^{3,7} memory code — [[2610, 744, ≤16]], rate 0.29.

defqianxu_lp_16_3_7_k_logical_qubits

def qianxu_lp_16_3_7_k_logical_qubits : Nat

defqianxu_lp_16_3_7_d_distance_upper

def qianxu_lp_16_3_7_d_distance_upper : Nat

defqianxu_lp_20_3_7_n_qubits

def qianxu_lp_20_3_7_n_qubits         : Nat

lp_20^{3,7} memory code — [[4350, 1224, ≤20]], rate 0.29.

defqianxu_lp_20_3_7_k_logical_qubits

def qianxu_lp_20_3_7_k_logical_qubits : Nat

defqianxu_lp_20_3_7_d_distance_upper

def qianxu_lp_20_3_7_d_distance_upper : Nat

defqianxu_lp_24_3_7_n_qubits

def qianxu_lp_24_3_7_n_qubits         : Nat

lp_24^{3,7} memory code — [[5278, 1480, ≤24]], rate 0.28.

defqianxu_lp_24_3_7_k_logical_qubits

def qianxu_lp_24_3_7_k_logical_qubits : Nat

defqianxu_lp_24_3_7_d_distance_upper

def qianxu_lp_24_3_7_d_distance_upper : Nat

defqianxu_tau_s_numerator

def qianxu_tau_s_numerator   : Nat

Surgery cycles per PPM ≈ 2·d_p / 3, where d_p is processor code distance. For d_p = 20: τ_s ≈ 13 cycles. Stored as (numerator, denominator) of 2/3.

defqianxu_tau_s_denominator

def qianxu_tau_s_denominator : Nat

defqianxu_per_toffoli_adder_se_tau_s

def qianxu_per_toffoli_adder_se_tau_s : Nat

Per-Toffoli cost in adders, space-efficient/balanced architecture (qianxu p. 24 body text). 25 τ_s. Derived from E3: τ_adder = 25 q_A τ_s.

defqianxu_per_toffoli_ctl_adder_tau_s

def qianxu_per_toffoli_ctl_adder_tau_s : Nat

Per-Toffoli cost in controlled-adders. 15 τ_s (qianxu p. 24, both architectures). Derived from E4: τ_ctl-adder = 30 q_A τ_s, with 2 q_A Toffolis per ctl-adder.

defqianxu_per_toffoli_adder_balanced_tau_s

def qianxu_per_toffoli_adder_balanced_tau_s : Nat

Per-Toffoli cost in adders when adder fits inside processor block (RSA-2048 balanced; qianxu p. 24 body, derived from E5). 13 τ_s.

defqianxu_per_toffoli_lookup_se_tau_s

def qianxu_per_toffoli_lookup_se_tau_s : Nat

Per-Toffoli cost in lookups, space-efficient architecture (qianxu p. 24 body text + Eq. E9). 71 τ_s. Derived from E9: `τ_lookup ≈ 15·q_w / (k_p − 3)` per Toffoli, where `q_w` is the window width and `k_p` is the lookup-table key parameter for the RSA-2048 instance. The 71 is the rounded value the paper carries forward into E10 (`0.5·25 + 0.5·71`).

defqianxu_E9_lookup_formula_numerator

def qianxu_E9_lookup_formula_numerator : Nat

The numerator constant in qianxu Eq. E9's lookup-cost formula: `τ_lookup ≈ 15·q_w / (k_p − 3)`. Carries forward as a structural anchor; a future tick will encode `q_w` and `k_p` symbolically and prove the ratio reaches 71 for the RSA-2048 parameter choice.

defqianxu_E9_evaluated

def qianxu_E9_evaluated (q_w k_p : Nat) : Nat

qianxu Eq. E9 evaluated for given window-width `q_w` and lookup key parameter `k_p`: returns the per-Toffoli τ_s cost `15·q_w / (k_p − 3)` using Nat integer division.

defqianxu_E9_q_w_RSA2048

def qianxu_E9_q_w_RSA2048 : Nat

Word length `q_w` for the RSA-2048 lookup, **as read from qianxu p. 23-24 (close reading 2026-05-12 12:32 PDT)**. The paper uses `q_w = 33`. Combined with `k_p = 10` below, the E9 formula evaluates as `15·33/(10−3) = 495/7 ≈ 70.71`, which the paper rounds to `71 τ_s` (the value appearing in Eq. E10). Note: under Nat integer division `495/7 = 70`, off by 1 from the paper's rounded 71. The `qianxu_E9_evaluated_matches_paper` decide example below uses a `≤ 1` slack to account for this real-vs-integer-division discrepancy.

defqianxu_E9_k_p_RSA2048

def qianxu_E9_k_p_RSA2048 : Nat

Processor-block size `k_p` for the RSA-2048 space-efficient architecture, **paper-actual** per qianxu p. 24 ("In the space-efficient architecture with k_p = 10...").

defqianxu_E9_q_w_RSA2048_alt_candidate

def qianxu_E9_q_w_RSA2048_alt_candidate : Nat

Preserved as an `_alt_candidate` for posterity: under Nat integer division, `(q_w=19, k_p=7)` recovers 71 exactly (`15·19/4 = 285/4 = 71`). This is a *valid* parametric solution but NOT the paper's actual choice.

defqianxu_E9_k_p_RSA2048_alt_candidate

def qianxu_E9_k_p_RSA2048_alt_candidate : Nat

Companion alternate to `_q_w_RSA2048_alt_candidate`.

defcuccaro_adder_toffolis_per_bit_qrisp

def cuccaro_adder_toffolis_per_bit_qrisp : Nat

Per-bit Toffoli count derived from Qrisp's Cuccaro adder implementation (one Toffoli per forward MAJ at each bit + one per reverse UMA = 2 per bit). Source: `PyCircuits/adders/CUCCARO_GATE_SEQUENCE.md` — read directly from `qrisp/src/qrisp/alg_primitives/arithmetic/adders/cuccaro_adder.py`. This is NOT a paper-claim def; it is a gate-derived review anchor. See `cuccaro_total_toffolis_n_bit_adder` below for the n-bit aggregate.

defcuccaro_total_toffolis_n_bit_adder

def cuccaro_total_toffolis_n_bit_adder (n : Nat) : Nat

Total Toffoli count for an n-bit Cuccaro adder, derived from the Qrisp gate sequence: 2 per bit × n bits. Will be cross-checked against Qrisp's compiled `mcx` count once `python PyCircuits/adders/cuccaro_qrisp.py` is run.

example(example)

example : cuccaro_total_toffolis_n_bit_adder 4 = 8

The 4-bit Cuccaro adder has 8 Toffolis.

defcuccaro_total_tau_s_n_bit_adder

def cuccaro_total_tau_s_n_bit_adder (n : Nat) : Nat

Cross-binding: at qianxu's 25 τ_s/Toffoli for adders, the n-bit Cuccaro adder costs `2n × 25 = 50n τ_s`. If qianxu's Eq. E3 `τ_adder ≈ 25 q_A τ_s` is total adder cost (not per Toffoli), this implies a factor-of-2 disambiguation flagged in `PyCircuits/adders/CUCCARO_GATE_SEQUENCE.md`.

example(example)

example : cuccaro_total_tau_s_n_bit_adder 4 = 200

4-bit Cuccaro adder costs 200 τ_s under the per-Toffoli reading of qianxu's "25" anchor.

defgidney_adder_toffolis_per_bit_qrisp

def gidney_adder_toffolis_per_bit_qrisp : Nat

Per-bit Toffoli count of Qrisp's Gidney adder. Source: `PyCircuits/adders/GIDNEY_GATE_SEQUENCE.md` — read directly from `qrisp/src/qrisp/alg_primitives/arithmetic/adders/gidney/qq_gidney_adder.py`. *Key difference from Cuccaro**: Gidney's `mcx(method="gidney")` uses measurement-based logical-AND uncomputation — 1 Toffoli forward, **0 Toffolis on the reverse pass** (the inverse compiles to CNOTs + a classical decision based on the measurement outcome). So Gidney costs **1 Toffoli per bit**, half of classic Cuccaro's 2 Toffolis per bit. This matches qianxu's claim: p. 22 says the q_A-bit adder uses "q_A Toffoli gates, q_A mid-circuit measurements."

defgidney_total_toffolis_n_bit_adder

def gidney_total_toffolis_n_bit_adder (n : Nat) : Nat

Total Toffoli count for an n-bit Gidney adder: 1 per bit × n bits = n. With c_out attached (so b extends by 1 bit) this is actually q_A Toffolis per q_A-bit adder, matching qianxu p. 22 word-for-word.

example(example)

example : gidney_total_toffolis_n_bit_adder 4 = 4

The 4-bit Gidney adder has 4 Toffolis (vs Cuccaro's 8).

defgidney_total_tau_s_n_bit_adder

def gidney_total_tau_s_n_bit_adder (n : Nat) : Nat

Total τ_s cost of an n-bit Gidney adder, at qianxu's 25 τ_s/Toffoli for adders: `n × 25 = 25n τ_s`. **Directly recovers qianxu Eq. E3: `τ_adder = 25 q_A τ_s`** for q_A = n.

example(example)

example : gidney_total_tau_s_n_bit_adder 4 = 100

4-bit Gidney adder costs 100 τ_s (Cuccaro would cost 200 τ_s).

theoremgidney_n_bit_adder_meets_qianxu_E3

theorem gidney_n_bit_adder_meets_qianxu_E3 (n : Nat) :
    gidney_total_tau_s_n_bit_adder n = qianxu_per_toffoli_adder_se_tau_s * n

*First gate-derived recovery of qianxu Eq. E3**: `gidney_total_tau_s_n_bit_adder n = 25 · n` literally (for the Gidney variant Qrisp implements, which is what qianxu actually uses). The paper's "τ_adder = 25 q_A τ_s" claim is therefore *structurally faithful** to a real ripple-carry implementation — it is not an averaged or amortized figure.

example(example)

example (n : Nat) :
    cuccaro_total_tau_s_n_bit_adder n
      = 2 * gidney_total_tau_s_n_bit_adder n

The Cuccaro vs Gidney τ_s comparison: at any n, Cuccaro is exactly 2× Gidney. This is the factor-of-2 disambiguation that vanishes once we use the variant qianxu actually uses.

example(example)

example :
    qianxu_E9_evaluated qianxu_E9_q_w_RSA2048_alt_candidate
                        qianxu_E9_k_p_RSA2048_alt_candidate
      = qianxu_per_toffoli_lookup_se_tau_s

The alternate candidate (q_w, k_p) = (19, 7) recovers the paper's rounded "71 τ_s" figure exactly under Nat integer division. Decide-checked. Kept for posterity — not the actual paper parameters.

example(example)

example :
    qianxu_E9_evaluated qianxu_E9_q_w_RSA2048
                        qianxu_E9_k_p_RSA2048
      = 70

*Paper-actual** (q_w, k_p) = (33, 10) per qianxu p. 24: `15·33 / (10−3) = 495 / 7 = 70` under Nat integer division. Paper rounds the real-valued `70.71...` to `71`. Decide-checked.

example(example)

example :
    qianxu_per_toffoli_lookup_se_tau_s
      - qianxu_E9_evaluated qianxu_E9_q_w_RSA2048 qianxu_E9_k_p_RSA2048
      ≤ 1

The paper's "71" is reachable from the paper-actual parameters only modulo the real-vs-integer-division off-by-one.

defqianxu_E9_lookup_gate_derived_count

def qianxu_E9_lookup_gate_derived_count (q_a : Nat) : Nat

Paper-claim Toffoli count for a single sub-lookup with `q_a` address bits: `2^q_a`. Source: qianxu p. 23. This is the count the paper relies on for the per-Toffoli cost figure of `15·q_w/(k_p-3) ≈ 71 τ_s`.

defqianxu_E9_q_a_RSA2048

def qianxu_E9_q_a_RSA2048 : Nat

For RSA-2048 SE (q_a = 6 per qianxu p. 24): 64 Toffolis per sub-lookup.

example(example)

example : qianxu_E9_lookup_gate_derived_count qianxu_E9_q_a_RSA2048 = 64

defqianxu_E9_total_tau_s_sub_lookup

def qianxu_E9_total_tau_s_sub_lookup (q_a : Nat) : Nat

Total τ_s cost of one space-efficient sub-lookup at qianxu's stated `71 τ_s/Toffoli`: `qianxu_per_toffoli_lookup_se_tau_s × 2^q_a τ_s`. Recovers qianxu Eq. E9 evaluated structurally — though the per-Toffoli figure (71) is still a `paper_claim_*` def, since the gate-faithful chain from a custom unary cascade to the cycle-cost formula isn't fully built yet (future ticks).

example(example)

example :
    qianxu_E9_total_tau_s_sub_lookup qianxu_E9_q_a_RSA2048 = 4544

For RSA-2048 SE: one sub-lookup costs `71 × 64 = 4544 τ_s`.

defqianxu_E9_num_sub_lookups

def qianxu_E9_num_sub_lookups (q_w k_p : Nat) : Nat

Number of sub-lookups for RSA-2048 SE: `⌈q_w / (k_p − 3)⌉ = ⌈33/7⌉ = 5`. Encoded via Nat ceiling: `(a + b - 1) / b`.

example(example)

example :
    qianxu_E9_num_sub_lookups qianxu_E9_q_w_RSA2048 qianxu_E9_k_p_RSA2048 = 5

defqianxu_E9_full_lookup_tau_s_RSA2048

def qianxu_E9_full_lookup_tau_s_RSA2048 : Nat

The full lookup at RSA-2048 SE: 5 sub-lookups × 4544 τ_s = 22720 τ_s. This is the **total** τ_s cost of one full lookup (not per Toffoli) in the space-efficient RSA-2048 architecture, derived from the `qianxu_E9_*` chain.

example(example)

example : qianxu_E9_full_lookup_tau_s_RSA2048 = 22720

defqianxu_per_toffoli_ctl_adder_se_tau_s

def qianxu_per_toffoli_ctl_adder_se_tau_s : Nat

Per-Toffoli τ_s cost of the controlled adder in the space-efficient architecture, per Eq. E4: `τ_ctl-adder / 2 q_A = 30 q_A / 2 q_A = 15`.

defctl_adder_total_toffolis_n_bit

def ctl_adder_total_toffolis_n_bit (n : Nat) : Nat

Toffoli count of the ctl-adder Gidney-variant chain: `2 · n` per n-bit ctl-adder (n on downward pass + n on upward pass for the additional controlled part). Source: qianxu p. 22 + Gidney structural extension.

example(example)

example : ctl_adder_total_toffolis_n_bit 4 = 8

The 4-bit ctl-adder has 8 Toffolis.

defctl_adder_total_tau_s_n_bit

def ctl_adder_total_tau_s_n_bit (n : Nat) : Nat

Total τ_s cost of an n-bit ctl-adder: `2 n × 15 = 30 n τ_s`.

example(example)

example : ctl_adder_total_tau_s_n_bit 4 = 120

4-bit ctl-adder costs 120 τ_s.

theoremctl_adder_n_bit_meets_qianxu_E4

theorem ctl_adder_n_bit_meets_qianxu_E4 (n : Nat) :
    ctl_adder_total_tau_s_n_bit n = 30 * n

*Gate-derived recovery of Eq. E4**: `ctl_adder_total_tau_s_n_bit n = 30 · n` literally.

example(example)

example (n : Nat) :
    5 * ctl_adder_total_tau_s_n_bit n
      = 6 * gidney_total_tau_s_n_bit_adder n

Cross-check: at any n, ctl-adder is exactly `30/25 = 6/5` times the plain Gidney adder under qianxu's stated per-Toffoli rates. Concretely, `5 · ctl_adder_total_tau_s = 6 · gidney_total_tau_s` so the ratio is rational with no rounding.

theoremqianxu_E9_full_lookup_via_toffoli_count

theorem qianxu_E9_full_lookup_via_toffoli_count :
    qianxu_E9_full_lookup_tau_s_RSA2048
      = qianxu_E9_num_sub_lookups qianxu_E9_q_w_RSA2048 qianxu_E9_k_p_RSA2048
        * qianxu_E9_lookup_gate_derived_count qianxu_E9_q_a_RSA2048
        * qianxu_per_toffoli_lookup_se_tau_s

Cross-check: total Toffolis in the full RSA-2048 SE lookup = `num_sub_lookups · 2^q_a = 5 · 64 = 320`. Combined with the `71 τ_s/Toffoli` figure, total = `320 · 71 = 22720 τ_s`. Both formulations agree.

defqianxu_E10_tau_Toff_RSA_se_tau_s

def qianxu_E10_tau_Toff_RSA_se_tau_s : Nat

E10: space-efficient RSA-2048 amortized τ_Toff. Paper says 43 τ_s. The arithmetic LHS (0.5·25 + 0.5·71) actually yields 48 — see `lean/FormalRV/G_A.lean` for the formal `decide` refuting this.

defqianxu_E11_tau_Toff_RSA_balanced_tau_s

def qianxu_E11_tau_Toff_RSA_balanced_tau_s : Nat

E11: balanced RSA-2048 amortized τ_Toff. 10 τ_s.

defqianxu_E12_tau_Toff_ECC_se_tau_s

def qianxu_E12_tau_Toff_ECC_se_tau_s : Nat

E12: space-efficient ECC-256 amortized τ_Toff. 72 τ_s.

defqianxu_E13_tau_Toff_ECC_balanced_tau_s

def qianxu_E13_tau_Toff_ECC_balanced_tau_s : Nat

E13: balanced ECC-256 amortized τ_Toff. 19 τ_s.

defqianxu_ECC256_pct_adders

def qianxu_ECC256_pct_adders     : Nat

Paper assumes ECC-256 Toffoli count splits as 40% adders + 50% controlled-adders + 10% lookups. Stored as integer percentages.

defqianxu_ECC256_pct_ctl_adders

def qianxu_ECC256_pct_ctl_adders : Nat

defqianxu_ECC256_pct_lookups

def qianxu_ECC256_pct_lookups    : Nat

defqianxu_total_qubits_ECC_space_eff

def qianxu_total_qubits_ECC_space_eff : Nat

Space-efficient ECC-256 with lp_20^{3,7} memory: 9,739 qubits.

defqianxu_total_qubits_RSA_space_eff

def qianxu_total_qubits_RSA_space_eff : Nat

Space-efficient RSA-2048 with lp_24^{3,7} memory: 11,033 qubits.

defqianxu_total_qubits_ECC_balanced

def qianxu_total_qubits_ECC_balanced : Nat

Balanced ECC-256 with lp_20^{3,7} memory: 11,961 qubits.

defqianxu_total_qubits_RSA_balanced

def qianxu_total_qubits_RSA_balanced : Nat

Balanced RSA-2048 with lp_24^{3,7} memory: 13,255 qubits.

defqianxu_total_qubits_ECC_time_eff_P20

def qianxu_total_qubits_ECC_time_eff_P20 : Nat

Time-efficient ECC-256 (P=20): ≈19,000 qubits.

defqianxu_total_qubits_ECC_time_eff_P130

def qianxu_total_qubits_ECC_time_eff_P130 : Nat

Time-efficient ECC-256 (P=130): ≈26,000 qubits.

defqianxu_total_qubits_RSA_time_eff_P100

def qianxu_total_qubits_RSA_time_eff_P100 : Nat

Time-efficient RSA-2048 (P=100): ≈68,000 qubits.

defqianxu_total_qubits_RSA_time_eff_P1160

def qianxu_total_qubits_RSA_time_eff_P1160 : Nat

Time-efficient RSA-2048 (P=1160): ≈102,000 qubits.

defqianxu_runtime_RSA_space_eff_days

def qianxu_runtime_RSA_space_eff_days     : Nat

defqianxu_runtime_RSA_balanced_days

def qianxu_runtime_RSA_balanced_days      : Nat

defqianxu_runtime_RSA_time_eff_P100_days

def qianxu_runtime_RSA_time_eff_P100_days : Nat

defqianxu_runtime_RSA_time_eff_P1160_days

def qianxu_runtime_RSA_time_eff_P1160_days : Nat

defqianxu_runtime_ECC_space_eff_days

def qianxu_runtime_ECC_space_eff_days     : Nat

defqianxu_runtime_ECC_balanced_days

def qianxu_runtime_ECC_balanced_days      : Nat

defqianxu_runtime_ECC_time_eff_P20_days

def qianxu_runtime_ECC_time_eff_P20_days  : Nat

defqianxu_runtime_ECC_time_eff_P130_days

def qianxu_runtime_ECC_time_eff_P130_days : Nat

defqianxu_cycle_time_microseconds

def qianxu_cycle_time_microseconds : Nat

Stabilizer-measurement cycle assumed by qianxu: 1 ms = 1000 µs.

defqianxu_p_T_numerator

def qianxu_p_T_numerator   : Nat

Cultivated |T⟩ error rate at p = 0.1%: ≈ 10⁻⁶ (numerator/denominator).

defqianxu_p_T_denominator

def qianxu_p_T_denominator : Nat

defqianxu_p_CCZ_numerator

def qianxu_p_CCZ_numerator   : Nat

Output |C̄CZ̄⟩ error rate via 8T-to-CCZ: p_CCZ ≈ 28·(2 p_T)² ≈ 10⁻¹⁰.

defqianxu_p_CCZ_denominator

def qianxu_p_CCZ_denominator : Nat

defqianxu_factory_kf_states

def qianxu_factory_kf_states : Nat

|C̄CZ̄⟩ states produced per factory round: k_f = 10.

defqianxu_factory_round_cycles

def qianxu_factory_round_cycles : Nat

Total time per factory round (cycles): 8·(τ_T + 2·τ_s^cult) ≈ 120.

defqianxu_factory_size_qubits

def qianxu_factory_size_qubits : Nat

Factory size (qubits) for space-efficient/balanced arch using bb18: 5·N_f + k_f·N_s ≈ 2565.

defqianxu_ancilla_lp_20_3_7_qubits

def qianxu_ancilla_lp_20_3_7_qubits : Nat

defqianxu_ancilla_lp_24_3_7_qubits

def qianxu_ancilla_lp_24_3_7_qubits : Nat

defbabbush_ECC256_lowqubit_logical_qubits

def babbush_ECC256_lowqubit_logical_qubits : Nat

Babbush low-qubit ECC-256 variant: ≤1200 logical qubits / ≤90M Toffolis. (Babbush §B "Updated Quantum Resource Estimates", p. 7.)

defbabbush_ECC256_lowqubit_toffolis

def babbush_ECC256_lowqubit_toffolis       : Nat

defbabbush_ECC256_lowgate_logical_qubits

def babbush_ECC256_lowgate_logical_qubits : Nat

Babbush low-gate ECC-256 variant: ≤1450 logical qubits / ≤70M Toffolis.

defbabbush_ECC256_lowgate_toffolis

def babbush_ECC256_lowgate_toffolis       : Nat

defbabbush_ECC256_fastclock_physical_qubits

def babbush_ECC256_fastclock_physical_qubits : Nat

Physical qubit count under SC architecture, 10⁻³ error rate, fast-clock superconducting: ≤500,000. (p. 8.)

defbabbush_ECC256_fastclock_runtime_minutes_low

def babbush_ECC256_fastclock_runtime_minutes_low  : Nat

Wall-clock runtime, fast-clock superconducting (1µs rounds, 10µs reaction time, 50% Toffoli overhead): 18-23 minutes.

defbabbush_ECC256_fastclock_runtime_minutes_high

def babbush_ECC256_fastclock_runtime_minutes_high : Nat

defbabbush_ECC256_fastclock_magic_qubits

def babbush_ECC256_fastclock_magic_qubits : Nat

Magic state production qubits, fast-clock arch: 25,000 physical qubits.

defbabbush_ECC256_slowclock_magic_qubits

def babbush_ECC256_slowclock_magic_qubits : Nat

Slow-clock arch (100µs rounds): 2.5 million physical qubits for magic.

defgidney_ekera_2021_RSA2048_physical_megaqubits

def gidney_ekera_2021_RSA2048_physical_megaqubits : Nat

Gidney-Ekerå 2021 RSA-2048: 20 megaqubits physical (Tab. 2, last row).

defgidney_ekera_2021_RSA2048_runtime_centidays

def gidney_ekera_2021_RSA2048_runtime_centidays : Nat

Expected runtime for RSA-2048 (parallel construction): 0.31 days (≈ 7.4 hours; the title's "8 hours" is the rounded figure).

defgidney_ekera_2021_RSA2048_megaqubitdays_tenths

def gidney_ekera_2021_RSA2048_megaqubitdays_tenths : Nat

Spacetime volume: 6.6 megaqubitdays (Tab. 2).

defgidney_ekera_2021_RSA2048_toffolis_billions

def gidney_ekera_2021_RSA2048_toffolis_billions : Nat

Toffoli+T/2 count formula coefficients (Tab. 1, ours 2019 row): Toffoli count = 0.3·n³ + 0.0005·n³·lg(n). For n=2048: ≈ 2.7 × 10⁹ Toffolis.

defgidney_ekera_2021_RSA2048_abstract_qubits

def gidney_ekera_2021_RSA2048_abstract_qubits : Nat

Abstract qubit count formula (Tab. 1): n_e = 3n + 0.002·n·lg(n). For n=2048: ≈ 6200 abstract qubits.

defgidney_ekera_2021_cycle_time_microseconds

def gidney_ekera_2021_cycle_time_microseconds : Nat

Surface-code physical assumptions: cycle 1 µs, gate error 0.1%, reaction time 10 µs, planar connectivity.

defgidney_ekera_2021_reaction_time_microseconds

def gidney_ekera_2021_reaction_time_microseconds : Nat

defgidney_ekera_2021_gate_error_perthousand

def gidney_ekera_2021_gate_error_perthousand : Nat

defgidney_2025_RSA2048_physical_qubits_upper

def gidney_2025_RSA2048_physical_qubits_upper : Nat

Gidney 2025 RSA-2048: less than 1 million physical qubits.

defgidney_2025_RSA2048_runtime_days_upper

def gidney_2025_RSA2048_runtime_days_upper : Nat

Less than 1 week.

defgidney_2025_cycle_time_microseconds

def gidney_2025_cycle_time_microseconds : Nat

Same physical assumptions as 2021.

defgidney_2025_reaction_time_microseconds

def gidney_2025_reaction_time_microseconds : Nat

defgidney_2025_gate_error_perthousand

def gidney_2025_gate_error_perthousand : Nat

defgidney_2018_cuccaro_adder_tcount_per_bit

def gidney_2018_cuccaro_adder_tcount_per_bit : Nat

Cuccaro-style n-bit ripple-carry adder T-count: 8n + O(1). Stored as the leading coefficient.

defgidney_2018_logical_AND_adder_tcount_per_bit

def gidney_2018_logical_AND_adder_tcount_per_bit : Nat

Gidney 2018 logical-AND adder T-count: 4n + O(1).

defgidney_2018_logical_AND_compute_tcount

def gidney_2018_logical_AND_compute_tcount   : Nat

Logical-AND temporary requires 4 T to compute, 0 T to uncompute.

defgidney_2018_logical_AND_uncompute_tcount

def gidney_2018_logical_AND_uncompute_tcount : Nat

defdraper_2006_QCLA_depth_log_factor

def draper_2006_QCLA_depth_log_factor : Nat

Carry-lookahead adder depth: O(log n). Coefficient placeholder.

defdraper_2006_QCLA_ancilla_per_bit

def draper_2006_QCLA_ancilla_per_bit : Nat

Carry-lookahead adder ancillary qubits: O(n) (linear in input size).

deflitinski_15to1_9333_qubits

def litinski_15to1_9333_qubits : Nat

(15-to-1)_{9,3,3,3} at p_phys = 10⁻⁴: 1150 qubits, 18.1 cycles, p_out = 9.3 × 10⁻¹⁰. Space-time = 4.71·d³ at d = 15.

deflitinski_15to1_9333_cycles_tenths

def litinski_15to1_9333_cycles_tenths : Nat

deflitinski_15to1_9333_pout_neg_log10

def litinski_15to1_9333_pout_neg_log10 : Nat

deflitinski_15to1_9333_full_distance_d

def litinski_15to1_9333_full_distance_d : Nat

deflitinski_8toCCZ_qubits

def litinski_8toCCZ_qubits : Nat

(15-to-1)_{7,3,3} × (8-to-CCZ)_{15,7,9} at p_phys = 10⁻⁴: 12,400 qubits, 36.1 cycles, p_out = 7.2 × 10⁻¹⁴, full distance = 21. **This is the 8T-to-CCZ protocol qianxu uses.**

deflitinski_8toCCZ_cycles_tenths

def litinski_8toCCZ_cycles_tenths : Nat

deflitinski_8toCCZ_pout_neg_log10

def litinski_8toCCZ_pout_neg_log10 : Nat

deflitinski_8toCCZ_full_distance_d

def litinski_8toCCZ_full_distance_d : Nat

defxu_2024_LP_k80_physical_qubits

def xu_2024_LP_k80_physical_qubits      : Nat

LP code physical-qubit savings vs surface code (Tab. 1, k=80 logical): LP: 1367 physical, surface: 12862, ratio 9.4×.

defxu_2024_surface_k80_physical_qubits

def xu_2024_surface_k80_physical_qubits : Nat

defxu_2024_LP_transport_exponent_denominator

def xu_2024_LP_transport_exponent_denominator : Nat

LP transport-time scaling on atom arrays (supplementary): O(n^{1/2}) after layout flattening (NOT O(L^{1/4}) as qianxu's main-text defense claims). Stored as the exponent denominator (1/2 = 1/2).

defzheng_2025_gross_n_qubits

def zheng_2025_gross_n_qubits : Nat

High-rate surgery demonstrated on Gross code [[144,12,12]].

defzheng_2025_gross_k_logical

def zheng_2025_gross_k_logical : Nat

defzheng_2025_gross_d_distance

def zheng_2025_gross_d_distance : Nat

defzheng_2025_SC_n_qubits

def zheng_2025_SC_n_qubits : Nat

Also demonstrated on a new SC code [[1125, 245, ≤10]].

defzheng_2025_SC_k_logical

def zheng_2025_SC_k_logical : Nat

defzheng_2025_SC_d_distance_upper

def zheng_2025_SC_d_distance_upper : Nat

defzheng_2025_parallel_logicals_factor

def zheng_2025_parallel_logicals_factor : Nat

High-rate surgery measures up to t ≈ k logicals in parallel per round.

defcross_2025_gross_ancilla_qubits

def cross_2025_gross_ancilla_qubits : Nat

For [[144, 12, 12]] Gross code: 103 ancilla qubits, 288 PPMs total.

defcross_2025_gross_total_PPMs

def cross_2025_gross_total_PPMs : Nat

defcross_2025_ancilla_per_weight

def cross_2025_ancilla_per_weight : Nat

Asymptotic ancilla cost: Θ(w) for measuring weight-w logical operator.

defpanteleev_2021_dimension_exponent_numerator

def panteleev_2021_dimension_exponent_numerator   : Nat

LP code dimension and distance scaling parameters (Theorems 1, 2): For α ∈ (0,1): dimension Ω(N^α log N), distance Ω(N^{1-α/2} log N).

defpanteleev_2021_dimension_exponent_denominator

def panteleev_2021_dimension_exponent_denominator : Nat

defpanteleev_2021_distance_exponent_numerator

def panteleev_2021_distance_exponent_numerator    : Nat

defpanteleev_2021_distance_exponent_denominator

def panteleev_2021_distance_exponent_denominator  : Nat

defpanteleev_2021_lp_3_7_distance_upper

def panteleev_2021_lp_3_7_distance_upper : Nat

LP code distance upper bound: d ≤ min((r_A+1)!, (n_A+1)!). For r_A=3, n_A=7 (qianxu's lp_*^{3,7}): d ≤ min(24, 40320) = 24.

defgu_xu_2026_CC1_n_qubits

def gu_xu_2026_CC1_n_qubits  : Nat

Clustered-cyclic codes presented: [[136, 8, 14]] and [[198, 18, 10]].

defgu_xu_2026_CC1_k_logical

def gu_xu_2026_CC1_k_logical : Nat

defgu_xu_2026_CC1_d_distance

def gu_xu_2026_CC1_d_distance : Nat

defgu_xu_2026_CC2_n_qubits

def gu_xu_2026_CC2_n_qubits  : Nat

defgu_xu_2026_CC2_k_logical

def gu_xu_2026_CC2_k_logical : Nat

defgu_xu_2026_CC2_d_distance

def gu_xu_2026_CC2_d_distance : Nat

defgu_xu_2026_parallel_PPMs_per_round_denominator

def gu_xu_2026_parallel_PPMs_per_round_denominator : Nat

Up to ⌊k/2⌋ disjoint Pauli-product measurements per surgery round.

defpeng_2022_shor_circuit_n_squared_coeff

def peng_2022_shor_circuit_n_squared_coeff   : Nat

SQIR's certified gate-count bound for Shor's algorithm (`SQIR/examples/shor/ResourceShor.v` line 788, lemma `ugcount_shor_circuit`): ugcount(shor_circuit a N) ≤ (212·n² + 975·n + 1031)·m + 4·m + m² where m = log₂(2 N²), n = log₂(2 N). Coefficients stored individually.

defpeng_2022_shor_circuit_n_coeff

def peng_2022_shor_circuit_n_coeff           : Nat

defpeng_2022_shor_circuit_constant_coeff

def peng_2022_shor_circuit_constant_coeff    : Nat

defpeng_2022_shor_circuit_4m_coeff

def peng_2022_shor_circuit_4m_coeff          : Nat

defpeng_2022_shor_circuit_m_squared_coeff

def peng_2022_shor_circuit_m_squared_coeff   : Nat

defpeng_2022_textbook_toffoli_tcount

def peng_2022_textbook_toffoli_tcount : Nat

Per-Toffoli T-count under SQIR's textbook decomposition: 7.

defpeng_2022_cuccaro_MAJ_gate_count_upper

def peng_2022_cuccaro_MAJ_gate_count_upper : Nat

Per-Cuccaro-MAJ gate count (SQIR `bcgcount_MAJ` ≤ 3): 3.

defpeng_2022_cuccaro_adder_gate_count_per_bit

def peng_2022_cuccaro_adder_gate_count_per_bit : Nat

Per-Cuccaro-adder gate count (SQIR `bcgcount_adder01` ≤ 6n): 6n. Coefficient.

defpeng_2022_modmult_rev_n_squared_coeff

def peng_2022_modmult_rev_n_squared_coeff : Nat

Per-modmult-rev gate count (SQIR `bcgcount_modmult_rev` ≤ 212n² + 943n + 967). Quadratic coefficient.

defpeng_2022_modmult_rev_n_coeff

def peng_2022_modmult_rev_n_coeff         : Nat

defpeng_2022_modmult_rev_constant_coeff

def peng_2022_modmult_rev_constant_coeff  : Nat

defpeng_2022_success_prob_kappa_permille

def peng_2022_success_prob_kappa_permille : Nat

Success probability of a single Shor round: ≥ 4·e⁻²/π² · (log₂ N)⁻⁴ ≈ 0.055 / (log₂ N)⁴. We record the numerator as a per-mille approximation (55 / 1000).

defgidney_ekera_2021_rsa2048_physical_qubits

def gidney_ekera_2021_rsa2048_physical_qubits : Nat

G-Ek 2021 RSA-2048 physical qubit count: 20 million. Source: Gidney–Ekerå 2021 (canonical headline).

defgidney_ekera_2021_rsa2048_wallclock_hours

def gidney_ekera_2021_rsa2048_wallclock_hours : Nat

G-Ek 2021 RSA-2048 wallclock estimate: 8 hours.

defgidney_ekera_2021_rsa2048_qubit_hours

def gidney_ekera_2021_rsa2048_qubit_hours : Nat

G-Ek 2021 qubit × time product (the standard cost metric): 20M qubits × 8h = 160M qubit·hours.

defqianxu_2026_rsa2048_physical_qubits

def qianxu_2026_rsa2048_physical_qubits : Nat

qianxu 2026 RSA-2048 physical qubit count: ~10,000.

defqianxu_2026_rsa2048_wallclock_hours

def qianxu_2026_rsa2048_wallclock_hours : Nat

qianxu 2026 RSA-2048 wallclock: ~1 week = 168 hours.

defqianxu_2026_rsa2048_qubit_hours

def qianxu_2026_rsa2048_qubit_hours : Nat

qianxu 2026 qubit·time product: 10K qubits × 168h = 1.68M qubit·hours.

example(example)

example : gidney_ekera_2021_rsa2048_qubit_hours = 160_000_000

G-Ek's qubit·time product is 160 million qubit·hours.

example(example)

example : qianxu_2026_rsa2048_qubit_hours = 1_680_000

qianxu's qubit·time product is 1.68 million qubit·hours.

theoremqianxu_qubit_hours_95x_lower_than_gidney_ekera

theorem qianxu_qubit_hours_95x_lower_than_gidney_ekera :
    95 * qianxu_2026_rsa2048_qubit_hours
      ≤ gidney_ekera_2021_rsa2048_qubit_hours

*Headline G-S finding**: qianxu's qubit·time product is at least 95× smaller than Gidney–Ekerå 2021 (i.e., 95 × qianxu ≤ G-Ek).

example(example)

example : (gidney_ekera_2021_rsa2048_qubit_hours * 1000)
            / qianxu_2026_rsa2048_qubit_hours = 95238

The exact ratio: 95.238... (encoded as G-Ek/qianxu × 1000 = 95238).

example(example)

example : qianxu_E10_tau_Toff_RSA_se_tau_s = 43

example(example)

example : babbush_ECC256_lowqubit_toffolis = 90000000

example(example)

example : peng_2022_shor_circuit_n_squared_coeff = 212

example(example)

example : qianxu_per_toffoli_adder_se_tau_s = 25

example(example)

example : qianxu_per_toffoli_lookup_se_tau_s = 71

example(example)

example :
    (qianxu_per_toffoli_adder_se_tau_s + qianxu_per_toffoli_lookup_se_tau_s) / 2
      ≠ qianxu_E10_tau_Toff_RSA_se_tau_s

The E10 LHS recomputed against the now-explicit E3 and E9 anchors: `0.5·adder + 0.5·lookup = (25 + 71) / 2 = 48`, not the claimed 43. Decide-checked. The full attribution lives in `lean/FormalRV/G_A.lean`; this lemma just re-binds the discrepancy to the named paper-claim constants for clarity.

defqianxu_q_A_RSA2048

def qianxu_q_A_RSA2048 : Nat

*q_A for RSA-2048**, the maximum adder size in the RSA-2048 Shor's circuit. Source: qianxu p. 22 ("we use q_A/k_add computation units ... with k_add = ⌊(k_p - 1)/3⌋"); for k_p = 10, k_add = 3, and the max adder is 33 bits (= 99 / 3 = 33 wide).

defgidney_adder_RSA2048_T_count_verified

def gidney_adder_RSA2048_T_count_verified : Nat

*Verified-tier T-count for RSA-2048 adder** (Iter 263 anchor). `14 × q_A = 462 T-gates per adder use`, derived from the verified parametric theorem `tcount_gidney_adder_full_faithful_no_measurement` (Iter 88 + Iter 213's semantic correctness).

example(example)

example : gidney_adder_RSA2048_T_count_verified = 462

defunary_lookup_iteration_RSA2048_T_count_verified

def unary_lookup_iteration_RSA2048_T_count_verified : Nat

*Verified-tier T-count for one RSA-2048 lookup iteration** (Iter 263 anchor). `14 × q_a = 84 T-gates per iter`, derived from Iter 14's `tcount_unary_lookup_iteration` + Iter 241's semantic correctness.

example(example)

example : unary_lookup_iteration_RSA2048_T_count_verified = 84

defunary_lookup_multi_RSA2048_no_meas_T_count_verified

def unary_lookup_multi_RSA2048_no_meas_T_count_verified : Nat

*Verified-tier T-count for the full no-measurement RSA-2048 lookup** (Iter 263 anchor). `14 × q_a × 2^q_a = 5376 T-gates total`, derived from Iter 14's `tcount_unary_lookup_multi_iteration` + Iter 257's semantic correctness. This is the **upper bound** without Gidney measurement trick + Gray-code amortization.

example(example)

example : unary_lookup_multi_RSA2048_no_meas_T_count_verified = 5376

FormalRV.Framework.ResourceBounds

FormalRV/Framework/ResourceBounds.lean

FormalRV.Framework.ResourceBounds — a GENERAL, reusable framework for auditing a paper's resource estimate by BRACKETING it between a verified LOWER bound (irreducible: data block / critical path) and a verified naive-construction UPPER bound, and quantifying the optimization GAP the paper claims over the naive build. This is the framework-level generalisation of the project's "naive upper bound + gap" pattern (System/NaiveUpperBound, Corpus/GidneyEkera2021Reproduction): a single `ResourceBounds` carries (lower, upper, reported), with decidable soundness / bracketing checks and the gap, applicable to ANY resource (qubits, time) of ANY paper. The honest reading: • lower ≤ reported : the paper respects the irreducible floor (else suspicious); • reported ≤ upper : the paper is at least as efficient as our naive build; • upper − reported : the optimization the paper claims but we did NOT construct (the GAP). No Mathlib. No `sorry`, no `axiom`.

structureResourceBounds

structure ResourceBounds

A resource bound: an irreducible LOWER bound, a naive-construction UPPER bound, and the paper's REPORTED figure.

defsound

def sound (b : ResourceBounds) : Bool

The bounds are SOUND: the lower bound does not exceed the naive upper bound.

defrespectsFloor

def respectsFloor (b : ResourceBounds) : Bool

The paper respects the irreducible floor (its claim is ≥ our lower bound).

defwithinNaive

def withinNaive (b : ResourceBounds) : Bool

The paper is within our naive upper bound (at least as efficient).

defbracketed

def bracketed (b : ResourceBounds) : Bool

The reported figure is BRACKETED: floor ≤ reported ≤ naive upper.

defoptimizationGap

def optimizationGap (b : ResourceBounds) : Nat

The optimization GAP: how much the paper saves vs the naive construction.

theorembracketed_sound

theorem bracketed_sound (b : ResourceBounds) (h : b.bracketed = true) : b.sound = true

A bracketed estimate is sound (lower ≤ upper), since lower ≤ reported ≤ upper.

theorembracketed_iff

theorem bracketed_iff (b : ResourceBounds) :
    b.bracketed = true ↔ (b.lower ≤ b.reported ∧ b.reported ≤ b.upper)

Bracketing splits into the two one-sided facts.

theoremreported_add_gap

theorem reported_add_gap (b : ResourceBounds) (h : b.withinNaive = true) :
    b.reported + b.optimizationGap = b.upper

If bracketed, the reported figure plus the optimization gap recovers the naive upper bound — the gap is exactly the unconstructed optimization.

FormalRV.Framework.ResourceEstimate

FormalRV/Framework/ResourceEstimate.lean

FormalRV.Framework.ResourceEstimate — the GENERAL parametric resource model. The Xiaodi reframe (`memory/feedback_framework_not_gotcha.md`): we do NOT re-derive any single paper's headline number from first principles, and we do NOT try to prove a paper's estimate is optimal. Instead we build ONE GENERAL, parametric resource-estimate FUNCTION — the same for every corpus paper — and let the reviewer plug in their own inputs. The inputs split into three classes: • HARDWARE — measured device parameters (the QEC code-cycle time). USER-SET. Different per platform (superconducting, neutral atom), never derived by us. • WORKLOAD — the algorithm's demand: #Toffoli of the logical Clifford+Toffoli circuit and its #logical qubits. A function of the problem (RSA-2048, ECC-256); supplied per instance from the L1/L2 layers. • ARCHITECTURE — the compilation method's per-operation cost + footprint: + ASSUMPTIONS code-cycles per logical Toffoli, physical qubits per logical, routing/ancilla footprint, magic-factory footprint. These are the mathematically-UNVERIFIABLE inputs (Type A hardware + Type B method assumptions, see `memory/feedback_type_AB_assumptions.md`): the framework does NOT derive them — the paper/user supplies and justifies them by their own analysis. The framework's job is the *verified derivation* (the composition): time = n_toff · tau_toff · t_cycle (critical path) qubits = n_logical · phys_per_logical + ancilla + factory i.e. "we verify that Shor takes time T with Q qubits ON THEIR hardware and architecture, mathematically." The composition is the theorem; the inputs are the reviewer's to plug in. Monotonicity lemmas (§3) make the sensitivity analysis mechanical: varying an input moves the output in the proven direction. General across all seven corpus papers — see the corpus instantiations under `Corpus/` and the verified upper-bound + gap analysis in `System/NaiveUpperBound.lean`. No Mathlib. Pure Nat / Bool. No `sorry`, no `axiom`.

structureHardware

structure Hardware

HARDWARE (user-set, measured): the QEC code-cycle time, in 1/10 μs units (matching `QualtranPhysicalParameters.cycle_time_us_tenths`; 10 ↔ 1 μs).

structureWorkload

structure Workload

WORKLOAD (the algorithm's demand): the Toffoli count and logical-qubit footprint of the logical Clifford+Toffoli circuit. A function of the problem size, supplied from the L1 (algorithm) / L2 (gadget) layers.

structureArchitecture

structure Architecture

ARCHITECTURE + ASSUMPTIONS (method + hardware-derived; NOT verified by the framework — the user/paper supplies and justifies these): • `tau_toff_cycles` : code-cycles to execute one logical Toffoli (lattice-surgery / magic-factory method-dependent). • `phys_per_logical` : physical qubits per logical qubit (code-dependent: 2(d+1)² for a surface patch, ⌈n/k⌉ for a qLDPC block). • `ancilla_qubits` : routing / operation-zone ancilla footprint. • `factory_qubits` : magic-state factory footprint.

structureResourceEstimate

structure ResourceEstimate

The DERIVED estimate: wallclock (1/10 μs units) + total physical qubits.

deftotalCycles

def totalCycles (w : Workload) (a : Architecture) : Nat

Total code-cycles on the sequential critical path: one Toffoli at a time.

deftotalTime

def totalTime (hw : Hardware) (w : Workload) (a : Architecture) : Nat

Total wallclock (1/10 μs units) = cycles × cycle-time.

deftotalQubits

def totalQubits (w : Workload) (a : Architecture) : Nat

Total physical qubits = data + routing/ancilla + factory.

defestimate

def estimate (hw : Hardware) (w : Workload) (a : Architecture) : ResourceEstimate

THE GENERAL RESOURCE ESTIMATE: the same function for every corpus paper.

theoremestimate_time

theorem estimate_time (hw : Hardware) (w : Workload) (a : Architecture) :
    (estimate hw w a).time_us_tenths
      = w.n_toff * a.tau_toff_cycles * hw.cycle_time_us_tenths

"Resource count follows": the wallclock is exactly the composition.

theoremestimate_qubits

theorem estimate_qubits (hw : Hardware) (w : Workload) (a : Architecture) :
    (estimate hw w a).qubits
      = w.n_logical * a.phys_per_logical + a.ancilla_qubits + a.factory_qubits

"Resource count follows": the qubit count is exactly the composition.

theoremtime_mono_cycle

theorem time_mono_cycle (w : Workload) (a : Architecture) {hw hw' : Hardware}
    (h : hw.cycle_time_us_tenths ≤ hw'.cycle_time_us_tenths) :
    (estimate hw w a).time_us_tenths ≤ (estimate hw' w a).time_us_tenths

Slower cycle time ⇒ at least as much wallclock (all else equal).

theoremtime_mono_toff

theorem time_mono_toff (hw : Hardware) (a : Architecture) {w w' : Workload}
    (h : w.n_toff ≤ w'.n_toff) :
    (estimate hw w a).time_us_tenths ≤ (estimate hw w' a).time_us_tenths

More Toffolis ⇒ at least as much wallclock (all else equal).

theoremtime_mono_tau

theorem time_mono_tau (hw : Hardware) (w : Workload) {a a' : Architecture}
    (h : a.tau_toff_cycles ≤ a'.tau_toff_cycles) :
    (estimate hw w a).time_us_tenths ≤ (estimate hw w a').time_us_tenths

More expensive Toffolis (more cycles each) ⇒ at least as much wallclock.

theoremqubits_mono_logical

theorem qubits_mono_logical (hw : Hardware) (a : Architecture) {w w' : Workload}
    (h : w.n_logical ≤ w'.n_logical) :
    (estimate hw w a).qubits ≤ (estimate hw w' a).qubits

More logical qubits ⇒ at least as many physical qubits (all else equal).

theoremqubits_mono_phys

theorem qubits_mono_phys (hw : Hardware) (w : Workload) {a a' : Architecture}
    (hp : a.phys_per_logical ≤ a'.phys_per_logical)
    (ha : a.ancilla_qubits = a'.ancilla_qubits)
    (hf : a.factory_qubits = a'.factory_qubits) :
    (estimate hw w a).qubits ≤ (estimate hw w a').qubits

A larger per-logical physical footprint ⇒ at least as many physical qubits.

defHardware.ofQualtran

def Hardware.ofQualtran (q : QualtranPhysicalParameters) : Hardware

Read the hardware cycle time straight from a Qualtran physical-parameter record (so a corpus instance's `QualtranPhysicalParameters` drives the estimate directly).

defphysPerLogical

def physPerLogical (c : QECCode) : Nat

Standard physical-qubits-per-logical read off a code: `⌈n/k⌉` for a qLDPC block packing `k` logicals into `n` physical qubits; `n` itself when `k = 0` (degenerate) or `k = 1` (a single-logical surface patch, where `n = 2(d+1)²`).

example(example)

example : physPerLogical { n

Smoke: surface patch (k = 1) gives the whole patch per logical.

example(example)

example : physPerLogical { n

Smoke: a qLDPC block [[5278, 1480, 24]] (qianxu lp_24) packs ≈ ⌈5278/1480⌉ = 4 physical per logical.

deftoyHW

def toyHW : Hardware

Toy hardware: 1 μs cycle.

deftoyWork

def toyWork : Workload

Toy workload: 100 Toffolis over 4 logical qubits.

deftoyArch

def toyArch : Architecture

Toy architecture: 13 cycles/Toffoli, 1568 physical/logical, 900 ancilla, 2565 factory (qianxu-ish numbers, but at a toy 100-Toffoli scale).

example(example)

example : (estimate toyHW toyWork toyArch).qubits = 9737

The composition fires: 4·1568 + 900 + 2565 = 9737 qubits.

example(example)

example : (estimate toyHW toyWork toyArch).time_us_tenths = 13000

The composition fires: 100·13·10 = 13000 tenths-μs = 1300 μs.