`hilbert_polya_candidate_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.HilbertPolyaCandidate
domain: NumberTheory
line: 279 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.HilbertPolyaCandidate on GitHub at line 279.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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,
 299   shiftOp_shiftInvOp,
 300   involutionOp_candidateOp⟩
 301
 302end
 303
 304end HilbertPolyaCandidate
 305end NumberTheory
 306end IndisputableMonolith

papers checked against this theorem

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