pith. machine review for the scientific record. sign in
theorem proved term proof

hilbert_polya_candidate_certificate

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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) :=

proof body

Term-mode proof.

 295  ⟨costAt_neg_eq,
 296   involutionOp_involutive,
 297   involutionOp_diagOp_comm,
 298   involutionOp_shiftOp,
 299   shiftOp_shiftInvOp,
 300   involutionOp_candidateOp⟩
 301
 302end
 303
 304end HilbertPolyaCandidate
 305end NumberTheory
 306end IndisputableMonolith

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more