candidateOp

formal source

 240    The full operator (sum over all primes) requires choosing a Hilbert space
 241    closure and analyzing convergence; we work here at the algebraic level
 242    with a finite truncation. -/
 243def candidateOp (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ) :
 244    StateSpace →ₗ[ℝ] StateSpace :=
 245  diagOp + S.sum (fun p => lam p • primeHop p)
 246
 247/-- Auxiliary: involution commutes with weighted sum of `primeHop` over a finset.
 248    Proved by induction on the finset. -/
 249private theorem involutionOp_sum_primeHop
 250    (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ) :
 251    involutionOp ∘ₗ S.sum (fun p => lam p • primeHop p)
 252      = S.sum (fun p => lam p • primeHop p) ∘ₗ involutionOp := by
 253  classical
 254  refine Finset.induction_on S ?_ ?_
 255  · simp
 256  · intro p S hp ih
 257    rw [Finset.sum_insert hp]
 258    rw [LinearMap.comp_add, LinearMap.add_comp, ih]
 259    congr 1
 260    rw [LinearMap.comp_smul, LinearMap.smul_comp]
 261    congr 1
 262    exact involutionOp_primeHop p
 263
 264/-- The candidate operator commutes with the reciprocal involution.
 265    This is the Hilbert--Pólya-style structural symmetry: any spectrum
 266    of the (closure of the) operator decomposes into eigenspaces of
 267    the involution, mirroring `s ↔ 1-s`. -/
 268theorem involutionOp_candidateOp (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ) :
 269    involutionOp ∘ₗ candidateOp S lam = candidateOp S lam ∘ₗ involutionOp := by
 270  unfold candidateOp
 271  rw [LinearMap.comp_add, LinearMap.add_comp]
 272  rw [involutionOp_diagOp_comm]
 273  rw [involutionOp_sum_primeHop]