The ambient scalar isomorphism carries the vacuum state

Proved

OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso_trace

by wurtle · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

free-group-factorsoai-math

Let $u,v$ be nonzero real numbers with $u^2+v^2=1$ . Let $\mathcal A(u,v)$ be the ambient von Neumann algebra of the weighted Fock model with edges labelled by $\mathbb N$ , with vacuum state $\omega$ , and let $\Psi$ be the isomorphism of $\mathcal A(u,v)$ onto the scalar Gaussian algebra generated by the scalar system with root $\Omega$ . For $T\in\mathcal A(u,v)$ ,

\langle\Omega,\Psi(T)\Omega\rangle=\omega(T).

This shows that the identification with the free Gaussian algebra is trace-preserving.

Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement.

Preamble

import Mathlib
import Definitions.Def_FreeGroupFactorProof18

namespace OAI

noncomputable section
namespace FreeGroupFactorMain.WeightedFock
open FreeFock Amplification GaussianRecognition
variable (u v : ℝ) (hv : 0<v) (hvu : v<u)

variable (hu : u≠0) (hv' : v≠0) (hunit : u^2+v^2=1)

Formal statement

theorem ambientScalarIso_trace (T : ambientAlgebra (ι := ℕ) u v) :
    inner ℂ scalarSystem.root ((ambientScalarIso u v hu hv' hunit T : FreeFock.Operator ScalarIndex) scalarSystem.root)=
      vacuumTrace u v (T:Operator ℕ) := by
  sorry

end FreeGroupFactorMain.WeightedFock
end
end OAI

Source

OpenAI, An isomorphism of the free group factors, September 23, 2026, https://github.com/openai/math (paper: preprints/An-isomorphism-of-the-free-group-factors-September-23-2026/An-isomorphism-of-the-free-group-factors-September-23-2026.pdf; Lean: lean/OAI/Analysis/FreeGroupFactor and lean/OAI/Analysis/InterpolatedFactors, Apache License 2.0); Lean declaration `OAI.FreeGroupFactorMain.WeightedFock.ambientScalarIso_trace`, https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Analysis/InterpolatedFactors/WeightedCorner.lean#L186

View graph