QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Shared mathematical foundations / Matrix Constructions

Matrix Constructions

Exercise LA-114

advanced · 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

  • e is an injection from r original indices into N physical positions
  • The extension is built by greedy transpositions starting from the identity
  • A transposition fixes every point other than its two endpoints
  • Original derivation from inspected local source; no fresh Lean verification

Question

A greedy swap process extends a finite injection e from r original indices into N physical positions: starting from the identity permutation, at stage k it swaps the current image of index k with the target e(k). Prove that after r stages the resulting permutation p agrees with e on every original index, i.e. p(castLE a) = e(a) for all a < r.

Hint: mathematical route

A greedy transposition process extending a finite injection agrees with the target injection on every original index, proved by a strengthened induction using injectivity to protect earlier placements.

  1. State the stronger below-k agreement invariant and set up induction.
  2. Stage k case: the fresh transposition carries index k to e(k).
  3. Earlier index case: apply the induction hypothesis.
  4. Show e(a) differs from both swap endpoints using injectivity of p_k and e.
Reference solution

Induct on the stage count k, proving the stronger statement: after k stages the permutation agrees with e on every index a with a.val < k. At k=0 the claim is vacuous. At stage k+1 the permutation is p_k followed by the transposition swapping p_k(k) with e(k). Take any index a with a.val < k+1. If a.val = k, then the fresh swap sends p_k(k) to e(k); since the composition first applies p_k (landing on p_k(k)) and then the swap (sending it to e(k)), index k maps to e(k) as required. If a.val < k, the induction hypothesis gives p_k(a) = e(a); it remains to see the new transposition fixes e(a). It does because e(a) differs from both swap endpoints: e(a) != p_k(k) since p_k is injective and a != k (otherwise p_k(a)=p_k(k)=e(a) would force, via injectivity of e, a=k), and e(a) != e(k) since e is injective and a != k. A transposition fixes any point distinct from its two endpoints, so p_{k+1}(a) = p_k(a) = e(a). Taking k=r gives agreement on all original indices. This is an exact placement guarantee, not a sorting-cost estimate.

Assessment rubric
  1. Strengthen to agreement on indices below k and induct (1 weight)
  2. Stage k: the fresh swap sends index k to e(k) (1 weight)
  3. Earlier indices preserved because e(a) avoids both swap endpoints (injectivity) (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

Contract: 020aa1e02d58cdfdced0aef6ebd3ca9271dc47c2671a4f96abd11ca9f6b84180

Item digest: d786b4f7dd920203358d420044561a976ab5979789857cbfc7dc3a3c73a6aa96

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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