FormalRV

Resource 141 declarations in 10 modules

FormalRV.Resource.Examples

FormalRV/Resource/Examples.lean
FormalRV.Resource.Examples ────────────────────────── Worked demonstrations of the resource-counting TRIPLE on a concrete gadget: (1) a syntactic object, (2) its semantic-correctness theorem, (3) the independent counters applied to THAT object = the closed form. Contains `#eval` demos, so kept OFF the default build path. Run on demand: lake build FormalRV.Resource.Examples
example(example)
example (n : Nat) : countT (cuccaro_n_bit_adder_full n 0) = 14 * n
(3) **The count is the closed form, on the same object** — via the bridge to the gadget's existing resource theorem. This is the third leg of the triple: the independent `countT` walk of `cuccaro_n_bit_adder_full n 0` equals `14·n`.
example(example)
example (n : Nat) :
    countT (cuccaro_n_bit_adder_full n 0)
      = 7 * countToffoli (cuccaro_n_bit_adder_full n 0)
And `countT` is exactly `7 ×` the (independently-counted) Toffolis — two counters reconciled on the same tree.

FormalRV.Resource.GateCount

FormalRV/Resource/GateCount.lean
FormalRV.Resource.GateCount ─────────────────────────── The canonical, INDEPENDENT resource counters for the reversible `Gate` IR. ## The separation discipline (why this folder exists) A resource counter is an HONEST recursive tree-walk over a syntactic object — nothing else. This module imports ONLY the IR (`Core.Gate`); it knows nothing about how a circuit is *built* (the gadget constructors) or *proved correct* (the semantics). Because the counters live in their own world, a resource theorem `countT (gadget n) = 14·n` CANNOT fudge the count — the number is forced by the syntax tree, and a skeptic can `#eval` the counter on a constructed circuit to check it WITHOUT reading any proof. Resource verification then has the shape John requires: a concrete syntactic object (or a generator that builds it), a proof it is semantically correct, and a proof that THESE counters applied to THAT object equal the closed form. `countT` agrees with the legacy `Gate.tcount` (bridge `countT_eq_tcount`), so existing resource theorems interoperate; new per-gate counters (`countCNOT`, `countToffoli`, `countX`) are added here.
defcountT
def countT : Gate → Nat
  | .I         => 0
  | .X _       => 0
  | .CX _ _    => 0
  | .CCX _ _ _ => 7
  | .seq a b   => countT a + countT b
*T-count.** 7 per Toffoli (textbook decomposition); Cliffords and identity are T-free. Sums over `seq`.
defcountCNOT
def countCNOT : Gate → Nat
  | .CX _ _    => 1
  | .seq a b   => countCNOT a + countCNOT b
  | _          => 0
*CNOT count.**
defcountToffoli
def countToffoli : Gate → Nat
  | .CCX _ _ _ => 1
  | .seq a b   => countToffoli a + countToffoli b
  | _          => 0
*Toffoli (CCX) count.**
defcountX
def countX : Gate → Nat
  | .X _       => 1
  | .seq a b   => countX a + countX b
  | _          => 0
*X (NOT) count.**
defgateCount
def gateCount : Gate → Nat
  | .I         => 0
  | .X _       => 1
  | .CX _ _    => 1
  | .CCX _ _ _ => 1
  | .seq a b   => gateCount a + gateCount b
*Total gate count** (identity is free).
defdepth
def depth : Gate → Nat
  | .I         => 0
  | .X _       => 1
  | .CX _ _    => 1
  | .CCX _ _ _ => 1
  | .seq a b   => depth a + depth b
*Sequential depth** (a TIME resource).
defwidth
def width : Gate → Nat
  | .I         => 0
  | .X q       => q + 1
  | .CX c t    => max (c + 1) (t + 1)
  | .CCX a b c => max (max (a + 1) (b + 1)) (c + 1)
  | .seq a b   => max (width a) (width b)
*Qubit count (register width).** The largest qubit index the circuit touches, plus one — the size of the register the machine must allocate. (Gate-IR gadgets use dense `0..w-1` indexing, so this is the qubit count.) This is the SPACE resource, dual to the gate counts (TIME).
theoremcountT_eq_seven_countToffoli
theorem countT_eq_seven_countToffoli (g : Gate) :
    countT g = 7 * countToffoli g
