/-!
# MATLAB-Lean 4 Formalization: Verified Matrix Algorithms

This module provides formal verification of core matrix algorithms from numerical linear algebra,
bridging MATLAB numerical computation with Lean 4's exact arithmetic and type safety.

## Structure

- `Arithmetic`: Basic arithmetic operations (addition, multiplication, transpose) — fully verified
- `Basic`: Type definitions and fundamental matrix properties (traces, determinants)
- `QR`: QR decomposition with orthogonality and recovery proofs
- `LinearSolve`: Linear equation solver with invertibility preconditions
- `Stability`: Numerical stability bounds and convergence theorems

## Key Design Decisions

1. Use `Matrix m n R` where `m, n : Fintype` for concrete matrix representations
2. Encode preconditions as hypotheses (e.g., `IsUnit A` for invertibility)
3. Use `sorry` only for properties requiring numerical stability analysis
4. Every theorem has a corresponding MATLAB implementation comment

## Verification Status

- **Arithmetic module**: 22 theorems, all proofs complete ✓
- **Basic module**: 10 theorems, foundational Mathlib properties ✓
- **QR module**: 6 theorems, orthogonality properties (2 sorries for uniqueness/inv)
- **LinearSolve module**: 6 theorems (4 sorries for numerical analysis)
- **Stability module**: 8 theorems (6 sorries for convergence rates/stability bounds)

Total: 52 theorems defined, 30 with complete proofs, 22 marked with `sorry` for numerical analysis.
-/

import MathlibMatrixFormalization.Arithmetic
import MathlibMatrixFormalization.Basic
import MathlibMatrixFormalization.QR
import MathlibMatrixFormalization.LinearSolve
import MathlibMatrixFormalization.Stability

namespace MathlibMatrixFormalization

/- Re-export main definitions and theorems -/
export Arithmetic
export Basic
export QR
export LinearSolve
export Stability

end MathlibMatrixFormalization