module module

`IndisputableMonolith.NumberTheory.HilbertPolyaCandidate`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.NumberTheory.CostOperatorRegularity module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (29)

abbrev MultIndex L60
def toRat L64
def costAt L68
theorem toRat_zero L70
theorem toRat_pos L73
theorem toRat_add L81
theorem toRat_neg L92
theorem costAt_neg_eq L102
abbrev StateSpace L110
def diagOp L122
theorem diagOp_single L126
def shiftOp L134
theorem shiftOp_single L138
def shiftInvOp L145
theorem shiftInvOp_single L148
def involutionOp L155
theorem involutionOp_single L158
theorem involutionOp_involutive L165
theorem involutionOp_diagOp_comm L171
theorem involutionOp_shiftOp L181
theorem involutionOp_shiftInvOp L191
theorem shiftOp_shiftInvOp L202
theorem shiftInvOp_shiftOp L211
def primeHop L224
theorem involutionOp_primeHop L229
def candidateOp L243
theorem involutionOp_sum_primeHop L249
theorem involutionOp_candidateOp L268
theorem hilbert_polya_candidate_certificate L279