Quantum Turing Patterns

Labyrinth pattern formation.

Public display  ·  Interactive explorer  ·  Numerical reproduction  ·  Lean 4 formalization

This repository accompanies Quantum Turing Patterns. The visualization, interactive explorer, numerical reproduction workflow, and Lean 4 formalization are kept in separate directories.

Highlights

• constructive Turing pattern formation in Lindblad lattice dynamics;
• finite-wave-number selection and commensurate stripe branches;
• two-dimensional stripe, spot, and labyrinth morphologies;
• microscopic Bragg order, Gaussian covariance dynamics, and opposite-momentum entanglement;
• Lean 4 verification of the finite-dimensional identities used in the construction.

Read the popular article on LinkedIn: how I conceived the research, what was solved, and why it is exciting.

Repository guide

Path	Contents
display/	Lightweight GitHub display and direct links to the stripe, spot, and labyrinth movies.
interactive-display/	Jupyter explorers, presentation viewer, and display-generation tools.
reproduction/	Numerical code, compact reference data, figure generation, and scientific verification.
lean4 formalization/	Lean 4 project for the spectral design, parameter map, stripe coefficients, and Gaussian formulas.

The interactive display and reproduction workflows are intentionally separate: interactive-display/ is designed for direct exploration and visualization, while reproduction/ contains the paper-scale calculations and verification tools.

Interactive Pattern Explorer

The interactive display package includes three Jupyter entry points:

• Portable Explorer — recommended for most readers; it uses a standard Python kernel and falls back to a regular notebook preview when widget controls are unavailable.
• Research Explorer — the full interactive interface for varying initial conditions, following the time evolution, and saving selected results.
• Exhibit Notebook — a streamlined presentation of the precomputed stripe, spot, and labyrinth movies.

To launch the full Research Explorer:

cd interactive-display
conda env create -f environment.yml
conda activate qtp-display
python launch_qtp_explorer.py

For a standard Jupyter environment, open the portable notebook directly:

cd interactive-display
jupyter lab qtp_explorer_portable.ipynb

See interactive-display/README.md for the notebook roles and display/README.md for the movie gallery.

Numerical reproduction

cd reproduction
conda env create -f environment.yml
conda activate quantum-turing-patterns
python verify.py

A short fresh calculation is available through:

python run.py --mode smoke --force
python verify.py --mode smoke

The quick workflow regenerates the compact stripe and Gaussian results. The full workflow also generates the complete spot and labyrinth trajectories. See reproduction/README.md for details.

Lean 4 formalization

cd "lean4 formalization"
lake build

The Lean toolchain and mathlib revision are pinned. The formalization verifies the algebraic identities used in the spectral design, Lindblad parameter map, explicit stripe coefficients, and homogeneous Gaussian analysis. See lean4 formalization/README.md for the precise scope.

References

K. Ikeda,
“Quantum Turing Patterns,” arXiv:2607.26331 [math-ph]
Quantum_Turing_Patterns__Kazuki_Ikeda(2026).pdf

K. Ikeda,
“A Zoology of Quantum Turing Patterns,” arXiv:2608.20151 [quant-ph]