Foundation Hamiltonian Emergence Operator Gen Skew Hermitian

The skew-Hermitian generator

In quantum mechanics, the time evolution of a system is generated by an operator that must satisfy a specific algebraic condition: its adjoint (the complex-conjugate transpose) equals its negative. Such an operator is called skew-Hermitian. This condition is what guarantees that the evolution it generates preserves total probability, a property known as unitarity. The declaration gen_skewHermitian in the Recognition Science library proves that a particular matrix, built from the framework's Hamiltonian, satisfies exactly this condition.

The framework models recognition dynamics on a finite-dimensional state space, denoted C^N, where N is the size of its eight-tick register. Within this setting, the relevant Hamiltonian is a real symmetric matrix, which becomes Hermitian when viewed as a complex matrix. The generator is then defined as the product of this Hermitian matrix with the imaginary unit i and a minus sign, written as gen = -i * Hc. The theorem gen_skewHermitian establishes that this generator is indeed skew-Hermitian, meaning its conjugate transpose equals its negative.

This single algebraic fact supports a larger structural result. From it, the library derives that the exponential family U(t) = exp(t * gen) forms a one-parameter group: it satisfies the identities U(0) = 1 and U(s)U(t) = U(s+t). Also, each U(t) is unitary, meaning it preserves inner products. The discrete evolution step used elsewhere in the framework is then shown to be exactly the first-order truncation of this exponential, connecting the discrete and continuous pictures.

The theorem is proved in the machine-checked library with no axioms beyond the standard logical ones. However, what this theorem does not establish is worth spelling out. It does not prove that the full nonlinear recognition operator equals this linear evolution to higher order. That identification remains a conditional hypothesis, depending on a scalar approximation bound and a modeling choice about how the nonlinear operator linearizes. The calibration of the time step, involving the constant 8 tau_0 / hbar, also remains a named residual rather than a derived result.

What the theorem does provide is a rigorous foundation for the operator-level claim that quantum mechanics emerges as the high-frequency limit of recognition dynamics. Within the finite-dimensional setting, the generator structure is not a placeholder but a proved fact. This turns a previously cited infinite-dimensional theorem, which was not available in the library, into a finite-dimensional result that is fully verified.

/-- The generator is skew-Hermitian: `(gen)^H = -gen`. This is the defining property of the generator
of a unitary one-parameter group. -/
theorem gen_skewHermitian (ev : DiscreteEvolution N) :
    (gen ev)ᴴ = -(gen ev) := by
  have hH : (Hc ev)ᴴ = Hc ev := (Hc_isHermitian ev).eq
  unfold gen
  rw [Matrix.conjTranspose_smul, hH]
  have hstar : star (-Complex.I) = Complex.I := by
    rw [star_neg, Complex.star_def, Complex.conj_I, neg_neg]
  rw [hstar, neg_smul, neg_neg]

/-- One-parameter group law: `U ev s * U ev t = U ev (s + t)`. -/
theorem U_add (ev : DiscreteEvolution N) (s t : ℝ) :
    U ev s * U ev t = U ev (s + t) := by
  have hcomm : Commute ((s : ℂ) • gen ev) ((t : ℂ) • gen ev) :=
    ((Commute.refl (gen ev)).smul_left (s : ℂ)).smul_right (t : ℂ)
  unfold U
  rw [← Matrix.exp_add_of_commute ℂ _ _ hcomm]
  congr 1
  rw [← add_smul, ← Complex.ofReal_add]

/-- Identity at `t = 0`: `U ev 0 = 1`. -/
theorem U_zero (ev : DiscreteEvolution N) : U ev 0 = 1 := by
  unfold U
  rw [Complex.ofReal_zero, zero_smul, exp_zero]

/-- Unitarity: `(U ev t)^H * U ev t = 1` and `U ev t * (U ev t)^H = 1`. -/
theorem U_unitary (ev : DiscreteEvolution N) (t : ℝ) :
    (U ev t)ᴴ * U ev t = 1 ∧ U ev t * (U ev t)ᴴ = 1 := by
  refine ⟨?_, ?_⟩
  · rw [U_conjTranspose, U_add, neg_add_cancel, U_zero]
  · rw [U_conjTranspose, U_add, add_neg_cancel, U_zero]

/-- The discrete evolution step of `HamiltonianEmergence` is exactly the first-order truncation
`(1 + gen ev) *v psi` of the exact unitary evolution `U ev 1 = exp(gen ev)`. This ties the existing
linear step to the operator exponential: `step` is the Euler / first-order approximation of the genuine
unitary recognition tick. -/
theorem step_eq_firstOrder (ev : DiscreteEvolution N) (ψ : DeviationHilbert N) :
    ev.step ψ = (1 + gen ev) *ᵥ ψ := by
  funext i
  rw [Matrix.add_mulVec, Matrix.one_mulVec, Pi.add_apply]
  have hg : (gen ev *ᵥ ψ) i
      = ∑ j, (-Complex.I) * ((ev.hamiltonian i j : ℂ) * ψ j) := by
    simp only [Matrix.mulVec, dotProduct, gen, Matrix.smul_apply, Hc, Matrix.of_apply,
      smul_eq_mul]
    exact Finset.sum_congr rfl (fun j _ => by ring)
  rw [hg, ← Finset.mul_sum]
  show ψ i - Complex.I * (∑ j, (ev.hamiltonian i j : ℂ) * ψ j)
      = ψ i + (-Complex.I) * ∑ j, (ev.hamiltonian i j : ℂ) * ψ j
  ring

What this page does not claim

The full nonlinear recognition operator equals this linear evolution to O(eps^3). The time step calibration 8 tau_0 / hbar is derived rather than assumed. The theorem applies to infinite-dimensional state spaces.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/HamiltonianEmergenceOperator.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: