## [Diagram]: Formal Proof Development of a Mathematical Theorem ### Overview The image displays a three-stage progression of a formal proof written in a dependently-typed proof assistant (likely Lean 4). It illustrates the development of a theorem stating that a unitary matrix which is also idempotent must be the identity matrix. The diagram shows the initial theorem statement, an intermediate proof sketch with placeholders, and the final, completed proof with specific tactics. ### Components/Axes The diagram is structured as a flowchart with three main code blocks connected by directional arrows. * **Top Block (Header):** Contains the formal theorem statement. * **Bottom-Left Block (Intermediate Stage):** Shows a proof outline with `sorry` placeholders for each step. * **Bottom-Right Block (Final Stage):** Presents the completed proof with actual tactic scripts. * **Flow Arrows:** A black arrow points from the top block to the bottom-left block. Another black arrow points from the bottom-left block to the bottom-right block, indicating the progression of the proof development. ### Detailed Analysis #### **1. Top Block: Theorem Statement** * **Content:** ```lean theorem unitary_idempotent_is_identity {n : Type*} [DecidableEq n] [Fintype n] {α : Type*} [CommRing α] [StarRing α] (U : Matrix.unitaryGroup n α) (h : (U : Matrix n n α) ^ 2 = (U : Matrix n n α)) : (U : Matrix n n α) = 1 := by sorry ``` * **Transcription & Explanation:** * **Theorem Name:** `unitary_idempotent_is_identity` * **Implicit Parameters:** * `{n : Type*}`: A type `n`, likely representing the dimension/index type of the matrix. * `[DecidableEq n]`: A typeclass instance asserting that equality on `n` is decidable. * `[Fintype n]`: A typeclass instance asserting that `n` is a finite type. * `{α : Type*}`: A type `α`, representing the scalar ring. * `[CommRing α]`: A typeclass instance asserting that `α` is a commutative ring. * `[StarRing α]`: A typeclass instance asserting that `α` has a star operation (for conjugation). * **Explicit Parameters:** * `(U : Matrix.unitaryGroup n α)`: A matrix `U` belonging to the unitary group over `n` and `α`. * `(h : (U : Matrix n n α) ^ 2 = (U : Matrix n n α))`: A hypothesis `h` stating that the square of the matrix `U` (coerced to a general matrix) equals itself (idempotence). * **Conclusion:** `(U : Matrix n n α) = 1`: The goal is to prove that the matrix `U` is the identity matrix. * **Proof Tactic:** `:= by sorry` - The proof is initially left incomplete with a placeholder. #### **2. Bottom-Left Block: Proof Sketch (Intermediate)** * **Content:** ```lean -- Step 1: Extract the unitary property U* U = 1 have h1 : star (U : Matrix n n α) * (U : Matrix n n α) = 1 := by sorry -- Step 2: From the idempotent property, multiply both sides by star U on the left have h2 : star (U : Matrix n n α) * (U : Matrix n n α) ^ 2 = star (U : Matrix n n α) * (U : Matrix n n α) := by sorry -- Step 3: Simplify the left side using associativity and the unitary property have h3 : star (U : Matrix n n α) * (U : Matrix n n α) ^ 2 = (U : Matrix n n α) := by sorry -- Step 4: Combine to get the final result have h4 : (U : Matrix n n α) = 1 := by sorry ``` * **Transcription & Explanation:** This block outlines the proof strategy in four commented steps, but each `have` statement (a local proof) is concluded with `sorry`, meaning the tactics to prove them are not yet provided. * **Step 1 (`h1`):** Aims to state the defining property of a unitary matrix: `U* U = I`. * **Step 2 (`h2`):** Applies the idempotent hypothesis `h` by multiplying both sides on the left by `U*`. * **Step 3 (`h3`):** Intends to simplify the left-hand side of `h2` using associativity of multiplication and the unitary property from `h1`. * **Step 4 (`h4`):** The final step to combine the previous results to conclude `U = I`. #### **3. Bottom-Right Block: Completed Proof (Final)** * **Content:** ```lean -- Step 1: Extract the unitary property U* U = 1 have h1 : star (U : Matrix n n α) * (U : Matrix n n α) = 1 := by exact Matrix.UnitaryGroup.star_mul_self U -- Step 2: From the idempotent property, multiply both sides by star U on the left have h2 : star (U : Matrix n n α) * (U : Matrix n n α) ^ 2 = star (U : Matrix n n α) * (U : Matrix n n α) := by rw [h] -- Step 3: Simplify the left side using associativity and the unitary property have h3 : star (U : Matrix n n α) * (U : Matrix n n α) ^ 2 = (U : Matrix n n α) := by rw [pow_two, ← Matrix.mul_assoc, h1, Matrix.one_mul] -- Step 4: Combine to get the final result have h4 : (U : Matrix n n α) = 1 := by rw [← h3, h2, h1] ``` * **Transcription & Explanation:** This block provides the actual tactic scripts to prove each step outlined in the intermediate block. * **Step 1 (`h1`):** Proven using `exact Matrix.UnitaryGroup.star_mul_self U`, which is a lemma stating `U* U = I` for a unitary `U`. * **Step 2 (`h2`):** Proven by rewriting (`rw`) with hypothesis `h` (idempotence). This changes `(U)^2` to `U` on the left side of the equation. * **Step 3 (`h3`):** Proven by a sequence of rewrites: 1. `pow_two`: Expands `(U)^2` to `U * U`. 2. `← Matrix.mul_assoc`: Associates the multiplication to the left: `(U* * U) * U`. 3. `h1`: Replaces `U* * U` with `I` (using the unitary property). 4. `Matrix.one_mul`: Simplifies `I * U` to `U`. * **Step 4 (`h4`):** Proven by rewriting backwards (`←`) with `h3`, then `h2`, then `h1`. This chain of equalities shows `U = (U* * U^2) = (U* * U) = I`. ### Key Observations 1. **Proof Development Workflow:** The diagram clearly visualizes the process of formal proof development: from a high-level statement, to a structured outline with placeholders, to a fully detailed proof with specific tactics. 2. **Use of `sorry`:** The intermediate block uses `sorry` as a placeholder, a common feature in proof assistants to mark incomplete proofs while working on the structure. 3. **Tactic-Based Proofs:** The final proof relies on rewriting (`rw`) with existing lemmas (`pow_two`, `Matrix.mul_assoc`, `Matrix.one_mul`) and hypotheses (`h`, `h1`, `h2`, `h3`). 4. **Mathematical Logic:** The proof follows a clear algebraic logic: start with the unitary property, manipulate the idempotent equation using it, and simplify to the identity. ### Interpretation This diagram is a technical artifact from the field of **formal verification** and **interactive theorem proving**. It demonstrates how a mathematical statement about linear algebra (unitary idempotent matrices) is encoded and proven within a computer system. * **What it demonstrates:** It shows the translation of an informal mathematical argument into a rigorous, machine-checkable proof. The core idea is that if a matrix `U` satisfies `U*U = I` (unitary) and `U² = U` (idempotent), then `U` must be `I`. The proof leverages the unitary property to "cancel" `U*` from the idempotent equation. * **Relationship between elements:** The arrows show a direct lineage. The theorem statement defines the problem. The intermediate sketch breaks the solution into logical steps, acting as a blueprint. The final block fills in the technical details required for the proof assistant to verify each step. * **Notable aspects:** The use of `Matrix.unitaryGroup` and associated lemmas indicates this is part of a larger formalized library of linear algebra. The proof is concise, relying on well-chosen rewrites rather than manual algebraic manipulation, showcasing the power of tactic-based proving. The progression from `sorry` to a complete proof is a quintessential experience in interactive theorem proving.