example(example)
example : countT (.CCX 0 1 2) = 7
example(example)
example : countCNOT (.seq (.CX 0 1) (.CX 1 2)) = 2
example(example)
example : countToffoli (.seq (.CCX 0 1 2) (.CCX 1 2 3)) = 2
example(example)
example : gateCount (.seq (.X 0) (.CCX 0 1 2)) = 2
example(example)
example : countT (.seq (.CCX 0 1 2) (.CCX 0 1 2)) = 7 * countToffoli (.seq (.CCX 0 1 2) (.CCX 0 1 2))
example(example)
example : width (.CCX 0 1 2) = 3
example(example)
example : width (.seq (.X 0) (.CX 1 2)) = 3

FormalRV.Resource.Interface

FormalRV/Resource/Interface.lean
FormalRV.Resource.Interface ─────────────────────────── The unified, IR-agnostic resource-counting interface. Every circuit IR in the project (`Gate`, `BaseUCom`, and — to be migrated — the PPM / lattice-surgery IRs) exposes the SAME two honest counters through one typeclass: a CNOT count and a total gate count. IR-specific counters that have no cross-IR meaning stay in their own module (`countT`/`countToffoli` on the reversible `Gate` IR; `oneQCountU` on the unitary `BaseUCom` IR). This is the single, separate "resource system": it depends only on the IRs, never on the circuit builders or the correctness proofs, so a count cannot be influenced by a proof.
classHasResourceCount
class HasResourceCount (α : Type _)
An IR whose syntactic objects carry honest resource counters, split into the two physical resources: TIME (gate counts) and SPACE (qubit count).
instanceHasResourceCount
instance : HasResourceCount Gate
The reversible `Gate` IR.
instancedim
instance {dim : Nat} : HasResourceCount (BaseUCom dim)
The unitary `BaseUCom` IR.
example(example)
example : HasResourceCount.gates  (Gate.CCX 0 1 2) = 1
example(example)
example : HasResourceCount.qubits (Gate.CCX 0 1 2) = 3
example(example)
example : HasResourceCount.cnot (Gate.seq (Gate.CX 0 1) (Gate.CX 1 2)) = 2
example(example)
example {dim} (c t : Nat) :
    HasResourceCount.cnot (BaseUCom.CNOT c t : BaseUCom dim) = 1

FormalRV.Resource.PPMCount

