totalJcost
plain-language theorem explainer
Total bond cost aggregates the J-cost of each ratio v/n across a list of neighbors. Researchers on the F1 foundation paper or discrete vorticity models cite this definition when summing bond energies. It is realized as a direct summation after mapping each neighbor through the J-cost function on the normalized ratio.
Claim. Let $J(x) = ½(x + x^{-1}) - 1$. For a reference value $v$ and neighbors $n_1, …, n_k$, the total bond cost is $∑_i J(v/n_i)$.
background
The F1 module develops log-domain geometry for the reciprocal cost $J(x) = ½(x + x^{-1}) - 1$. It collects identities from JcostCore, including the identity $J(e^ε) = cosh(ε) - 1$ and the fact that the geometric mean minimizes total cost. The present definition extends the per-bond cost to a sum over an arbitrary neighbor list, matching the scalar energy needed for the foundation paper.
proof idea
One-line definition that maps each neighbor n to Jcost(v/n) and sums the resulting list.
why it matters
This definition supplies the total cost appearing in the quadratic approximation theorem and the non-negativity theorem of HamiltonianEmergence. It implements F1.2.3 in the log-domain J-cost geometry section. The result supports the hypothesis that the Recognition Operator generates a self-adjoint Hamiltonian in the small-deviation limit by furnishing the scalar sum. It sits inside the T5–T8 forcing chain through the J-uniqueness property and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.