diagOp_single
plain-language theorem explainer
The diagonal cost operator multiplies the coefficient of each basis vector by the recognition cost J at its multiplicative index. Researchers constructing Hilbert-Pólya candidates would cite this to confirm the operator's explicit action on the free module. The proof is a one-line simplification that unfolds the operator definition and uses commutativity of real multiplication.
Claim. Let $v$ be a multiplicative index and $c$ a real scalar. The diagonal operator $D$ satisfies $D(c e_v) = c J(v) e_v$, where $J(v)$ is the recognition cost at the positive rational corresponding to $v$.
background
MultIndex is the free abelian group on the primes, realized as finitely supported maps from primes to integers; toRat converts each index to the corresponding positive rational. costAt assigns to each index the value of the J-cost function, which satisfies the Recognition Composition Law and is strictly convex with minimum at 1. diagOp is the diagonal operator on the free real module StateSpace that multiplies the basis vector at index $v$ by this cost value.
proof idea
The proof is a one-line wrapper that applies the definition of diagOp together with commutativity of multiplication on the reals.
why it matters
This theorem verifies the explicit action of the diagonal cost operator on basis elements, which is presupposed by the module's main results on commutation with the involution and invertibility of prime shifts. It fills the definitional step in the algebraic skeleton for a Hilbert-Pólya candidate built from the J-cost, as stated in the module documentation. The construction links directly to the reciprocal symmetry J(x) = J(1/x) and the Recognition Science forcing chain through the upstream J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.