Exercise LA-119

The unoptimized Gray/Givens producer emits L=N(N-1)/2 selected planes, each3*2^q-2 gates. Its exact family ratio G/N grows quadratically, while the N4 check only distinguishes stage cost from total cost; none is an optimal-synthesis lower bound.

1. Each full-control selected rotation on q+1 wires emits exactly2^q RY and2(2^q-1) CX gates with no opaque oracle.
2. The fixed decomposeSO list emits N(N-1)/2 planes, including identity angles; this is not a minimal necessary plane count for each target.
3. Exact aggregation G=N(N-1)/2*(3N/2-2) has unbounded G/N along powers of two, unlike a linear backend family; an upper bound alone would not establish that.
4. The q1 check gives24 total versus4 per plane, not a universal asymptotic refutation. Distinct semantics/decomposition proofs and optimal/finite-bit/resource limits remain explicit.

Counts for ONE selected plane must be multiplied by the number of planes in the specified generated list. Fix the unsimplified recursive Gray/Givens backend, let S=2^q>=1, N=2^(q+1)=2S, and L=N(N-1)/2. AdjacentGivens.decomposeSO always EMITS L planes, including harmless zero-angle identity rotations. It is a list-length equality, not a theorem that a particular SO matrix optimally needs L nonidentity gates. Each full-control selected plane on the existing q+1 wires has q controls and emits S RY plus2(S-1) CX records, total3S-2. The exact generated counts are RY=L S, CX=L*2(S-1), G=L(3S-2), with zero opaque-oracle calls. These follow from the actual count equalities, not just a cubic upper bound.

Substituting S=N/2 gives G/N=((N-1)/2)*(3N/2-2). Along N=2,4,8,... this ratio is unbounded, so no fixed constant C bounds THIS backend's emitted count by C N for all widths. More quantitatively, for N>=4, L>=N^2/4 and3N/2-2>=N, hence G>=N^3/4; also G<=3N^3/4=6S^3. Thus this generated family has Theta(N^3) records. The lower comparison was derived from the exact equality for this backend; the source upper-bound theorem G<=6S^3 by itself would not prove nonlinearity or any lower bound.

At q=0,N=2,L=1 the counts are one RY and zero CX, G=1. At q=1,N=4,L=6 they are12 RY and12 CX, G=24, while one selected plane costs only four records. This datum refutes treating one-plane cost four as the whole generated list cost, but does NOT refute every asymptotic linear bound:24=6N at this size. Only the growing-width ratio above supplies that family argument.

Nor does any of this prove a lower bound on optimal SO synthesis or preparation of one chosen state/column. The identity matrix, for example, is SO and has an empty exact circuit, although this unsimplified backend still emits its fixed list and identity-angle records. A different optimizer or architecture is not constrained by the backend's count equality. Full-control coverage must actually enumerate all non-target wires, and plane realization/decomposition are extra semantic obligations beyond the per-plane resource line. In this current source those obligations are supplied separately by decomposeSO_action, selectedStep_matrix/Gray transport and compileSO_eval; they are not absent globally and are not proved merely by reading gate counts.

The count concerns the actual finite exact-angle RY/CX list on q+1 wires and no opaque oracle. It is not arithmetic preprocessing time, a finite-bit angle-synthesis/error bound, hardware routing cost, or an optimal gate lower bound. The correct lesson is to aggregate the generated family under its actual model and keep that claim distinct from optimal necessity.

1. Separates per-plane and whole generated-backend counts: L=N(N-1)/2 emitted planes, RY=L2^q, CX=2L(2^q-1), G=L(3*2^q-2), zero oracle, with identity rotations retained. (1 weight)
2. Uses the exact family equality to prove G/N unbounded (or a valid Theta(N^3) comparison), not a cubic upper bound alone or one finite-size datum. Qualifies all lower comparisons as THIS unsimplified backend, not optimal SO synthesis. (1 weight)
3. Checks q=0 and q=1; assigns the N4=24 datum only its legitimate per-stage/whole-list role. Notes full-control/decomposition semantics, their actual separate current proofs, and the identity empty-circuit counterexample to necessity. (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/SelectedRyPlane.lean

  compileSelectedRy_ryCount143-148; compileSelectedRy_cxCount150-156; compileSelectedRySteps_noOracle225-227

  Source SHA-256: 0098a9ef2bfc1af9eeaa44357b0818628084be35f88854232496e14d715c2f40 · MIT (repository LICENSE)
• QuantumBlockEncoding/GrayGivensCompiler.lean

  compileSO_cubic_bound196-199

  Source SHA-256: 21bb92938d2d0d81341700123e66195fdebb12e72db7faf066a897479fe942ce · MIT (repository LICENSE)
• QuantumBlockEncoding/AdjacentGivens.lean

  decomposeSO_length611-613

  Source SHA-256: a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c · MIT (repository LICENSE)

Contract: 24c44aece1fcea0871151b7cead13621a753b47db0ea3ba7cd7b2b6cd171e0e0

Item digest: a9967b91c8189fd5fee0735e021c093ddca3092baf82b778254b0426617d066c

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.

{ "predecessor_item_digest": "2e11be7304fdf2cc58f23e09e0f22e1e42c339a4b78bf1f957a432a7a8aa9155", "predecessor_key": "qcb-core-la-119", "repair_record": "shared/repairs/la-119-generated-backend-count-repair.json", "repair_record_digest": "07269a311d3585f1f7888bf1c54ac0d8e1b9b8dd16fee466dde740b0819db8e4", "review_record": "reports/textbook-v1/repairs/la-119-generated-backend-count-repair-review.json", "review_digest": "21277909d5def61bf93c7b0fec8375162c385327bb080dcae480242776f8d50e" }