SmallDeviationState
plain-language theorem explainer
The small deviation state structure defines a vector of real numbers ε_i for N components, each satisfying |ε_i| ≤ 1/2, to represent configurations near equilibrium with bond multipliers 1 + ε_i. Researchers deriving emergent Hamiltonians from recognition dynamics cite this to set up the quadratic J-cost approximation. It is introduced as a direct structure declaration without any proof steps.
Claim. A configuration with $N$ real deviations $ε_i$ (for $i=0,…,N-1$) qualifies as a small deviation state precisely when $|ε_i|≤1/2$ holds for each $i$.
background
The HamiltonianEmergence module shows how the quantum Hamiltonian arises as the small deviation limit of the Recognition Operator. For states near equilibrium the J cost expands as J(1 + ε) = ε²/2 + O(ε³), making the quadratic term the emergent kinetic energy. The small deviation state structure supplies the domain for this expansion. Upstream, the cost function is defined via the multiplicative recognizer comparator and the J cost core.
proof idea
This is a direct structure definition. The deviations field maps each index in Fin N to a real number, and the small predicate enforces the uniform bound of 1/2. No tactics or lemmas are invoked.
why it matters
It supplies the type for quadraticEnergy, which extracts the leading ε²/2 term, and for the hypothesis that the Recognition Operator generates a self adjoint Hamiltonian. This completes the scalar part of the emergence argument, resting on the J uniqueness from the forcing chain and the Recognition Composition Law. The remaining gap is the full operator emergence requiring discrete Stone theorem infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.