Jcost_unit0
plain-language theorem explainer
The lemma establishes that the recognition cost J vanishes at the fixed point unity. Acoustics and action-space researchers cite it to confirm zero penalty for matched frequencies or constant admissible paths. The proof is a direct simplification that unfolds the definition of Jcost and reduces the expression to zero.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then $J(1) = 0$.
background
In the Cost.JcostCore module, Jcost is introduced as the noncomputable function $J(x) = (x + x^{-1})/2 - 1$. This expression is the core cost measure of Recognition Science and is equivalent to the squared-ratio form $J(x) = (x-1)^2/(2x)$. The local setting treats Jcost as the base cost function whose minimum occurs at the self-similar fixed point 1. An upstream result records the alternative algebraic identity $J(x) = (x-1)^2/(2x)$.
proof idea
This is a one-line wrapper that applies simp to the definition of Jcost.
why it matters
The result anchors the zero-cost point that feeds forty downstream declarations, including pitchCost_at_unison (zero cost for identical frequencies), actionJ_const_one (vanishing action on constant paths), and hearingLossPenalty_zero. It supplies the base case required by the J-uniqueness step in the forcing chain and enables the quadratic Taylor expansion near the minimum. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Massive constant activations act as fixed biases in LLMs
"their values largely stay constant regardless of the input, and they function as indispensable bias terms in LLMs"
-
Fine-tuning a 175B model needs only a rank-2 update
"We use a random Gaussian initialization for A and zero for B, so ΔW = BA is zero at the beginning of training. We then scale ΔW x by α/r."