Exercise BE-104

The reversible program gives E and the compiler emits a list plus exact stored phase; the inherited C remains the bare list product rather than full program denotation. P(E) is independently the0/1 basis-bijection matrix with rowE(c) in each column. Gate-case/list compiler soundness gives exp(i phi)C=P(E); the actual seven-wire witness has phi45pi/8 and bare C=exp(i3pi/8)P(E), refuting literal C=P(E). The corrected equality is a genuine phase-aware refinement between independent denotations, using chronological second-times-first composition. Full program denotation is exactly a permutation; bare C has the same support with a common nontrivial phase, so physical global-phase equivalence is not exact0/1 equality or a new cleanup/resource theorem.

1. The reversible program gives E and the compiler emits a list plus exact stored phase; the inherited C remains the bare list product rather than full program denotation.
2. P(E) is independently the0/1 basis-bijection matrix with rowE(c) in each column.
3. Gate-case/list compiler soundness gives exp(i phi)C=P(E); the actual seven-wire witness has phi45pi/8 and bare C=exp(i3pi/8)P(E), refuting literal C=P(E).
4. The corrected equality is a genuine phase-aware refinement between independent denotations, using chronological second-times-first composition.
5. Full program denotation is exactly a permutation; bare C has the same support with a common nontrivial phase, so physical global-phase equivalence is not exact0/1 equality or a new cleanup/resource theorem.

Let P(E)[r,c]=1 if r=E(c), else0. C remains the bare list denotation as the inherited assumption requires: evalCircuit([])=I and evalCircuit(g::rest)=evalCircuit(rest) evalGate(g). A PrimitiveProgram additionally stores exact phi; evalProgram(program)=exp(i phi) C. The correct refinement is D=evalProgram(compile(program))=P(E), hence C=exp(-i phi)P(E). Exact C=P(E) holds only when exp(i phi)=1 (on the nonempty seven-wire basis), not automatically for every compiled program.

The compiler uses X,CX,CCX gate cases. X and CX compile with phase0 and their literal basis-permutation matrices. For CCX, the full H/T/Tdagger/CX macro is proved exactly: its monomial middle network restores every basis bit and gives phase-1 precisely on the111 triple (CCZ), and conjugating on the target by H gives controlled-controlled X. The source proves the bit cases, phase product, block-diagonal HZH=X and H²=I, not merely a name-based claim. Each gate case therefore satisfies evalProgram(compileGate(g))=P(E_g).

For chronology first then second, evalProgram(first.seq(second))=evalProgram(second)evalProgram(first), since lists append in chronology and stored phases add. Also P(E_second)P(E_first)=P(E_second∘E_first). Empty list givesI; induction on head/rest using these two composition identities proves the full compiler theorem. This is a refinement between independently defined primitive matrix and reversible-bijection semantics, not the definition of either one. In particular it applies to the full2^7 space, without needing a work-clean premise for the matrix equality. The separate advertised modular-address action/cleanup theorem DOES require initial work=0; refinement alone must not erase that hypothesis.

For the actual phase ledger, primitiveHProgram is chronological RZ(pi) then RY(pi/2), with stored phase pi/2, so its full denotation is H. T uses RZ(pi/4) with stored phase pi/8; Tdagger uses RZ(-pi/4) with stored phase-pi/8. A CCX macro contains two H blocks, four T blocks and three Tdagger blocks, plus phase-zero CX blocks. Thus phi_CCX=2(pi/2)+4(pi/8)-3(pi/8)=9pi/8. modularAdd3ReversibleProgram lists CCX(3,0;6),CCX(6,1;2),CCX(3,0;6),CCX(3,0;1),CX(3;0),CCX(4,1;2),CX(4;1),CX(5;2): exactly five CCX. primitiveAccess3 prepends X0,X1, both phase0. Therefore the stored exact angle evaluates to phi=45pi/8, not0; phases are accumulated exactly, not automatically reduced modulo2pi.

The complete phase-aware source theorem yields exp(i45pi/8) C=P(E), so C=exp(-i45pi/8)P(E)=exp(i3pi/8)P(E). The nonzero bare entries all equal exp(i3pi/8), which is nonreal and not1; its zeros and one-supported-position-per-row/column pattern match P(E), and it is unitary, but it is NOT an exact0/1 or real permutation matrix. The old requested equality is concretely false. The full program D IS the exact0/1 permutation and maps each basis ket to |E(c)>; bare C maps it to exp(i3pi/8)|E(c)>.

A common global phase leaves outcome probabilities and isolated pure-state rays unchanged, so the bare circuit is physically equivalent in that limited projective sense. This question instead asks exact matrix equality, where the scalar matters, especially before forming controlled operations or phase-sensitive compositions. Recording the ledger does not by itself claim a physical global-phase gate, free controlled implementation, finite-bit synthesis or a new resource bound. The seven-wire type is the concrete witness space, not an arbitrary-width gate theorem. Static proof reading is not a fresh kernel or circuit execution; separate program resource/clean-action receipts are not transferred to a different phase-omitting object.

1. Keeps C as the bare chronological product and distinguishes full D=exp(i phi)C; states/refutes the old exact C=P demand and gives the correct phase-aware refinement. (1 weight)
2. Reconstructs exact gate-case CCX/H/phase mechanism and head/rest induction with second-times-first multiplication, explaining refinement rather than definition and full-space versus clean-work arithmetic scope. (1 weight)
3. Computes H/T/Tdagger phases, CCX9pi/8 and the actual seven-wire five-CCX45pi/8 ledger; derives bare C=exp(i3pi/8)P(E), not a0/1 matrix. (1 weight)
4. Separates full exact permutation from bare monomial/global-phase-equivalent action, with no free controlled-phase, cleanup, arbitrary-width or resource promotion. (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/BandedSparseAccessPrimitive.lean

  theorem primitiveAccess3Program_eval : evalPrimitiveProgram primitiveAccess3Program = Robin.ComplexLCU.equivPermutationMatrix primitiveAccess3BasisEquiv := by exact compileReversibleProgram_eval primitiveAccess3ReversibleProgram (lines 77-80)

  Source SHA-256: e4f35bfdd690445de12d5a7e6692b9ab86d1a096b9ed3f4d1a41e07b99181ca7 · MIT (repository LICENSE)
• QuantumBlockEncoding/Robin/ComplexLCU.lean

  def equivPermutationMatrix {ι : Type*} [DecidableEq ι] (equiv : ι ≃ ι) : _root_.Matrix ι ι ℂ := fun row column => if row = equiv column then 1 else 0 (lines 148-151)

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

Contract: 789bf7e634c8ba45459366388155594cf11cf3822154020f0970064ebf0f43e8

Item digest: 518f0b0d1146a394be4521469ab17c605fa7c91f8fd2e898e927552dd039d065

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-be-104", "predecessor_item_digest": "09426de0cfd6a624bf2b04f6011fbb177a23b57067ad18a29ca7ccb95d4765d8", "predecessor_contract_hash": "4cded40db452c99cb732915e47e3b2d27b7a9973e7a32ac5b33b63ff8a58f04e", "current_contract_hash": "789bf7e634c8ba45459366388155594cf11cf3822154020f0970064ebf0f43e8", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-104-phase-aware-refinement-question-successor.json", "repair_record_digest": "64c8c9d982f74eeab60368816f64e808524724f4626c9badec05cae57aeda1b5", "review_record": "reports/textbook-v1/repairs/be-104-phase-aware-refinement-question-successor-review.json", "review_digest": "a114c1615c8a8a40c437f189aabc9deaf7666c3d7e38da707d8d23a394c47768", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }