jcost_hessian
plain-language theorem explainer
The declaration establishes that the Hessian of the J-cost function at equilibrium equals 1. Researchers deriving the simple harmonic oscillator from recognition cost would cite this calibration. The proof is a one-line term application of trivial, resting on the direct evaluation J''(1) = 1.
Claim. The second derivative of the J-cost function at the equilibrium point satisfies $J''(1) = 1$.
background
The module shows that the simple harmonic oscillator potential arises as the leading-order expansion of J-cost near the matched point: J(1 + ε) = ε²/2 + O(ε³). This fixes the spring constant k = J''(1) = 1 for any recognition pattern oscillating near equilibrium. In RS units the angular frequency then becomes ω = φ^{5/2} once the coherent mass scale is inserted.
proof idea
The proof is a one-line term proof that applies the trivial tactic. It directly asserts the Hessian calibration without expansion, relying on the prior evaluation that the second derivative of J at 1 is 1.
why it matters
This result supplies the Hessian calibration that lets the oscillatory dynamics module derive ω_RS = φ^{5/2} and the energy levels E_n = φ^{-5/2}(n + 1/2). It fills the structural step linking J-cost to the harmonic oscillator in the Recognition framework and connects to the J-uniqueness property from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.