Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Circuit Resource Composition

Statement

For circuits placed on a declared common physical register, sequential composition adds gate counts and explicit depths; its width is the declared common-register width. Reusing workspace can make that width the maximum of the component widths only when the alignment and ancilla contracts permit reuse; otherwise all required wires remain allocated. Parallel composition on disjoint registers adds gate counts and widths and has depth equal to the maximum component depth. A clean ancilla is counted as clean only when the complete composed block returns it exactly to zero for every allowed data input.

Facts & Assumptions

Given: two circuits A and B embedded in one explicitly aligned physical wire register, and the intended QC09 conventions for syntax, matrix denotation and elementary resources.

[A1]

Finite circuit syntax and ordered wire labels defines a finite ordered wire set, ordered gate supports, and finite chronological layers, with the first layer applied first. The current Definition body was inspected.

[A2]

Denotational semantics of a finite layered circuit defines each layer's embedded-gate product and the chronological circuit product. The current Definition and its local proof were inspected.

[A3]

Finite circuit resource accounting counts gate occurrences, explicit layers, and all wires including workspace. The current Definition body was inspected; width below means that declared wire count.

[A4]

Tensor products of finitely many linear maps defines tensor maps by their action on elementary tensors. This is the exact interface used for the parallel tensor block.

[F1]

A clean ancilla register starts in ∣0⟩ and is returned exactly to ∣0⟩ by the complete block on every data input (Clean and dirty ancillas).

Proof

1.1A1A2A3givenalgebra

Write g(A),d(A),w(A) for gate count, explicit depth and declared width. Once both blocks are embedded in the declared common physical register, concatenating their schedules uses each gate occurrence and each layer exactly once and in order, so g(A;B)=g(A)+g(B) and d(A;B)=d(A)+d(B). The composite width is the common register's width. It equals max⁡(w(A),w(B)) only when the declared alignment reuses workspace; any wires that must remain allocated are included before taking that maximum.

2.1A1A2A3A4step 1.1algebra

In the parallel block on disjoint registers, the gate lists and wire sets are disjoint unions, so gate count and width add. Pairing the first layers, then the second layers, and so on, with empty layers on the shorter schedule, gives depth max⁡(d(A),d(B)). On elementary product vectors, the combined circuit acts by the tensor map specified in [A4]; the circuit denotation follows from [A2]. Thus this schedule realizes the stated tensor product without adding operations.

3.1F1step 1.1step 2.1∎

By [F1], a wire is a clean ancilla of the composite block only if the complete composition returns it to zero for every allowed data input. Returning it after A alone does not suffice when B later changes it. Thus an internal wire may be counted clean only after the full block's return condition is checked.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources