pith. sign in
def

totalJcost

definition
show as:
module
IndisputableMonolith.Foundation.HamiltonianEmergence
domain
Foundation
line
54 · github
papers citing
none yet

plain-language theorem explainer

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.

Claim. Let $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

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.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.