IndisputableMonolith.Foundation.HamiltonianEmergenceOperator

   1import IndisputableMonolith.Foundation.HamiltonianEmergence
   2
   3/-!
   4# Operator-level Hamiltonian emergence: the finite-dimensional Stone generator
   5
   6Build-spine item HLG-2.1 of `simulation/Reality_Simulation_Master_Plan.html`.
   7
   8`HamiltonianEmergence` proves the SCALAR foundation: the J-cost near equilibrium is a quadratic form,
   9`J(1 + eps) = eps^2/2 + O(eps^3)`, and the total cost approximates the quadratic energy. It then leaves
  10the operator-level claim `R-hat = exp(-i H-hat * 8 tau_0 / hbar)` as a HYPOTHESIS, citing "Stone's
  11theorem for discrete unitary groups not in Mathlib".
  12
  13That citation mis-frames the problem. The recognition register is FINITE-dimensional (the 8-tick
  14register is `C^N`), so the operator-level statement needs no infinite-dimensional Stone theory at all.
  15On `C^N` everything is matrix exponentials, and Mathlib has the full API. This module proves the
  16finite-dimensional Stone generator outright:
  17
  18* the complexified small-deviation Hamiltonian `Hc ev` (a real symmetric matrix viewed over `C`) is
  19  Hermitian, so it IS a self-adjoint generator;
  20* the generator `gen ev = -i * Hc ev` is skew-Hermitian;
  21* the evolution family `U ev t = exp(t * gen ev)` is a one-parameter group: `U 0 = 1` and
  22  `U s * U t = U (s + t)`;
  23* every `U ev t` is unitary (`(U t)^H * U t = 1` and `U t * (U t)^H = 1`) and lies in the unitary
  24  group `Matrix.unitaryGroup (Fin N) C`;
  25* the discrete evolution step already defined in `HamiltonianEmergence`,
  26  `DiscreteEvolution.step ev psi = psi - i * (Hc ev *v psi)`, is EXACTLY the first-order truncation
  27  `(1 + gen ev) *v psi` of the exponential `U ev 1 = exp(gen ev) = 1 + gen ev + gen ev^2/2 + ...`.
  28
  29So `R-hat`'s small-deviation linearization is a genuine unitary one-parameter group generated by a
  30self-adjoint `H-hat`. This is the operator-level content of "quantum mechanics is the high-frequency
  31limit of recognition dynamics", as a finite-dimensional THEOREM rather than a placeholder.
  32
  33Honest status: CONDITIONAL THEOREM. The Stone-generator structure (Hermitian generator, unitary group,
  34first-order truncation) is a kernel THEOREM. What stays conditional is the identification that the FULL
  35nonlinear `R-hat` action equals this linear `step` to `O(eps^3)`: that rests on the proved scalar bound
  36`totalJcost_approx_quadratic` plus the modeling choice that `R-hat` linearizes to `step`, and the exact
  37operator `O(Delta^2)` exponential Taylor bound and the `Delta = 8 tau_0 / hbar` calibration remain named
  38residuals (the same units bridge as HLG-1.2).
  39
  40Lean status: 0 sorry, 0 new axiom.
  41-/
  42
  43namespace IndisputableMonolith.Foundation.HamiltonianEmergence
  44
  45open NormedSpace
  46open scoped Matrix
  47
  48noncomputable section
  49
  50variable {N : ℕ}
  51
  52/-! ## The complexified Hamiltonian and the skew-Hermitian generator -/
  53
  54/-- The complexification of a discrete-evolution Hamiltonian: the real symmetric matrix
  55`ev.hamiltonian` viewed as a complex matrix. -/
  56def Hc (ev : DiscreteEvolution N) : Matrix (Fin N) (Fin N) ℂ :=
  57  Matrix.of (fun i j => (ev.hamiltonian i j : ℂ))
  58
  59/-- The complexified Hamiltonian is Hermitian: a real symmetric matrix is self-adjoint over `C`. -/
  60theorem Hc_isHermitian (ev : DiscreteEvolution N) : (Hc ev).IsHermitian := by
  61  show (Hc ev)ᴴ = Hc ev
  62  ext i j
  63  simp only [Matrix.conjTranspose_apply, Hc, Matrix.of_apply, Complex.star_def,
  64    Complex.conj_ofReal]
  65  norm_cast
  66  exact ev.symmetric j i
  67
  68/-- The infinitesimal generator `gen ev = -i * Hc ev`. This is the `-i H-hat` of
  69`R-hat = exp(-i H-hat * Delta)`. -/
  70def gen (ev : DiscreteEvolution N) : Matrix (Fin N) (Fin N) ℂ :=
  71  (-Complex.I) • Hc ev
  72
  73/-- The generator is skew-Hermitian: `(gen)^H = -gen`. This is the defining property of the generator
  74of a unitary one-parameter group. -/
  75theorem gen_skewHermitian (ev : DiscreteEvolution N) :
  76    (gen ev)ᴴ = -(gen ev) := by
  77  have hH : (Hc ev)ᴴ = Hc ev := (Hc_isHermitian ev).eq
  78  unfold gen
  79  rw [Matrix.conjTranspose_smul, hH]
  80  have hstar : star (-Complex.I) = Complex.I := by
  81    rw [star_neg, Complex.star_def, Complex.conj_I, neg_neg]
  82  rw [hstar, neg_smul, neg_neg]
  83
  84/-! ## The unitary one-parameter group -/
  85
  86/-- The recognition evolution family `U ev t = exp(t * gen ev)`. For the calibrated tick
  87`t = 8 tau_0 / hbar` this is the operator-level recognition step. -/
  88def U (ev : DiscreteEvolution N) (t : ℝ) : Matrix (Fin N) (Fin N) ℂ :=
  89  exp ℂ ((t : ℂ) • gen ev)
  90
  91/-- Identity at `t = 0`: `U ev 0 = 1`. -/
  92theorem U_zero (ev : DiscreteEvolution N) : U ev 0 = 1 := by
  93  unfold U
  94  rw [Complex.ofReal_zero, zero_smul, exp_zero]
  95
  96/-- One-parameter group law: `U ev s * U ev t = U ev (s + t)`. -/
  97theorem U_add (ev : DiscreteEvolution N) (s t : ℝ) :
  98    U ev s * U ev t = U ev (s + t) := by
  99  have hcomm : Commute ((s : ℂ) • gen ev) ((t : ℂ) • gen ev) :=
 100    ((Commute.refl (gen ev)).smul_left (s : ℂ)).smul_right (t : ℂ)
 101  unfold U
 102  rw [← Matrix.exp_add_of_commute ℂ _ _ hcomm]
 103  congr 1
 104  rw [← add_smul, ← Complex.ofReal_add]
 105
 106/-- The adjoint of the evolution is the time-reversed evolution: `(U ev t)^H = U ev (-t)`. -/
 107theorem U_conjTranspose (ev : DiscreteEvolution N) (t : ℝ) :
 108    (U ev t)ᴴ = U ev (-t) := by
 109  have hexp : ((t : ℂ) • gen ev)ᴴ = ((-t : ℝ) : ℂ) • gen ev := by
 110    rw [Matrix.conjTranspose_smul, gen_skewHermitian]
 111    simp [Complex.star_def, Complex.conj_ofReal, smul_neg, neg_smul, Complex.ofReal_neg]
 112  unfold U
 113  rw [← Matrix.exp_conjTranspose, hexp]
 114
 115/-- Unitarity: `(U ev t)^H * U ev t = 1` and `U ev t * (U ev t)^H = 1`. -/
 116theorem U_unitary (ev : DiscreteEvolution N) (t : ℝ) :
 117    (U ev t)ᴴ * U ev t = 1 ∧ U ev t * (U ev t)ᴴ = 1 := by
 118  refine ⟨?_, ?_⟩
 119  · rw [U_conjTranspose, U_add, neg_add_cancel, U_zero]
 120  · rw [U_conjTranspose, U_add, add_neg_cancel, U_zero]
 121
 122/-- The evolution lies in the unitary group of `C^N`. -/
 123theorem U_mem_unitaryGroup (ev : DiscreteEvolution N) (t : ℝ) :
 124    U ev t ∈ Matrix.unitaryGroup (Fin N) ℂ := by
 125  rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose]
 126  exact (U_unitary ev t).2
 127
 128/-! ## The discrete step is the first-order truncation of the exponential -/
 129
 130/-- The discrete evolution step of `HamiltonianEmergence` is exactly the first-order truncation
 131`(1 + gen ev) *v psi` of the exact unitary evolution `U ev 1 = exp(gen ev)`. This ties the existing
 132linear step to the operator exponential: `step` is the Euler / first-order approximation of the genuine
 133unitary recognition tick. -/
 134theorem step_eq_firstOrder (ev : DiscreteEvolution N) (ψ : DeviationHilbert N) :
 135    ev.step ψ = (1 + gen ev) *ᵥ ψ := by
 136  funext i
 137  rw [Matrix.add_mulVec, Matrix.one_mulVec, Pi.add_apply]
 138  have hg : (gen ev *ᵥ ψ) i
 139      = ∑ j, (-Complex.I) * ((ev.hamiltonian i j : ℂ) * ψ j) := by
 140    simp only [Matrix.mulVec, dotProduct, gen, Matrix.smul_apply, Hc, Matrix.of_apply,
 141      smul_eq_mul]
 142    exact Finset.sum_congr rfl (fun j _ => by ring)
 143  rw [hg, ← Finset.mul_sum]
 144  show ψ i - Complex.I * (∑ j, (ev.hamiltonian i j : ℂ) * ψ j)
 145      = ψ i + (-Complex.I) * ∑ j, (ev.hamiltonian i j : ℂ) * ψ j
 146  ring
 147
 148/-! ## Master certificate -/
 149
 150/-- **Finite-dimensional Stone generator certificate.** For any small-deviation Hamiltonian `ev` on
 151`C^N`, the recognition evolution is a genuine unitary one-parameter group generated by a self-adjoint
 152operator, and the existing discrete step is its first-order truncation:
 153
 154* `hamiltonian_hermitian`: the complexified Hamiltonian is self-adjoint;
 155* `generator_skewHermitian`: `gen = -i H-hat` is skew-Hermitian;
 156* `evolution_id` / `one_parameter_group`: `U` is a one-parameter group;
 157* `evolution_unitary` / `evolution_mem_unitary`: every `U t` is unitary;
 158* `discrete_step_is_first_order`: the `HamiltonianEmergence` step is `(1 + gen) *v psi`.
 159
 160Honest tag: CONDITIONAL THEOREM. The operator-level Stone structure is a kernel theorem; the
 161identification of the full nonlinear `R-hat` with this linearization to `O(eps^3)`, and the `8 tau_0 /
 162hbar` calibration of the tick, remain the named residuals. -/
 163structure StoneGeneratorCert (N : ℕ) (ev : DiscreteEvolution N) : Prop where
 164  hamiltonian_hermitian : (Hc ev).IsHermitian
 165  generator_skewHermitian : (gen ev)ᴴ = -(gen ev)
 166  evolution_id : U ev 0 = 1
 167  one_parameter_group : ∀ s t : ℝ, U ev s * U ev t = U ev (s + t)
 168  evolution_unitary : ∀ t : ℝ, (U ev t)ᴴ * U ev t = 1 ∧ U ev t * (U ev t)ᴴ = 1
 169  evolution_mem_unitary : ∀ t : ℝ, U ev t ∈ Matrix.unitaryGroup (Fin N) ℂ
 170  discrete_step_is_first_order :
 171    ∀ ψ : DeviationHilbert N, ev.step ψ = (1 + gen ev) *ᵥ ψ
 172
 173/-- The Stone generator certificate holds for every discrete-evolution Hamiltonian. -/
 174theorem stoneGeneratorCert (ev : DiscreteEvolution N) :
 175    StoneGeneratorCert N ev where
 176  hamiltonian_hermitian := Hc_isHermitian ev
 177  generator_skewHermitian := gen_skewHermitian ev
 178  evolution_id := U_zero ev
 179  one_parameter_group := U_add ev
 180  evolution_unitary := U_unitary ev
 181  evolution_mem_unitary := U_mem_unitaryGroup ev
 182  discrete_step_is_first_order := step_eq_firstOrder ev
 183
 184/-- **ONE-STATEMENT SUMMARY.** On the finite-dimensional recognition register `C^N`, the small-deviation
 185recognition evolution `U ev t = exp(t * (-i H-hat))` is a unitary one-parameter group generated by the
 186self-adjoint `H-hat`, and the discrete recognition step is its first-order truncation. -/
 187theorem operator_level_hamiltonian_emergence (ev : DiscreteEvolution N) :
 188    (Hc ev).IsHermitian ∧
 189      (gen ev)ᴴ = -(gen ev) ∧
 190      U ev 0 = 1 ∧
 191      (∀ s t : ℝ, U ev s * U ev t = U ev (s + t)) ∧
 192      (∀ t : ℝ, U ev t ∈ Matrix.unitaryGroup (Fin N) ℂ) ∧
 193      (∀ ψ : DeviationHilbert N, ev.step ψ = (1 + gen ev) *ᵥ ψ) :=
 194  ⟨Hc_isHermitian ev, gen_skewHermitian ev, U_zero ev, U_add ev, U_mem_unitaryGroup ev,
 195    step_eq_firstOrder ev⟩
 196
 197end
 198
 199end IndisputableMonolith.Foundation.HamiltonianEmergence
 200