FormalRV/Resource/PPMCount.lean
FormalRV.Resource.PPMCount ────────────────────────── The canonical, INDEPENDENT resource counters for the PPM program IR (`PPM/Syntax/Program.lean` — John's `c2 = Measure X[0]Z[1]X[3]` / `if c2 == 1 then …` syntax). Same discipline as the rest of `Resource/`: this file imports ONLY the leaf IR (which itself imports nothing), never a semantics, compiler, or gadget builder — so a count theorem `countMeas (compilePPM g) = n` cannot fudge the count; the number is forced by the program's syntax tree, and a skeptic can `#eval` the counters on any constructed program without reading a proof. TIME counters: measurements, corrections (statements and worst-case fired frame ops), magic-state consumption (T / CCZ). SPACE: the IR's own `PPMProg.width` (qubits) and `PPMProg.cwidth` (classical outcome slots) are re-exposed through the same interface.
defcountMeasS
def countMeasS : PPMStmt → Nat
  | .measure ..     => 1
  | .measureSel ..  => 1
  | .measureSel2 .. => 1
  | _               => 0
Pauli-product measurements (the dominant PPM cost unit).
defcountCorrectS
def countCorrectS : PPMStmt → Nat
  | .correct ..  => 1
  | .correctQ .. => 1
  | _            => 0
Conditional-correction statements.
defcountMagicTS
def countMagicTS : PPMStmt → Nat
  | .useT _ => 1
  | _       => 0
T magic states consumed.
defcountMagicCCZS
def countMagicCCZS : PPMStmt → Nat
  | .useCCZ .. => 1
  | _          => 0
CCZ magic states consumed.
defcountMeas
def countMeas : PPMProg → Nat
  | []     => 0
  | s :: p => countMeasS s + countMeas p
*Measurement count** of a PPM program.
defcountCorrect
def countCorrect : PPMProg → Nat
  | []     => 0
  | s :: p => countCorrectS s + countCorrect p
*Correction-statement count** of a PPM program.
defcountMagicT
def countMagicT : PPMProg → Nat
  | []     => 0
  | s :: p => countMagicTS s + countMagicT p
*T-magic count** of a PPM program.
defcountMagicCCZ
def countMagicCCZ : PPMProg → Nat
  | []     => 0
  | s :: p => countMagicCCZS s + countMagicCCZ p
*CCZ-magic count** of a PPM program.
defcountMagic
def countMagic (p : PPMProg) : Nat
*Total magic count** (T + CCZ).
theoremcountMeas_append
theorem countMeas_append (p q : PPMProg) :
    countMeas (p ++ q) = countMeas p + countMeas q
theoremcountCorrect_append
theorem countCorrect_append (p q : PPMProg) :
    countCorrect (p ++ q) = countCorrect p + countCorrect q
theoremcountMagicT_append
theorem countMagicT_append (p q : PPMProg) :
    countMagicT (p ++ q) = countMagicT p + countMagicT q
theoremcountMagicCCZ_append
theorem countMagicCCZ_append (p q : PPMProg) :
    countMagicCCZ (p ++ q) = countMagicCCZ p + countMagicCCZ q
theoremcountMagic_append
theorem countMagic_append (p q : PPMProg) :
    countMagic (p ++ q) = countMagic p + countMagic q
theoremcwidth_eq_countMeas
theorem cwidth_eq_countMeas (p : PPMProg) :
    PPMProg.cwidth p = countMeas p
The classical width IS the measurement count (each measurement binds exactly one outcome slot) — two independent walks reconciled.
example(example)
example :
    countMeas [.useT 1, .measure 0 [⟨0, .z⟩, ⟨1, .z⟩],
               .correct [0] [⟨1, .x⟩] []] = 1
example(example)
example :
    countMagicT [.useT 1, .measure 0 [⟨0, .z⟩], .useT 0] = 2
example(example)
example :
    countCorrect [.measure 0 [⟨0, .z⟩], .correct [0] [⟨1, .x⟩] [],
                  .correct [0] [⟨0, .z⟩] [⟨1, .z⟩]] = 2

FormalRV.Resource.QECCircuitCount

FormalRV/Resource/QECCircuitCount.lean
FormalRV.Resource.QECCircuitCount — canonical independent counters for the QEC-layer physical-circuit IR (`FormalRV.QEC.Circuit.PhysCircuit`). ## Discipline (see FormalRV/Resource/README.md) Counters are honest tree-walks importing ONLY the circuit IR — never gadget constructors or correctness proofs — so `counter(object) = formula` theorems cannot be fudged and a skeptic can `#eval` the counter on the constructed object. The per-gadget count theorems (e.g. that the compiled syndrome- extraction circuit of a surgery gadget has width `surgeryPhysQubits g`) live with the gadgets, in `FormalRV/QEC/Circuit/ExtractionCount.lean`. ## TIME vs SPACE TIME : `cxCountC` (two-qubit gates), `measCountC`, `prepCountC`, `opCountC` (total ops = sequential-depth upper bound, one op per step — the IR is a flat sequential list; logical-cycle time is the `FormalRV/QEC/Time/LogicalCycle.lean` algebra, not a gate count). SPACE: `widthC` — max touched virtual-qubit index + 1. Because syndrome and surgery ancillas are explicit indices in the syntax tree, they are counted; this is the layer at which "hidden" QEC overhead becomes visible to a skeptic. No Mathlib. No `sorry`, no `axiom`.
defcxCountC
def cxCountC (c : PhysCircuit) : Nat
Number of CNOTs.
defmeasCountC
def measCountC (c : PhysCircuit) : Nat
Number of measurements.
defprepCountC
def prepCountC (c : PhysCircuit) : Nat
Number of basis preparations (resets).
defopCountC
def opCountC (c : PhysCircuit) : Nat
Total operation count (= sequential-step upper bound).
theoremcxCountC_append
theorem cxCountC_append (c d : PhysCircuit) :
    cxCountC (c ++ d) = cxCountC c + cxCountC d
theoremmeasCountC_append
theorem measCountC_append (c d : PhysCircuit) :
    measCountC (c ++ d) = measCountC c + measCountC d
theoremprepCountC_append
theorem prepCountC_append (c d : PhysCircuit) :
    prepCountC (c ++ d) = prepCountC c + prepCountC d
theoremopCountC_append
theorem opCountC_append (c d : PhysCircuit) :
    opCountC (c ++ d) = opCountC c + opCountC d
theoremopCountC_eq_parts
theorem opCountC_eq_parts (c : PhysCircuit) :
    opCountC c = prepCountC c + cxCountC c + measCountC c
Counter reconciliation: every operation is exactly one of prep/CX/meas.
defopWidth
def opWidth : PhysOp → Nat
  | .prep _ q => q + 1
  | .cx c t   => max c t + 1
  | .meas _ q => q + 1
Footprint of one operation: max touched index + 1.
defwidthC
def widthC (c : PhysCircuit) : Nat
Register width: max touched virtual-qubit index + 1 (0 for the empty circuit). Dense `0..w−1` indexing assumed, as for `Resource.width` on the `Gate` IR.
theoremwidthC_append
theorem widthC_append (c d : PhysCircuit) :
    widthC (c ++ d) = max (widthC c) (widthC d)
Width of a concatenation is the max of the widths (space is shared, not added — virtual qubits are reused by index, never double-counted).
defancillaOpQubit
def ancillaOpQubit : PhysOp → Option Nat
  | .prep _ q => some q
  | .meas _ q => some q
  | .cx _ _   => none
The qubit a prep/meas op acts on (ancilla activity); `none` for `cx`.
defancillaQubits
def ancillaQubits (c : PhysCircuit) : List Nat
The distinct ANCILLA qubits of a circuit: those prepped or measured.
defdataQubits
def dataQubits (c : PhysCircuit) : List Nat
The distinct DATA qubits: CX endpoints that are never prepped/measured.
defnumAncillaQubits
def numAncillaQubits (c : PhysCircuit) : Nat
*Number of ANCILLA qubits used** (independent walk of the circuit).
defnumDataQubits
def numDataQubits (c : PhysCircuit) : Nat
*Number of DATA qubits used** (independent walk of the circuit).
defnumPhysQubits
def numPhysQubits (c : PhysCircuit) : Nat
*Total distinct physical qubits used** = data + ancilla (no double counting — data and ancilla qubit-sets are disjoint by definition: a data qubit is never prepped/measured, an ancilla qubit always is).
theoremdata_ancilla_disjoint
theorem data_ancilla_disjoint (c : PhysCircuit) (q : Nat)
    (hd : q ∈ dataQubits c) : q ∉ ancillaQubits c
Data and ancilla qubit sets are DISJOINT (the split is well-defined).
instanceHasResourceCount
instance : HasResourceCount FormalRV.QEC.Circuit.PhysCircuit

FormalRV.Resource.RotationCount

FormalRV/Resource/RotationCount.lean
FormalRV.Resource.RotationCount ─────────────────────────────── The canonical, INDEPENDENT resource counters for the Pauli-rotation IR (`PauliRotation/Syntax.lean` — the Litinski layer between circuits and PPM). Same discipline as the rest of `Resource/`: imports ONLY the leaf IR, never a semantics, compiler, or gadget builder, so a count theorem cannot fudge — the number is forced by the program's syntax tree, and a skeptic can `#eval` the counters on any constructed rotation program without reading a proof. TIME readouts: • `countPi8` — π/8 (T-level) rotations: THE T-count of the program (the only non-Clifford angle). • `countAngle` — rotations at any given angle level. • `countRot` — all rotations. • `depth` — number of parallel layers: the PARALLEL logical depth (the whole point of the layer structure — grouped commuting rotations cost ONE time step, not many). SPACE: the IR's own `RotProg.width` (logical data qubits; this layer has no ancillas) is the space readout.
defcountAngleL
def countAngleL (a : RAngle) (L : RotLayer) : Nat
Rotations at angle `a` in one layer.
defcountRotL
def countRotL (L : RotLayer) : Nat
All rotations in one layer.
defcountAngle
def countAngle (a : RAngle) : RotProg → Nat
  | []     => 0
  | L :: p => countAngleL a L + countAngle a p
*Rotations at angle `a`** in a program.
defcountPi8
def countPi8 (p : RotProg) : Nat
*The T-count**: π/8 rotations are the only non-Clifford content.
defcountRot
def countRot : RotProg → Nat
  | []     => 0
  | L :: p => countRotL L + countRot p
*Total rotation count.**
defrotDepth
def rotDepth (p : RotProg) : Nat
*Parallel logical depth**: each layer of pairwise-commuting rotations is one parallel time step.
theoremcountAngle_append
theorem countAngle_append (a : RAngle) (p q : RotProg) :
    countAngle a (p ++ q) = countAngle a p + countAngle a q
theoremcountPi8_append
theorem countPi8_append (p q : RotProg) :
    countPi8 (p ++ q) = countPi8 p + countPi8 q
theoremcountRot_append
theorem countRot_append (p q : RotProg) :
    countRot (p ++ q) = countRot p + countRot q
theoremrotDepth_append
theorem rotDepth_append (p q : RotProg) :
    rotDepth (p ++ q) = rotDepth p + rotDepth q
theoremcountAngleL_partition
private theorem countAngleL_partition (L : RotLayer) :
    countAngleL .pi L + countAngleL .piHalf L
      + countAngleL .piQuarter L + countAngleL .piEighth L = countRotL L
theoremcountRot_eq_angle_partition
theorem countRot_eq_angle_partition (p : RotProg) :
    countAngle .pi p + countAngle .piHalf p
      + countAngle .piQuarter p + countAngle .piEighth p = countRot p
example(example)
example :  -- one layer of two parallel T's + one Clifford layer: T-count 2, depth 2
    countPi8 [[⟨false, .piEighth, [⟨0, .z⟩]⟩, ⟨false, .piEighth, [⟨1, .z⟩]⟩],
              [⟨true, .piQuarter, [⟨0, .z⟩, ⟨1, .x⟩]⟩]] = 2
example(example)
example :
    rotDepth [[⟨false, .piEighth, [⟨0, .z⟩]⟩, ⟨false, .piEighth, [⟨1, .z⟩]⟩],
           [⟨true, .piQuarter, [⟨0, .z⟩, ⟨1, .x⟩]⟩]] = 2
example(example)
example :
    countRot [[⟨false, .piEighth, [⟨0, .z⟩]⟩, ⟨false, .piEighth, [⟨1, .z⟩]⟩],
              [⟨true, .piQuarter, [⟨0, .z⟩, ⟨1, .x⟩]⟩]] = 3

FormalRV.Resource.SysCallCount

FormalRV/Resource/SysCallCount.lean
FormalRV.Resource.SysCallCount — THE system-level (SysCall) resource counters. ## Contract (the folder's design principle, enforced here for L4) These are honest tree-walks over the concrete syntactic object `List SysCall` and NOTHING else: no architecture, no checkers, no proofs. **Every verifier, certificate, or theorem that claims a system-level resource (time, op counts, qubit footprint, peak occupancy, syndrome volume) must call THESE functions — never redefine its own.** A skeptic can `#eval` any of them on any schedule without reading a proof. Re-pointed consumers (single-source enforcement): `ScheduleCombinators.scheduleWallclockUs` → `wallclockUs` `CompressedSchedule.resourceOfSysCalls` → the per-kind counters `FTSchedule.countKind` → `countWhere` `GE2021PPMSysInv.count_*` → the per-kind counters `QECScheduleToSystem.decodeIds/pfuCorrs` → moved here The FTQ-VM computes the same quantities independently from the same DEVICE-PROGRAM files; `scripts/EmitResourceCounts.lean` + `ftq_vm/backend/tests/test_resource_counts.py` assert exact agreement.
defisGate1q
def isGate1q   : SysCallKind → Bool | .Gate1q ..             => true | _ => false
defisGate2q
def isGate2q   : SysCallKind → Bool | .Gate2q ..             => true | _ => false
defisMeasure
def isMeasure  : SysCallKind → Bool | .Measure ..            => true | _ => false
defisTransit
def isTransit  : SysCallKind → Bool | .TransitQubit ..       => true | _ => false
defisFreshAnc
def isFreshAnc : SysCallKind → Bool | .RequestFreshAncilla _ => true | _ => false
defisMagicReq
def isMagicReq : SysCallKind → Bool | .RequestMagicState _   => true | _ => false
defisDecode
def isDecode   : SysCallKind → Bool | .DecodeSyndrome _      => true | _ => false
defisFeedback
def isFeedback : SysCallKind → Bool | .PauliFrameUpdate _    => true | _ => false
defwallclockUs
def wallclockUs (xs : List SysCall) : Nat
*Wallclock** (µs): the latest `end_us` (0 for the empty schedule).
deftotalBusyUs
def totalBusyUs (xs : List SysCall) : Nat
*Total busy time** (µs): the sum of all op durations (a lower bound on hardware-seconds; ≥ wallclock·(min parallelism)).
defcountWhere
def countWhere (p : SysCallKind → Bool) (xs : List SysCall) : Nat
Count SysCalls whose kind satisfies `p`.
defcountGate1q
def countGate1q   (xs : List SysCall) : Nat
defcountGate2q
def countGate2q   (xs : List SysCall) : Nat
defcountMeasure
def countMeasure  (xs : List SysCall) : Nat
defcountTransit
def countTransit  (xs : List SysCall) : Nat
defcountFreshAnc
def countFreshAnc (xs : List SysCall) : Nat
defcountMagicReq
def countMagicReq (xs : List SysCall) : Nat
defcountDecode
def countDecode   (xs : List SysCall) : Nat
defcountFeedback
def countFeedback (xs : List SysCall) : Nat
defopCountS
def opCountS (xs : List SysCall) : Nat
Total SysCall count (physical ops AND system calls).
defdecodeIds
def decodeIds (xs : List SysCall) : List Nat
The decode round ids, in emission order.
defpfuCorrs
def pfuCorrs (xs : List SysCall) : List Nat
The frame-update correction ids, in emission order.
defsitesTouched
def sitesTouched (xs : List SysCall) : List Nat
All sites the schedule ever touches (deduplicated; uses the IR's `syscall_acts_on` site map).
defqubitFootprint
def qubitFootprint (xs : List SysCall) : Nat
*Qubit footprint**: how many distinct sites the schedule uses.
defsitesActiveAt
def sitesActiveAt (xs : List SysCall) (t : Nat) : List Nat
Sites occupied at instant `t` (half-open `[begin, end)` activity).
defpeakSiteOccupancy
def peakSiteOccupancy (xs : List SysCall) : Nat
*Peak site occupancy**: the maximum number of simultaneously occupied sites, sampled at op start times (sufficient: occupancy only increases when an op begins).
defsyndromeBitsTotal
def syndromeBitsTotal (bits : Nat) (xs : List SysCall) : Nat
Total syndrome bits produced, at `bits` per measurement.
instanceFormalRV.Resource.HasResourceCount
instance : FormalRV.Resource.HasResourceCount (List SysCall)
theoremcountWhere_append
theorem countWhere_append (p : SysCallKind → Bool) (xs ys : List SysCall) :
    countWhere p (xs ++ ys) = countWhere p xs + countWhere p ys
theoremdecodeIds_append
theorem decodeIds_append (xs ys : List SysCall) :
    decodeIds (xs ++ ys) = decodeIds xs ++ decodeIds ys
theorempfuCorrs_append
theorem pfuCorrs_append (xs ys : List SysCall) :
    pfuCorrs (xs ++ ys) = pfuCorrs xs ++ pfuCorrs ys
theoremcountDecode_eq_decodeIds_length
theorem countDecode_eq_decodeIds_length (xs : List SysCall) :
    countDecode xs = (decodeIds xs).length

FormalRV.Resource.SysCallCountLaws

FormalRV/Resource/SysCallCountLaws.lean
FormalRV.Resource.SysCallCountLaws — the counting ALGEBRA: how the canonical L4 counters (`SysCallCount`) behave under the schedule combinators (`shiftSchedule` / `seqSchedules` / `parSchedules`). These laws are what lets a composite schedule's resources be computed from its parts' WITHOUT expansion — they back the `CompressedSchedule.resource = resourceOfSysCalls ∘ expand` correctness theorem (`System/Artifacts/CompressedRepeat/ResourceCorrectness.lean`).
theoremcountWhere_shift
theorem countWhere_shift (p : SysCallKind → Bool) (dt : Nat)
    (xs : List SysCall) :
    countWhere p (shiftSchedule dt xs) = countWhere p xs
theoremcountWhere_seqSchedules
theorem countWhere_seqSchedules (p : SysCallKind → Bool)
    (xs ys : List SysCall) :
    countWhere p (seqSchedules xs ys) = countWhere p xs + countWhere p ys
theoremcountWhere_parSchedules
theorem countWhere_parSchedules (p : SysCallKind → Bool)
    (xs ys : List SysCall) :
    countWhere p (parSchedules xs ys) = countWhere p xs + countWhere p ys
theoremopCountS_shift
theorem opCountS_shift (dt : Nat) (xs : List SysCall) :
    opCountS (shiftSchedule dt xs) = opCountS xs
theoremopCountS_seqSchedules
theorem opCountS_seqSchedules (xs ys : List SysCall) :
    opCountS (seqSchedules xs ys) = opCountS xs + opCountS ys
theoremopCountS_parSchedules
theorem opCountS_parSchedules (xs ys : List SysCall) :
    opCountS (parSchedules xs ys) = opCountS xs + opCountS ys
theoremmax_add
private theorem max_add (a b d : Nat) :
    Nat.max (a + d) (b + d) = Nat.max a b + d
theoremfoldl_max_init
private theorem foldl_max_init (xs : List SysCall) :
    ∀ a, xs.foldl (fun acc sc => Nat.max acc sc.end_us) a
      = Nat.max a (wallclockUs xs)
theoremwallclockUs_append
theorem wallclockUs_append (xs ys : List SysCall) :
    wallclockUs (xs ++ ys) = Nat.max (wallclockUs xs) (wallclockUs ys)
theoremwallclockUs_parSchedules
theorem wallclockUs_parSchedules (xs ys : List SysCall) :
    wallclockUs (parSchedules xs ys)
      = Nat.max (wallclockUs xs) (wallclockUs ys)
theoremfoldl_max_shift
private theorem foldl_max_shift (dt : Nat) (xs : List SysCall) :
    ∀ a, (shiftSchedule dt xs).foldl (fun acc sc => Nat.max acc sc.end_us) (a + dt)
      = xs.foldl (fun acc sc => Nat.max acc sc.end_us) a + dt
theoremwallclockUs_shift_of_ne_nil
theorem wallclockUs_shift_of_ne_nil (dt : Nat) (xs : List SysCall)
    (h : xs ≠ []) : wallclockUs (shiftSchedule dt xs) = dt + wallclockUs xs
Shifting a NONEMPTY schedule shifts its wallclock.
theoremwallclockUs_seqSchedules
theorem wallclockUs_seqSchedules (xs ys : List SysCall) :
    wallclockUs (seqSchedules xs ys) = wallclockUs xs + wallclockUs ys
*Wallclock is additive under sequential composition** (the case split handles the empty tail, whose shift contributes nothing).

FormalRV.Resource.UComCombinators

FormalRV/Resource/UComCombinators.lean
FormalRV.Resource.UComCombinators ───────────────────────────────── Resource-count laws for the CORE `BaseUCom` circuit combinators: the derived gates (`CCX`, `controlled_R`) and the generic builders (`control`, `npar`, `npar_H`). These are the compositional laws that let a gadget's count theorem reduce a structured circuit to the counts of its parts — e.g. QPE's count decomposes over a BLACK-BOX oracle family via `control`/`npar`. Same discipline as the rest of `Resource/`: the counters (`UComCount.lean`) never change; this file only PROVES what they return on the core combinators. Everything here is forced by the syntax tree — `SKIP` is honestly one `app1` gate (`ID 0 = R(0,0,0)` on qubit 0), `SWAP` is honestly 3 CNOTs, `CCX` is honestly its 15-gate decomposition. Imports: the IR-level counters + `Core.UnitaryOps` (where `control`/`npar` live). Still NO gadget constructors, NO correctness proofs.
theoremwidthU_SWAP
theorem widthU_SWAP {dim : Nat} (m n : Nat) :
    widthU (SWAP m n : BaseUCom dim) = max (m + 1) (n + 1)
Width of `SWAP` (3 CNOTs): it touches exactly its two qubits.
theoremwidthU_controlled_R
theorem widthU_controlled_R {dim : Nat} (q t : Nat) (θ φ lam : ℝ) :
    widthU (controlled_R q t θ φ lam : BaseUCom dim) = max (q + 1) (t + 1)
Width of `controlled_R`: it touches exactly the control and the target.
theoremwidthU_CCX
theorem widthU_CCX {dim : Nat} (a b c : Nat) :
    widthU (CCX a b c : BaseUCom dim) = max (a + 1) (max (b + 1) (c + 1))
Width of `CCX`: it touches exactly its three qubits.
theoremoneQCountU_control
theorem oneQCountU_control {dim : Nat} (q : Nat) (c : BaseUCom dim) :
    oneQCountU (control q c) = 4 * oneQCountU c + 9 * cnotCountU c
One-qubit-gate count of a controlled circuit: `4·(one-qubit gates of c) + 9·(CNOTs of c)`.
theoremcnotCountU_control
theorem cnotCountU_control {dim : Nat} (q : Nat) (c : BaseUCom dim) :
    cnotCountU (control q c) = 2 * oneQCountU c + 6 * cnotCountU c
CNOT count of a controlled circuit: `2·(one-qubit gates of c) + 6·(CNOTs of c)`.
theoremwidthU_control
theorem widthU_control {dim : Nat} (q : Nat) (c : BaseUCom dim) :
    widthU (control q c) = max (q + 1) (widthU c)
Width of a controlled circuit: the control qubit joins the footprint.
theoremoneQCountU_npar
theorem oneQCountU_npar {dim : Nat} (n : Nat) (g : Nat → BaseUCom dim) :
    oneQCountU (npar n g) = (∑ i ∈ Finset.range n, oneQCountU (g i)) + 1
One-qubit-gate count of `npar n g`: the sum over the family, plus 1 for the terminal `SKIP` (honestly an `app1` in the tree).
theoremcnotCountU_npar
theorem cnotCountU_npar {dim : Nat} (n : Nat) (g : Nat → BaseUCom dim) :
    cnotCountU (npar n g) = ∑ i ∈ Finset.range n, cnotCountU (g i)
CNOT count of `npar n g`: the sum over the family (the `SKIP` is CNOT-free).
theoremoneQCountU_npar_H
theorem oneQCountU_npar_H {dim : Nat} (k : Nat) :
    oneQCountU (npar_H k : BaseUCom dim) = k + 1
The Hadamard layer `npar_H k` has exactly `k + 1` one-qubit gates (`k` Hadamards + the terminal `SKIP`)…
theoremcnotCountU_npar_H
theorem cnotCountU_npar_H {dim : Nat} (k : Nat) :
    cnotCountU (npar_H k : BaseUCom dim) = 0
… and zero CNOTs.
theoremwidthU_npar_H
theorem widthU_npar_H {dim : Nat} (k : Nat) (hk : 0 < k) :
    widthU (npar_H k : BaseUCom dim) = k
Width of the Hadamard layer: exactly `k` qubits (for `k ≥ 1`).

FormalRV.Resource.UComCount

FormalRV/Resource/UComCount.lean
FormalRV.Resource.UComCount ─────────────────────────── The canonical, INDEPENDENT resource counters for the `BaseUCom` UNITARY IR (Hadamards, rotations, CNOT, SWAP, …) — the genuinely-quantum circuits (QFT, QPE) that the reversible `Gate` IR cannot express. CLOSES THE GAP: before this file, `BaseUCom` had NO gate counter at all — QFT/QPE "resource" was only an `IsCliffordT` predicate plus a real-valued approximation ERROR budget, neither of which is a gate count. Here are honest counters. Each counter is a structural recursion over the `UCom` syntax tree. It matches ONLY the shape (`app1` = 1-qubit gate, `app2` = CNOT, `seq` = compose) and never inspects the rotation angles, so it is a pure, computable tree-walk independent of the gate parameters — the same uncheatable discipline as `GateCount.lean`, now over the unitary IR. (`BaseUnitary 1 = {R}`, `BaseUnitary 2 = {CNOT}`, `BaseUnitary 3` is empty — so these three shapes cover every `BaseUCom`.) Imports ONLY the IR (`Core.QuantumGate`). The per-gadget count THEOREMS (`countCNOT (IQFT n) = …`) live with their gadget (e.g. `QFT/IQFTResource.lean`).
defoneQCountU
def oneQCountU {dim : Nat} : BaseUCom dim → Nat
  | UCom.seq a b      => oneQCountU a + oneQCountU b
  | UCom.app1 _ _     => 1
  | UCom.app2 _ _ _   => 0
  | UCom.app3 _ _ _ _ => 0
*1-qubit-gate count** of a `BaseUCom` circuit (each `app1`: H, Rz, T, X, …).
defcnotCountU
def cnotCountU {dim : Nat} : BaseUCom dim → Nat
  | UCom.seq a b      => cnotCountU a + cnotCountU b
  | UCom.app1 _ _     => 0
  | UCom.app2 _ _ _   => 1
  | UCom.app3 _ _ _ _ => 0
*CNOT count** of a `BaseUCom` circuit (`app2` is CNOT — the only 2-qubit primitive in `BaseUnitary`).
defgateCountU
def gateCountU {dim : Nat} : BaseUCom dim → Nat
  | UCom.seq a b      => gateCountU a + gateCountU b
  | UCom.app1 _ _     => 1
  | UCom.app2 _ _ _   => 1
  | UCom.app3 _ _ _ _ => 0
*Total primitive-gate count** of a `BaseUCom` circuit.
defwidthU
def widthU {dim : Nat} : BaseUCom dim → Nat
  | UCom.seq a b      => max (widthU a) (widthU b)
  | UCom.app1 _ n     => n + 1
  | UCom.app2 _ m n   => max (m + 1) (n + 1)
  | UCom.app3 _ a b c => max (max (a + 1) (b + 1)) (c + 1)
*Qubit count (register width)** of a `BaseUCom` circuit: the largest qubit index touched, plus one — the SPACE resource, dual to the gate counts (TIME).
theoremgateCountU_eq_oneQ_add_cnot
theorem gateCountU_eq_oneQ_add_cnot {dim} (c : BaseUCom dim) :
    gateCountU c = oneQCountU c + cnotCountU c
The total gate count is exactly the 1-qubit gates plus the CNOTs (two independent counters, reconciled from the same tree).
example(example)
example {dim} (c t : Nat) : gateCountU (BaseUCom.CNOT c t : BaseUCom dim) = 1
A `SWAP` is three CNOTs (and no 1-qubit gates).
example(example)
example {dim} (m n : Nat) : gateCountU (BaseUCom.SWAP m n : BaseUCom dim) = 3
example(example)
example {dim} (n : Nat) :
    gateCountU (UCom.seq (BaseUCom.H n) (BaseUCom.CNOT 0 1) : BaseUCom dim) = 2