H_HamiltonianIsGenerator
plain-language theorem explainer
The declaration packages the scalar emergence hypothesis: for each natural number N there exists a discrete evolution operator such that the total J-cost of any small-deviation state differs from its quadratic energy by at most a cubic remainder. Physicists deriving quantum Hamiltonians from recognition dynamics cite this as the proved scalar foundation. The definition is a direct existential statement over the DiscreteEvolution structure and the explicit cubic bound from the J-cost expansion.
Claim. For each natural number $N$, the hypothesis holds if there exists a symmetric real $N$-by-$N$ matrix serving as discrete evolution generator such that, for every small-deviation state $s$ with components $|ε_i|≤1/2$, the difference between the sum of $J(1+ε_i)$ and the quadratic form $½Σε_i²$ is bounded by twice the sum of $|ε_i|^3$.
background
The HamiltonianEmergence module shows that the Recognition Operator produces an effective Hamiltonian in the small-strain regime. SmallDeviationState is the structure of bond multipliers $1+ε_i$ with $|ε_i|≤1/2$. totalJcost sums the per-bond J-cost values $J(1+ε_i)$, while quadraticEnergy extracts the leading quadratic term $½Σε_i²$. DiscreteEvolution is the structure carrying a symmetric real matrix that defines the linearized step on DeviationHilbert states. The module already proves the expansion $J(1+ε)=ε²/2+O(ε³)$ and uses it to state the generator hypothesis.
proof idea
This is a definition that directly encodes the existential claim. It references only the prior definitions of totalJcost, quadraticEnergy, SmallDeviationState, and DiscreteEvolution; no additional lemmas or tactics are applied.
why it matters
The definition supplies the scalar hypothesis discharged by the downstream theorem emergence_scalar_proved, which witnesses it with diagonalHamiltonian and the totalJcost_approx_quadratic bound. It completes the scalar foundation step in the emergence roadmap, connecting the quadratic J-cost form (from J-uniqueness) to the generator of discrete Schrödinger evolution. The operator-level claim that this generator is self-adjoint via a discrete Stone theorem remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.