JcostN_reciprocal
plain-language theorem explainer
The n-dimensional J-cost is invariant under componentwise inversion of its vector argument. Workers extending the scalar Recognition Science cost to multiple components cite this reciprocity to confirm symmetry preservation. The term proof rewrites both sides via the cosh-logsum identity, applies the sign flip of the weighted log aggregate under inversion, and invokes evenness of cosh.
Claim. For weight vector $α$ and positive vector $x$ in $ℝ^n$, the n-dimensional cost satisfies $JcostN(α, x^{-1}) = JcostN(α, x)$, where $x^{-1}$ is the componentwise reciprocal.
background
The module lifts the scalar J-kernel to n dimensions by replacing the single log argument with a weighted aggregate over component logs. Vec n is the type of n-component real vectors, written as functions Fin n → ℝ. JcostN α x is defined as JlogN α (logVec x) and equals cosh(dot α (logVec x)) − 1 by the upstream identity JcostN_eq_cosh_logsum. hadamardInv x supplies the componentwise reciprocal, and dot_log_hadamardInv records that the weighted log aggregate of the reciprocal equals the negative of the original aggregate.
proof idea
Term-mode reduction. Rewrite both sides with JcostN_eq_cosh_logsum to obtain cosh of the weighted log-dot product on each side. Apply dot_log_hadamardInv to replace the inverted aggregate by its negative, then close with Real.cosh_neg.
why it matters
The result embeds the scalar inversion symmetry J(x) = J(1/x) into the n-dimensional cost, a direct consequence of the cosh(log ·) form that appears in the Recognition Science forcing chain. It belongs to the core definitions that build the multi-component cost before any aggregation or positivity lemmas are applied. No downstream uses are recorded, leaving the property available for later invariance arguments in the cost domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.