Chapter EulerGenericDensity

import Mathlib


/-!
# Chapter — Euler's formula for a generic phase-space (density-matrix recursion)

Formalization of the *density-matrix* identity in `book.tex`, chapter
*"Wave-function collapse versus Euler's formula"*, §§*"Euler's formula for a
phase-space with 4 states"* and *"Euler's formula for a generic phase-space"*
(`book.tex` lines ~3478 and ~3565).

The book parametrizes a normalized wave-function recursively as
`vₙ = cₙ·lₙ + sₙ·vₙ₊₁`, with `cₙ = cos θₙ`, `sₙ = sin θₙ`, and `{lₙ}` an
orthonormal basis, and writes the projector `vₙ vₙ†` in *Euler form*:

> `vₙ vₙ† = ½ + ½(lₙ lₙ† − vₙ₊₁ vₙ₊₁†)(cos 2θₙ + Jₙ sin 2θₙ)`,
>   where `Jₙ = lₙ vₙ₊₁† − vₙ₊₁ lₙ†` plays the role of the imaginary unit in the
>   2-dimensional subspace generated by `{lₙ, vₙ₊₁}`,

and describes collapse as *"suppressing the off-diagonal `Jₙ`-proportional
terms"*, leaving the diagonal operator
`diag(vₙ vₙ†) = cₙ² lₙ lₙ† + sₙ² vₙ₊₁ vₙ₊₁†` representing the classical
conditional-probability recursion.

This module formalizes the self-contained algebraic core of that "single
recursion step" for *arbitrary* orthonormal real vectors `l, w` in `Fin d → ℝ`
(any finite dimension `d`), where `w` plays the role of `vₙ₊₁`.  It generalizes
`BookProof.ChapterEulerDensityMatrix` (the concrete 2-state `2×2` case) to the
recursion step over an arbitrary orthonormal pair in any dimension.

All results are `sorry`-free and `axiom`-clean (only `propext`,
`Classical.choice`, `Quot.sound`).

## Definitions

* `eulerVec θ l w` — the wave-function `v = cos θ · l + sin θ · w`.
* `Jgen l w` — the "imaginary unit" `J = l wᵀ − w lᵀ` of the `{l, w}` subspace.

## Results

* `vecMulVec_mul_vecMulVec` — outer-product multiplication
  `(u vᵀ)(x yᵀ) = (v · x)·(u yᵀ)`.
* `eulerVec_unit` — `v` is a unit vector (`v · v = 1`).
* `outer_eulerVec` — the density matrix expanded:
  `v vᵀ = c²·llᵀ + s²·wwᵀ + cs·(lwᵀ + wlᵀ)`.
* `Jgen_sq` — `J² = −(llᵀ + wwᵀ)` (`J` is the imaginary unit of the subspace).
* `Jgen_mul` — `(llᵀ − wwᵀ)·J = lwᵀ + wlᵀ` (the off-diagonal generator).
* **HEADLINE `density_euler_generic`** — the projector in Euler form
  `v vᵀ = ½·(llᵀ + wwᵀ) + (cos 2θ)/2·(llᵀ − wwᵀ) + (sin 2θ)/2·((llᵀ − wwᵀ)·J)`.
* **`density_collapse_generic`** — removing the `J`-proportional part yields the
  diagonal recursion `cos²θ·llᵀ + sin²θ·wwᵀ` (the book's collapse rule).
* `density_trace` (`tr = 1`), `density_symm` (`ρᵀ = ρ`), `density_idempotent`
  (`ρ² = ρ`: a projector / pure state).
-/

open scoped Matrix
open Matrix

namespace BookProof.ChapterEulerGenericDensity

variable {d : ℕ}



/-- The Euler wave-function `v = cos θ · l + sin θ · w` for the recursion step. -/
noncomputable def eulerVec (θ : ℝ) (l w : Fin d → ℝ) : Fin d → ℝ :=
  Real.cos θ • l + Real.sin θ • w

/-- The matrix `J = l wᵀ − w lᵀ` that plays the role of the imaginary unit in the
2-dimensional subspace generated by `{l, w}`. -/
def Jgen (l w : Fin d → ℝ) : Matrix (Fin d) (Fin d) ℝ :=
  Matrix.vecMulVec l w - Matrix.vecMulVec w l























end BookProof.ChapterEulerGenericDensity