diagOp
plain-language theorem explainer
The diagonal cost operator D scales each basis vector e_v in the free real module over multiplicative indices by the Recognition J-cost at the corresponding positive rational. Researchers constructing algebraic candidates for the Hilbert-Pólya operator cite this as the diagonal term whose spectrum is conjectured to yield the imaginary parts of zeta zeros. The definition is a direct linear sum that applies costAt pointwise via Finsupp.lsum.
Claim. The linear endomorphism $D$ of the free real module on multiplicative indices satisfies $D(e_v) = J(r(v)) e_v$ for each basis vector $e_v$, where $r(v)$ denotes the positive rational associated to index $v$ and $J(x) = (x + x^{-1})/2 - 1$.
background
StateSpace is the free real module on MultIndex, the free abelian group on primes that parametrizes positive rationals via toRat. costAt assigns to each index the value J(toRat v), with J the Recognition cost function obeying the composition law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and fixed by the phi-ladder. The module constructs an algebraic skeleton for a candidate Hilbert-Pólya operator on this space, using the reciprocal symmetry J(q) = J(1/q) to ensure commutation with the involution that mirrors the zeta functional equation.
proof idea
One-line definition that applies Finsupp.lsum to the family of scaled single maps, with each coefficient supplied by costAt. No lemmas are invoked beyond the standard linear-map constructors imported from Mathlib.
why it matters
diagOp supplies the diagonal term inside candidateOp and is invoked by hilbert_polya_candidate_certificate and involutionOp_diagOp_comm. It realizes the J-cost operator at the algebraic level, encoding T5 J-uniqueness and the eight-tick octave symmetry inside the candidate whose spectrum is left open. The module doc states that the construction proves structural symmetries but does not prove the spectrum equals the imaginary parts of zeta zeros.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.