JlogN
plain-language theorem explainer
JlogN defines the n-dimensional cost in log coordinates by composing the scalar J-cost with the exponential of the weighted dot product of the input vectors. Researchers extending scalar recognition costs to vector settings in the Recognition Science framework would cite this when deriving multi-component results. The definition is a direct one-line composition that applies the scalar cost to exp of the aggregate.
Claim. For vectors $α, t ∈ ℝ^n$, the log-coordinate cost is defined as $J( exp(α · t) )$, where $J$ is the scalar cost function and $·$ denotes the weighted dot product $∑ α_i t_i$.
background
Vec n denotes n-component real vectors as functions from Fin n to ℝ. The dot product is the weighted sum ∑_{i:Fin n} α i * t i, which aggregates the log coordinates. The module lifts the scalar kernel through this weighted log aggregate to obtain the n-dimensional reciprocal cost. Upstream, the cost function from MultiplicativeRecognizerL4 is the derived cost of its comparator on positive ratios, while the cost from ObserverForcing is the J-cost of a recognition event state.
proof idea
One-line wrapper that applies the scalar Jcost to the exponential of the dot product dot α t.
why it matters
This definition underpins JcostN and its derived theorems including JcostN_eq_cosh_logsum, JcostN_eq_zero_iff, and JcostN_unit. It fills the extension of scalar cost to log coordinates in the N-dimensional reciprocal cost module. The construction connects to the Recognition Composition Law and the forcing chain steps that derive D=3 dimensions from the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.