Foundation Hamiltonian Emergence Operator Stone Generator Cert

The Stone generator certificate

In quantum mechanics, the time evolution of a system is generated by a Hermitian operator, the Hamiltonian, through the exponential map. The Stone generator certificate is a formal result that establishes this structure for the linearized recognition dynamics in the Recognition Science framework. It proves that, on a finite-dimensional state space, the evolution family is a genuine unitary one-parameter group, and that the discrete step used in the framework is exactly its first-order truncation.

The framework models recognition dynamics as a discrete evolution on a finite-dimensional register, the recognition register (a discrete record of possible states). The certificate proves that for any small-deviation Hamiltonian, the complexified Hamiltonian is Hermitian, and the generator is skew-Hermitian. Consequently, the evolution family U(t) = exp(t * gen) satisfies the group law, is unitary at every time, and lies in the unitary group. The discrete step, previously defined as psi - i * H * psi, is shown to be exactly the first-order term of the exponential expansion.

This result is a conditional theorem. The Stone-generator structure is a kernel theorem, verified with zero axioms. What remains conditional is the identification that the full nonlinear evolution operator equals this linearization to third order, which rests on a proved scalar bound plus a modeling choice. The exact operator Taylor bound and the calibration of the tick remain named residuals.

The certificate does not claim that the full nonlinear evolution is exactly exponential, nor that the Hamiltonian is derived from first principles. It establishes the operator-level structure for the linearized dynamics, providing the mathematical foundation for treating recognition dynamics as a quantum-like evolution in the high-frequency limit.

/-- The complexified Hamiltonian is Hermitian: a real symmetric matrix is self-adjoint over `C`. -/
theorem Hc_isHermitian (ev : DiscreteEvolution N) : (Hc ev).IsHermitian := by
  show (Hc ev)ᴴ = Hc ev
  ext i j
  simp only [Matrix.conjTranspose_apply, Hc, Matrix.of_apply, Complex.star_def,
    Complex.conj_ofReal]
  norm_cast
  exact ev.symmetric j i

/-- 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]

/-- 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 certificate does not prove that the full nonlinear evolution operator equals the linearization to third order. It does not derive the Hamiltonian from first principles; it establishes the operator structure for a given small-deviation Hamiltonian. It does not claim that the discrete step is exact; it is the first-order approximation of the exponential.

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: