hamiltonian_emergence
plain-language theorem explainer
Near balance, recognition cost expands as J(1+ε)=ε²/2 + c ε³ with |c|≤2 whenever |ε|≤1/2. The quadratic piece is the kinetic term of the canonical Hamiltonian in the T5–T7 bridge. Cited by the unified forcing chain's Hamiltonian-emergence bridge. Proof is a one-line wrapper of the Cost-library expansion of J about 1.
Claim. Let $J(x)=(x+x^{-1})/2-1$. For every real $\varepsilon$ with $|\varepsilon|\le 1/2$, there exists $c\in\mathbb{R}$ with $|c|\le 2$ such that $J(1+\varepsilon)=\varepsilon^2/2+c\,\varepsilon^3$.
background
The module Complex Structure Forcing starts from the forced eight-tick shift (T7): a cyclic operator $T$ on ledger states with $T^8=I$. Its eigenvalues are eighth roots of unity; $\omega^2=i$ has no real representative, so diagonalization forces $\mathbb{C}$. DFT-8 is the canonical unitary change of basis, and $J$-cost is phase-invariant (depends on modulus only).
The recognition cost is the unique T5 functional $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Balance is the fixed point $x=1$, where $J(1)=0$. Small ledger deviations are written $x=1+\varepsilon$. The present statement is the local Taylor control of $J$ in that chart: leading term $\varepsilon^2/2$, cubic remainder with uniform coefficient bound on $|\varepsilon|\le 1/2$.
Upstream, Jcost and its one-plus-eps quadratic expansion in the Cost library supply the algebraic identity; tick/$\tau_0$ fix the RS time unit but do not enter the expansion itself.
proof idea
One-line wrapper: apply Cost.Jcost_one_plus_eps_quadratic at the given $\varepsilon$ and the hypothesis $|\varepsilon|\le 1/2$. That lemma returns the witness $c$ together with the identity $J(1+\varepsilon)=\varepsilon^2/2+c\varepsilon^3$ and the bound $|c|\le 2$. No further rewriting is done in this declaration.
why it matters
In the module summary this is item 12: the Hamiltonian emerges as the quadratic small-deviation form of $J$. Downstream, t5_t7_to_canonical_hamiltonian_bridge_holds packages it as hamiltonian_quadratic_emergence under hypotheses T5 (J-uniqueness) and T7 (eight-tick), alongside cost_phase_duality. That bridge is the forcing-chain step that turns the unique cost and the octave period into a canonical kinetic Hamiltonian.
Framework landmarks: T5 fixes $J$; T7 supplies the eight-tick operator whose complex eigenstructure the module forces; the expansion $J(1+\varepsilon)\approx\varepsilon^2/2$ is the local energy that unitarity and phase invariance act on. The doc-comment states the interpretation directly: the quadratic form is the Hamiltonian kinetic energy. Status is still scaffolding until the Cost expansion it wraps is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.