Exercise BE-012

Permutation Gram sums give identity for a bijection, and finite-square injectivity already implies surjectivity; the historical alleged independent necessity is explicitly refuted. The injective product embedding yields a raw0/1 partial permutation in both rows and columns; a positive normalizer can rescale that block but supplies no arbitrary relative weights or circuit/resource certificate.

1. Permutation Gram sums give identity for a bijection, and finite-square injectivity already implies surjectivity; the historical alleged independent necessity is explicitly refuted.
2. The injective product embedding yields a raw0/1 partial permutation in both rows and columns; a positive normalizer can rescale that block but supplies no arbitrary relative weights or circuit/resource certificate.

For P(i,j)=1[i=p(j)], (P^T P)(i,j)=sum_k1[k=p(i)]1[k=p(j)]. If i=j the single surviving term at p(i) gives1; if i≠j injectivity makes p(i)≠p(j) so it is0. Thus injectivity proves column Gram identity.

For a bijection, (PP^T)(i,j)=sum_k1[i=p(k)]1[j=p(k)]. If i≠j every summand is0. If i=j exactly one preimage k=p^{-1}(i) exists by surjectivity and is unique by injectivity, giving1. This reproduces the complete source row proof, and both identities give the rational orthogonality proxy. The source's separate injective-column and bijective-row interfaces express a proof organization, not an independence theorem about their hypotheses.

Crucially p is a self-map of ONE finite set of n elements. If injective, its image has n elements and therefore is the whole codomain; hence it is surjective. So injectivity alone ALREADY implies bijectivity and both Gram identities in the declared finite square setting. The historical demand that injectivity is insufficient is false here; there is no allowed missing-row counterexample. Infinite or rectangular injections could change that conclusion, but are not replacements for this question. At n0 all entrywise assertions are vacuous and the unique empty self-map is both injective and surjective.

With a chosen zero:Fin ancilla, let e(s)=zero.val*system+s.val. This embedding is injective: equality cancels the common offset and gives equal system values. The clean block is B(r,c)=1[e(r)=p(e(c))]. It is0/1. Two different clean rows cannot both equal the same p(e(c)), so each column has at most one1. If one row had1 at two columns, injectivity of p followed by injectivity of e would force those columns equal. Thus each row also has at most one1, and B is a partial permutation; a clean column may have zero1s because its image leaks outside the clean set. A chosen zero requires a nonempty ancilla-basis carrier; a zero-qubit signal register still has dimension1 and is not an empty carrier. If system dimension0 the clean block is empty and assertions are vacuous.

At unit normalizer the directly extracted target B can only be that raw0/1 partial permutation. However the conventional exact encoding equation is A=alpha B. For positive alpha a common rescaling alpha times such a block is encoded by the same U with that declared normalizer. For example U=I and alpha2 encode A=2I, whose entries are not all0/1. Thus the unqualified assertion that a permutation can encode no non-0/1 target is false once nonunit normalizers are allowed. A common scalar does not create arbitrary relative weights, signs or dense entries; realizing those generally requires further constructions or a different encoding. These finite rational identities embed into real/complex unitary matrices, but do not compile a reversible map into primitive gates, charge its cost, establish workspace cleanup or prove postselection/preparation efficiency.

1. Derives column Gram by injective disjoint supports and row Gram by unique preimages for a bijection; handles empty basis. (1 weight)
2. Explicitly refutes injectivity-insufficient in a finite square self-map by finite injective=>surjective, without substituting a rectangular/infinite contract or mistaking lemma interfaces for necessity. (1 weight)
3. Gives exact product clean-block formula, both row/column partial-permutation bounds and clean-index domain; distinguishes raw B from A=alpha B and avoids resource overclaims. (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/BlockEncodingClassics.lean

  def permMatrix (lines 19-20); def columnInner/rowInner/IsRationalOrthogonal (lines 23-36); theorem permMatrix_columnInner_of_injective (lines 283-327); permMatrix_rowInner_of_bijective (lines 330-382); permMatrix_isRationalOrthogonal_of_bijective (lines 389-394); def productIndex (lines 48-57); theorem cleanBlockProduct_permMatrix_entry (lines 81-86)

  Source SHA-256: 94ac6632924df0a49b1ebd99bb5d9ed69b2ea463ec527033f38bd73deeb1346a · MIT (repository LICENSE)

Contract: 9dcb092d2d4df085dca462e15f8adfb57c3e054e64c640be62c132ac9cda81ce

Item digest: d3531b7ea66a3643d9cf50addc453ad037f9a0cb641b855d4ba3517ffd568c49

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-be-012", "predecessor_item_digest": "f2574f4e42e99fa324af5c0df2eb12570c39d40fa042763277872b2a3b8abb8a", "predecessor_contract_hash": "be2e431321111e231fd75ca79c603a24a827d45ffc7335d5621f6abd48b5977e", "current_contract_hash": "9dcb092d2d4df085dca462e15f8adfb57c3e054e64c640be62c132ac9cda81ce", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/be-012-finite-injection-question-successor.json", "repair_record_digest": "38ca61034725e92bfe7863c8d0d2d02d3287aac60b7a641b72afeb1a29a08b5c", "review_record": "reports/textbook-v1/repairs/be-012-finite-injection-question-successor-review.json", "review_digest": "0777fd82f02c7538518a8fb598fbfb690497c984bdf2c94ef65be6e910dd73bd", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }