Matrix Constructions

Exercise LA-101

intermediate · proof · test_public

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

Finite-dimensional real matrices; two selected rows and one column
The split angle reproduces the pair up to the nonnegative length r

RY half-angle convention: a plane rotation uses cos(t/2) and sin(t/2)
Elimination angle is the negative of the exact preparation angle; zero pivots get angle 0
Original derivation from inspected local source; no fresh Lean verification

Question

A planar rotation acts on two rows by the half-angle convention: the first row becomes cos(t/2)*x - sin(t/2)*y and the second becomes sin(t/2)*x + cos(t/2)*y, where (x,y) are the two entries in some column. Choosing the elimination angle to be the negative of the exact angle whose cosine and sine (times the pair length r=sqrt(x^2+y^2)) reproduce x and y, prove that this rotation sends the pair (x,y) to (r,0). Then explain why the special pair x=y=0 needs no separate division-by-zero case.

Hint: mathematical route

A half-angle plane rotation by the negative exact split angle sends a column pair (x,y) to (sqrt(x^2+y^2),0); the zero pair uses angle 0 and needs no division.

Record the defining identities cos(a/2)*r=x and sin(a/2)*r=y of the split angle.
Substitute into the first transformed entry and collapse via cos^2+sin^2=1 to get r.
Substitute into the second transformed entry and cancel to 0.
Handle the zero pair by the defined angle 0, giving the identity with no division.

Reference solution

By construction the exact split angle a satisfies cos(a/2)*r = x and sin(a/2)*r = y. The elimination angle is -a, so cos(-a/2)=cos(a/2) and sin(-a/2)=-sin(a/2). The transformed first entry is cos(a/2)*x + sin(a/2)*y = cos(a/2)*(cos(a/2)*r) + sin(a/2)*(sin(a/2)*r) = (cos^2(a/2)+sin^2(a/2))*r = r by the Pythagorean identity. The transformed second entry is -sin(a/2)*x + cos(a/2)*y = -sin(a/2)*cos(a/2)*r + cos(a/2)*sin(a/2)*r = 0. Hence the pair maps to (r,0) exactly, with no approximation. For x=y=0 the length r is 0 and the chosen elimination angle is defined to be 0, so the rotation is the identity and the already-zero pair stays (0,0); no reciprocal of a vanishing norm is ever formed, so the construction is total. This is an exact-real elimination identity, not a floating-point or arithmetic-cost claim.

Assessment rubric

Use cos(a/2)*r=x, sin(a/2)*r=y and the Pythagorean identity to get first entry r (1 weight)
Show the second entry cancels to exactly 0 (1 weight)
Explain the zero pair is handled by angle 0 with no division (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

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.

Read the Lean track and existing diagnostic warmups

Sources and provenance

QuantumBlockEncoding/AdjacentGivens.lean
splitAngle_real_firstColumn84-97; eliminationAngle99-99; eliminationAngle_zero101-102; eliminate_pair104-119
Source SHA-256: a43c3b4f543738cb317be01fa664fd466bfa28e21c33d10c7a90e74037a58d9c · MIT (repository LICENSE)

Contract: c3aa2e490e4464dbc7fd9b776bdaba0d27edae368772371b17fb50a66213a957

Item digest: 5d349b058b56a55a91b036f2d61d63d6c9cdc6be9ba99988d6e0d0ecea65486e

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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