diagonalHamiltonian
plain-language theorem explainer
The definition supplies the diagonal matrix with unit entries on the diagonal as the Hamiltonian generator for discrete evolution of small deviations. Researchers deriving Schrödinger dynamics from the quadratic regime of the recognition cost function cite this construction. It is realized by a direct case split on matrix indices that satisfies the symmetry axiom of DiscreteEvolution without external lemmas.
Claim. The diagonal Hamiltonian matrix on an $N$-dimensional deviation space is the real $N$ by $N$ matrix $H$ with entries $H_{ij} = 1$ when $i = j$ and $H_{ij} = 0$ otherwise. The constant 1 is fixed by the calibration $J''(1) = 1$ of the J-cost function at equilibrium.
background
The Hamiltonian Emergence module linearizes the Recognition Operator near states where the argument of the J-cost equals 1. DiscreteEvolution is the structure that packages a real symmetric matrix $H$ together with the linearized step map that approximates one application of the recognition dynamics on deviation vectors in the embedded Hilbert space. The J-cost expansion $J(1 + ε) = ε²/2 + O(ε³)$ supplies the quadratic form whose second derivative at unity calibrates the diagonal entries to 1. Upstream ledger factorization and arithmetic embedding results fix the positive-real normalization of J that makes this derivative exactly 1.
proof idea
The definition directly constructs the DiscreteEvolution record by setting the hamiltonian field to the Kronecker delta via a conditional expression and discharging the symmetry requirement with a two-case split on index equality. No upstream lemmas beyond basic equality rewriting are required.
why it matters
This definition supplies the concrete matrix that appears inside the proved scalar emergence theorem, which packages it with the quadratic J-cost approximation to discharge the scalar half of the emergence hypothesis. It realizes the J-uniqueness calibration at the operator level and closes the scalar foundation for the claim that recognition dynamics reduce to discrete Schrödinger evolution near equilibrium. The full operator statement remains conditional on discrete Stone theory, which is noted as absent from the current library.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.