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

Structure before circuit tricks

Fourier multipliers and Schrödingerisation

Can a nonunitary evolution be represented as transport in an auxiliary coordinate?

\[w_t=-A_1\partial_pw+iA_2w\quad\longmapsto\quad i\partial_t\widehat w=(\eta A_1-A_2)\widehat w\]

What this technique preserves

A Fourier basis converts transport into a real-frequency Hermitian multiplier. Smooth extension improves a separate approximation problem; its sampled preparation is a reusable input supplier.

Hypotheses and hidden contracts

  • A_1 and A_2 Hermitian with declared Fourier sign and register order
  • Domain/boundary or finite discretization fixed
  • Safe recovery region and truncation error are explicit

Mathematical proof mechanism

This is an authored reusable derivation guide, not a claim that the full family has been source-assimilated.

  1. Split A into its Hermitian and anti-Hermitian parts.
  2. Differentiate the warped profile on its recovery region.
  3. Specify the Fourier transform and identify the derivative multiplier.
  4. Separate initial-state, discretization, simulation and recovery errors.

Exact Lean substrates

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Do not cross this boundary

This is a candidate mathematical route, not an end-to-end PDE theorem inferred from Hermite state preparation.

Related transports

Harmonic analysis to quantum evolution — proposal

Source and prior-art ledger

No external source is attached to this local mechanism note. It remains authored exposition, not a literature-priority claim.

Copy mathematical mechanism as LaTeX
% Authored mechanism lesson; not a new theorem certificate.
\section*{Fourier multipliers and Schrödingerisation}
Can a nonunitary evolution be represented as transport in an auxiliary coordinate?
\[
w_t=-A_1\partial_pw+iA_2w\quad\longmapsto\quad i\partial_t\widehat w=(\eta A_1-A_2)\widehat w
\]
A Fourier basis converts transport into a real-frequency Hermitian multiplier. Smooth extension improves a separate approximation problem; its sampled preparation is a reusable input supplier.
\paragraph{Hypotheses and contracts.}
\begin{enumerate}
\item A\_1 and A\_2 Hermitian with declared Fourier sign and register order
\item Domain/boundary or finite discretization fixed
\item Safe recovery region and truncation error are explicit
\end{enumerate}
\paragraph{Mathematical proof mechanism.}
This is a reusable derivation guide; exact certified scope is given by the linked Lean signatures.
\begin{enumerate}
\item Split A into its Hermitian and anti-Hermitian parts.
\item Differentiate the warped profile on its recovery region.
\item Specify the Fourier transform and identify the derivative multiplier.
\item Separate initial-state, discretization, simulation and recovery errors.
\end{enumerate}
\paragraph{Boundary.} This is a candidate mathematical route, not an end-to-end PDE theorem inferred from Hermite state preparation.

Download LaTeX