Matrix Constructions

Exercise LA-115

intermediate · proof · train

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

Assumptions and conventions

Finite real orthogonal matrix with determinant 1 before reorientation
The sign flip acts on a single designated unused column

Branch selection uses the permutation parity, a discrete value in {+1,-1}
Original derivation from inspected local source; no fresh Lean verification

Question

An orthogonal matrix U is reoriented to have determinant 1 by multiplying it with a sign-flip on a single designated unused column exactly when U already has the wrong sign; the choice is made by the parity (sign) of an accompanying column permutation, not by evaluating the determinant. Prove the reoriented matrix is orthogonal with determinant 1 regardless of which branch is taken.

Hint: mathematical route

Reorienting an orthogonal matrix to determinant 1 by a single sign-flip chosen from column-permutation parity yields an orthogonal det-1 matrix on both parity branches, without ever evaluating the determinant.

Positive-parity branch: permuted matrix is orthogonal with determinant sign(P)*det U = 1.
Negative-parity branch: compose with a single-column sign flip to multiply the determinant by -1.
Show orthogonality survives the sign flip since it is itself orthogonal.
Conclude both exhaustive parity branches give orthogonal determinant-one matrices.

Reference solution

Let P be the column permutation and consider two branches. If sign(P) = +1, the output is the permuted matrix permuteColumns(U,P) alone; a column permutation of an orthogonal matrix is orthogonal (its Gram matrix is the identity permuted on both sides, still the identity), and its determinant equals sign(P) times det(U) = (+1)*(1) = 1 when U has determinant 1. If sign(P) = -1, the output is permuteColumns(U,P) multiplied by a single-column sign flip S. Orthogonality: S is orthogonal (it is a diagonal of plus/minus ones), and a product of orthogonal matrices is orthogonal, with S^T (permuteColumns Gram) S = S^T I S = I. Determinant: det(permuteColumns(U,P)*S) = det(permuteColumns(U,P)) * det(S) = (sign(P)*det U) * (-1) = (-1)*(1)*(-1) = 1. Because the orthogonal group over the reals has only signs plus or minus one for a permutation, these two branches are exhaustive, and both yield orthogonal determinant-one matrices. Crucially the branch is selected by the discrete permutation parity, so no real determinant comparison or thresholding is performed. This is an exact orientation-fix construction, not a numerical sign test.

Assessment rubric

Positive-parity branch: permuted matrix orthogonal with det 1 (1 weight)
Negative-parity branch: single sign-flip restores det 1 and keeps orthogonality (1 weight)
Note the branch is chosen by discrete parity, not a determinant evaluation (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/ConstructiveIsometryCompletion.lean
permuteColumns_orthogonal223-229; permuteColumns_det231-234; orientColumns237-240; orientColumns_orthogonal242-254; orientColumns_det256-267
Source SHA-256: 1b61cbc9ad587cc2ae2a7cdc7bacd3b7d39fb05274833a3fea5dbb4dff69678c · MIT (repository LICENSE)

Contract: b748764c4bc330261446756e2f7c633c2f5257491bc08adeb0dee387b7c89d9b

Item digest: c1f7bebe1314ec75cc91e72658ca0457c6bc62518acffb2a8b53db63dd6bb50d

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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