totalJcost
The total J-cost for a small-deviation state sums the individual J-cost of each bond multiplier 1 plus its deviation component. Researchers deriving the emergent Hamiltonian from the recognition operator cite this definition when reducing dynamics to quadratic energy near equilibrium. The definition is a direct finite sum over the deviation components using the base cost function.
claimLet $s$ be a small-deviation state on $N$ bonds with deviations $ε_i$ satisfying $|ε_i| ≤ 1/2$. The total J-cost is $∑_{i=1}^N J(1 + ε_i)$, where $J$ denotes the recognition cost function.
background
The Hamiltonian Emergence module shows that the Recognition Operator reduces to a quadratic form near equilibrium. A small-deviation state consists of a vector of deviations $ε_i$ with $|ε_i| ≤ 1/2$, so that bond multipliers remain close to unity. The J-cost function $J(x)$ measures recognition cost of a multiplier $x$, and upstream results establish that $J(1 + ε)$ expands as $ε²/2$ plus higher-order terms.
proof idea
The definition computes the sum over the finite set of all indices, applying the base J-cost function to each term 1 plus the corresponding deviation. It is a direct aggregation with no lemmas or tactics required.
why it matters in Recognition Science
This definition supplies the left-hand side for the approximation theorem that bounds the difference from quadratic energy by a sum of cubic terms. It underpins the hypothesis that the Recognition Operator generates a self-adjoint Hamiltonian in the small-deviation limit. The module connects the scalar sum to the forcing chain steps where J-uniqueness forces the phi fixed point, the eight-tick octave, and three spatial dimensions, while the alpha inverse band arises from the same Recognition Composition Law.
scope and limits
- Does not prove the quadratic approximation or remainder bounds.
- Does not define the base J-cost function, which is imported from core modules.
- Does not address time evolution or the unitary approximation.
- Does not apply to states with large deviations.
- Does not establish non-negativity of the total cost.
formal statement (Lean)
54def totalJcost (s : SmallDeviationState N) : ℝ :=
proof body
Definition body.
55 Finset.univ.sum fun i => Jcost (1 + s.deviations i)
56
57/-! ## Quadratic Emergence (PROVED) -/
58
59/-- The scalar J-cost expansion: J(1+ε) = ε²/2 + c·ε³ with |c| ≤ 2.
60 This is the fundamental lemma: J-cost IS a quadratic form near unity. -/