Exercise BE-008

For rational x,y embedded inR, both row norms are x²+y² and the cross overlap0, so D is orthogonal iff x²+y²=1. The question's real-completion existence has boundary|x|≤1, but rational witnesses need a rational square; universal clean-compression contraction rules out|c|>1 at normalizer1 in every auxiliary dimension.

1. For rational x,y embedded inR, both row norms are x²+y² and the cross overlap0, so D is orthogonal iff x²+y²=1.
2. The question's real-completion existence has boundary|x|≤1, but rational witnesses need a rational square; universal clean-compression contraction rules out|c|>1 at normalizer1 in every auxiliary dimension.

Use the inherited rational-entry backend for the initial matrix: x,y∈Q, regarded as real numbers. For D=[[x,y],[y,-x]], the two row self-overlaps are x²+y² and y²+(-x)²=x²+y². The cross-overlaps are xy+y(-x)=0 and yx+(-x)y=0. Consequently DD^T=(x²+y²)I2, and D is orthogonal exactly when x²+y²=1; the same equation gives D^T D=I2. These identities are polynomial algebra valid overQ andR. Automatic zero cross-overlap alone is not unit normalization.

The question separately asks whether a REAL y exists. For a fixed rational x viewed inR (indeed for any real x under this scalar extension), a real y with y²=1-x² exists iff|x|≤1. Necessity is y²≥0; sufficiency is y=±sqrt(1-x²). This is real-existence mathematics, not a claim that those witnesses have rational entries. Remaining within the inherited rational matrix backend, a rational y exists exactly when1-x² is a square of a rational number. For rational x=1/2 the required y=±sqrt(3)/2 is irrational: if sqrt3=a/b in lowest positive integer terms, a²=3b² forces3 to divide a and then b, a contradiction. Thus|x|≤1 alone is not a rational-completion theorem. Conversely x=3/5,y=4/5 is rational; x0 admits y±1. At x=1 or-1, y0 works over both carriers, so the largest possible |x| is1 in either carrier, although the interior rational-existence criterion is stricter.

The normalizer-one obstruction is independent of auxiliary dimension. Let J be any clean isometric embedding, J†J=I, and U any unitary (real orthogonal in the real case). Then ||J†UJ z||≤||UJz||=||z||. Hence every clean compression is a contraction. In particular a scalar c with|c|>1 cannot appear as a normalizer-one clean block in ANY signal-register dimension. More signal qubits do not remedy this. This also follows entrywise because an entry of a unit vector has magnitude≤1.

With conventional positive normalizer alpha and exact target A=alpha B, it is B=J†UJ=A/alpha that must have norm≤1; for a scalar c this requires alpha≥|c|. Raising alpha is the necessary normalization remedy, not enlarging the signal space at fixed alpha1. Over real matrices, a2x2 dilation then realizes c/alpha; over rational entries its rational completion condition still applies and no arbitrary real square-root witness is silently imported. The Gram lemmas prove conditional algebraic identities, not a general rational-existence, finite-bit synthesis, success-probability or efficient circuit theorem.

1. Computes both row norms x²+y² and both cross terms0, and derives full orthogonality iff x²+y²=1. (1 weight)
2. Distinguishes real-y existence |x|≤1 from rational-y existence1-x² a rational square, including the x1/2 obstruction and endpoint y0. (1 weight)
3. Proves clean compression is a contraction for every auxiliary dimension; rejects added signal qubits as a remedy at alpha1 and states the positive-normalizer convention A=alpha B correctly. (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 scalarDilation [[x,y],[y,-x]] (lines 532-537); scalarDilationRowDot and theorems scalarDilation_row0_normSq / row1_normSq = x*x+y*y (lines 556-571); scalarDilation_rows01_orthogonal = 0 (lines 583-588); scalarDilation_row0_unit_norm_of (lines 573-581)

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

Contract: feff0f307f0c6ad39e5005c64e9c3468a58c3a773630c438345563f33c66d55c

Item digest: ab4a63627ae3bf951da2437aeaee8a566a6610f4487fbdbb7ba3c8344a2f4974

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "predecessor_item_digest": "f7551d5420a1e61e7be02a212873d5cc4384b08c62628605282e64b91c4a7181", "predecessor_key": "qcb-core-be-008", "repair_record": "shared/repairs/be-008-contraction-carrier-answer-repair.json", "repair_record_digest": "aa3d8dd0d2ca5db0dfb2a2f84a045d398df7860fd834759d424d61ae753e6d17", "review_record": "reports/textbook-v1/repairs/be-008-contraction-carrier-answer-repair-review.json", "review_digest": "4df56bcbfedbf0f37ed4c8fada83351f35f71cef958488dd11e17fb30c3b7aaf" }