Oracle Composition
Exercise BE-120
nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- The dagger is stored as the same matrix as the oracle
- The oracle's integer image map is asserted self-inverse
- A permutation matrix P is unitary with P-dagger = P^{-1}
- An uncompute restores the register iff forward then inverse is the identity
Question
A fixed indicator oracle and its stated dagger are certified for a warm Robin instance by four facts bundled together: the dagger's matrix equals the oracle's own matrix; the integer image map of the oracle is self-inverse; and the oracle matrix is a permutation (each row has a unique column with a 1, and each column a unique row). From these, explain the precise sense in which this indicator oracle is self-inverse, why 'dagger equals itself' plus 'image map self-inverse' together certify a clean uncompute, and what would break the uncompute if only the permutation property held without the self-inverse image.
Hint: mathematical route
The indicator-oracle bundle certifies U is a permutation of a self-inverse label map, so U^2 = I and U-dagger = U; dagger-equals-itself plus self-inverse image make the same oracle its own exact clean uncompute, which permutation-ness alone (P-dagger = P^{-1} not P) would not guarantee.
- The oracle matrix is a permutation of a self-inverse label map, hence an involution U^2 = I with U-dagger = U.
- Fact (a) stores the dagger as the same matrix, and fact (b) self-inverse image makes applying U twice the identity on labels.
- Thus forward-then-same-oracle is an exact clean uncompute with no residual on the register.
- With only permutation-ness, P-dagger = P^{-1} need not equal P, so reusing the same matrix gives P^2, not the identity, and the uncompute fails.
Reference solution
The bundle certifies that the indicator oracle U is an involutive permutation and that its dagger is realized by the SAME matrix. Reading the four facts: (a) the dagger's stored matrix equals the oracle's matrix, so applying 'U-dagger' is operationally identical to applying U again; (b) the oracle's integer image map j |-> image(j) satisfies image(image(j)) = j, i.e. it is self-inverse as a function on labels; (c) and (d) the matrix is a genuine permutation matrix (unique 1 per row and per column). Combining (b),(c),(d): U is the permutation matrix of a self-inverse label map, so U is an involution, U*U = I, hence U-dagger = U already follows abstractly, and (a) confirms the stored dagger matches. The precise sense of self-inverse is this involution U^2 = I. Why (a) plus (b) certify a clean uncompute: an uncompute step must restore the register, and it does so iff running the 'inverse' block after the forward block returns to the start. Here the inverse block is stored as U-dagger = U (fact a), and because the image map is self-inverse (fact b) applying U twice returns every basis label to itself, so the composite forward-then-uncompute is exactly the identity on labels. That is a clean, exact uncompute with no residual. What breaks if only the permutation property (c),(d) held WITHOUT self-inverse image: a general permutation P is unitary with P-dagger = P^{-1}, but P^{-1} need not equal P. Then applying the SAME stored matrix twice gives P^2, not the identity, so re-running the forward block does not uncompute; the register ends in the permuted-twice state and the ancilla is not restored. The self-inverse image hypothesis is exactly what guarantees that the physically convenient choice 'use the same oracle to uncompute' is correct rather than an error; permutation-ness alone gives unitarity but not involutivity.
Assessment rubric
- Interpret the bundle as: U is a permutation matrix of a self-inverse label map, hence an involution U^2 = I with U-dagger = U (1 weight)
- Explain that dagger-equals-itself (fact a) plus self-inverse image (fact b) make forward-then-same-oracle an exact clean uncompute with no residual (1 weight)
- Show that permutation-ness alone gives P-dagger = P^{-1} but not P^2 = I, so reusing the same matrix would give P^2 and fail to uncompute without the self-inverse image hypothesis (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
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.
Sources and provenance
- QuantumBlockEncoding/RobinEvolution.lean
theorem warmRobinIndicatorCertificate : (GHL2025.oneTermRobinGate_U_indic_dagger warmRobinParameters).matrix = (GHL2025.oneTermRobinGate_U_indic warmRobinParameters).matrix ∧ (∀ j : Nat, GHL2025.indicatorOracleImage warmRobinParameters (GHL2025.indicatorOracleImage warmRobinParameters j) = j) ∧ (... indicatorOracleMatrix is a permutation ...) (lines 180-210)
Source SHA-256:8673572458ff260cf35d6cfce60ffcc52b5b2be721671b3171919e32d0b73a37· MIT (repository LICENSE)
Contract: 08b2271b6f4469db7950d77bcb1428fcfac6ef910e392de1feb1ac5b167720cc
Item digest: e5fce40032b6c3cf22a772b67ac145bb32118f946cb8534d087744848f82c38b
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.