embed

formal source

 103abbrev DeviationHilbert (N : ℕ) := Fin N → ℂ
 104
 105/-- Embed real deviations into the complex Hilbert space. -/
 106def embed (s : SmallDeviationState N) : DeviationHilbert N :=
 107  fun i => (s.deviations i : ℂ)
 108
 109/-- The squared norm of the embedding equals twice the quadratic energy. -/
 110theorem embed_norm_sq (s : SmallDeviationState N) :
 111    (Finset.univ.sum fun i => Complex.normSq (embed s i)) =
 112    Finset.univ.sum fun i => (s.deviations i) ^ 2 := by
 113  apply Finset.sum_congr rfl
 114  intro i _
 115  simp [embed, Complex.normSq_ofReal]
 116  ring
 117
 118/-! ## Discrete Evolution Operator -/
 119
 120/-- The discrete evolution operator at small strain: applies R̂ in the
 121    quadratic regime, parameterized by a real "Hamiltonian matrix" H. -/
 122structure DiscreteEvolution (N : ℕ) where
 123  hamiltonian : Fin N → Fin N → ℝ
 124  symmetric : ∀ i j, hamiltonian i j = hamiltonian j i
 125
 126/-- Apply one step of discrete evolution to deviations (linearized). -/
 127def DiscreteEvolution.step (ev : DiscreteEvolution N) (ψ : DeviationHilbert N) :
 128    DeviationHilbert N :=
 129  fun i => ψ i - Complex.I * (Finset.univ.sum fun j => (ev.hamiltonian i j : ℂ) * ψ j)
 130
 131/-- The diagonal Hamiltonian: H_ii = 1 (from J''(1) = 1 calibration). -/
 132def diagonalHamiltonian (N : ℕ) : DiscreteEvolution N where
 133  hamiltonian := fun i j => if i = j then 1 else 0
 134  symmetric := by intro i j; by_cases h : i = j <;> simp [h, eq_comm]
 135
 136/-! ## Emergence Hypothesis -/