involutionOp_candidateOp

formal source

 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 :
 280    -- (1) Reciprocal symmetry of the cost at the index level.
 281    (∀ (v : MultIndex), costAt (-v) = costAt v) ∧
 282    -- (2) The reciprocal involution is involutive.
 283    (involutionOp ∘ₗ involutionOp = LinearMap.id) ∧
 284    -- (3) The diagonal cost operator commutes with the involution.
 285    (involutionOp ∘ₗ diagOp = diagOp ∘ₗ involutionOp) ∧
 286    -- (4) Each prime shift inverts under the involution.
 287    (∀ (p : Nat.Primes),
 288      involutionOp ∘ₗ shiftOp p = shiftInvOp p ∘ₗ involutionOp) ∧
 289    -- (5) Shifts are formally unitary.
 290    (∀ (p : Nat.Primes),
 291      shiftOp p ∘ₗ shiftInvOp p = LinearMap.id) ∧
 292    -- (6) The full candidate operator commutes with the involution.
 293    (∀ (S : Finset Nat.Primes) (lam : Nat.Primes → ℝ),
 294      involutionOp ∘ₗ candidateOp S lam = candidateOp S lam ∘ₗ involutionOp) :=
 295  ⟨costAt_neg_eq,
 296   involutionOp_involutive,
 297   involutionOp_diagOp_comm,
 298   involutionOp_shiftOp,