 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]
 274
 275/-! ## Master certificate -/
 276
 277/-- Master certificate: the structural properties of the candidate
 278    Hilbert--Pólya operator that this module establishes. -/
 279theorem hilbert_polya_candidate_certificate :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.