Exercise BE-105

A real planar rotation [[c,-s],[s,c]] over C is unitary exactly when c^2+s^2=1: the off-diagonals of the Gram matrix cancel identically and conjugation is trivial on real entries.

1. Since c,s are real, the conjugate transpose M* equals the real transpose [[c,s],[-s,c]].
2. The diagonal entries of M* M are both c^2 + s^2.
3. The off-diagonal entries cancel identically to 0 as -cs+cs for every real c,s.
4. Therefore M* M = (c^2+s^2) I, equal to the identity iff c^2+s^2 = 1.
5. With c=cos t, s=sin t the Pythagorean identity makes unitarity automatic for every angle.

Call the matrix M with M = [[c, -s], [s, c]], entries real but viewed in the complex field. Its conjugate transpose M* has entries that are complex conjugates of the transpose; since c and s are real, conjugation is the identity on them, so M* = [[c, s], [-s, c]] (the ordinary real transpose). Compute M* M entrywise using Fin-2 sums. (1,1) entry: c*c + s*s = c^2 + s^2. (1,2) entry: c*(-s) + s*c = -cs + cs = 0. (2,1) entry: (-s)*c + c*s = -sc + cs = 0. (2,2) entry: (-s)*(-s) + c*c = s^2 + c^2 = c^2 + s^2. So M* M = [[c^2+s^2, 0],[0, c^2+s^2]], which equals the 2x2 identity if and only if c^2 + s^2 = 1. Hence M is unitary precisely under the normalization c^2 + s^2 = 1. No further hypothesis is required: the off-diagonal entries cancel identically for every real c, s (they are structural cancellations -cs+cs), so the only constraint comes from the diagonal. Conjugation plays no role because the entries are real: for a genuinely complex rotation one would need |entries|^2, but here conjugation acts trivially and the unitarity condition collapses to the real Pythagorean identity c^2 + s^2 = 1. In particular, taking c = cos t and s = sin t makes the identity automatic, so every angle-parameterized real rotation is unitary.

1. Compute M* as the real transpose [[c,s],[-s,c]], noting conjugation is trivial on real entries (1 weight)
2. Compute all four entries of M* M and show the off-diagonals cancel identically while the diagonal equals c^2+s^2 (1 weight)
3. Conclude unitarity iff c^2+s^2=1, with no extra hypothesis, and note cos/sin make it automatic (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/Robin/ComplexLCU.lean

  noncomputable def realOrthogonalRotation (cosine sine : Real) : _root_.Matrix (Fin 2) (Fin 2) ℂ := fun row column => match row.val, column.val with | 0, 0 => (cosine : ℂ) | 0, _ => -(sine : ℂ) | _, 0 => (sine : ℂ) | _, _ => (cosine : ℂ) (lines 23-29); theorem realOrthogonalRotation_unitary (cosine sine : Real) (normalization : cosine * cosine + sine * sine = 1) : realOrthogonalRotation cosine sine ∈ _root_.Matrix.unitaryGroup (Fin 2) ℂ (lines 32-57)

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

Contract: c70f8090a882fbf82b245b4db5bd2438d1224df0b02fb79d23233af66c0d03cc

Item digest: 15381b174d3517cf5ade51fd5a8bfdf0eee977640793ea43e93c0627b2eaede1

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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