gradientEntry
plain-language theorem explainer
The log-coordinate gradient entry for the n-dimensional cost JlogN is the product of the i-th weight component α_i and sinh of the weighted dot product α · t. Researchers deriving the rank-one Hessian of the reciprocal cost in log-coordinates cite this definition when assembling gradient and second-derivative tensors. The definition is a direct algebraic expression that multiplies the selected component of α by sinh applied to the scalar aggregate from dot.
Claim. The i-th entry of the gradient of $JlogN(α, t)$ equals $α_i sinh(α · t)$, where $α · t = ∑_{i=1}^n α_i t_i$ is the weighted dot product and $JlogN(α, t) = Jcost(exp(α · t))$.
background
The module supplies explicit formulas for the Hessian of the n-dimensional reciprocal cost. In log-coordinates this cost depends only on the single scalar aggregate dot α t, which forces the Hessian to be rank one and to factor through the outer product α ⊗ α. Vec n is the type of n-component real vectors, written as maps from Fin n to ℝ. The weighted dot product is defined by summation: dot α t := ∑_i α_i t_i. JlogN α t is obtained by composing the original positive-coordinate cost Jcost with the exponential of that dot product.
proof idea
One-line definition that directly multiplies the i-th component of α by sinh of the scalar returned by dot α t.
why it matters
This supplies the explicit gradient entries required to build the Hessian matrix and related operators (hessianEntry, applyHessian) for the log-coordinate cost. It realizes the rank-one factorization implied by dependence on a single aggregate, consistent with the J-uniqueness and self-similar fixed-point structure in the forcing chain. The definition closes part of the cost-analysis scaffolding referenced by Metric.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.