structure
definition
IntegrationGapCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.IntegrationGap on GitHub at line 120.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
117
118/-! ## Master certificate -/
119
120structure IntegrationGapCert where
121 config_dim : configDim D = 5
122 parity_count : parityCount D = 9
123 gap_value : integrationGap D = 45
124 gap_minus_one : gapMinusOne D = 44
125 coprime_at_3 : Nat.Coprime (2 ^ D) (integrationGap D)
126 odd_coprime : ∀ k, Nat.Coprime (2 ^ (2*k+1)) ((2*k+1)^2 * (2*k+3))
127 even_not_coprime : ∀ k, 0 < k → ¬ Nat.Coprime (2^(2*k)) ((2*k)^2 * (2*k+2))
128
129theorem integrationGapCert : IntegrationGapCert where
130 config_dim := configDim_at_D3
131 parity_count := parityCount_at_D3
132 gap_value := integrationGap_at_D3
133 gap_minus_one := gapMinusOne_at_D3
134 coprime_at_3 := coprime_at_D3
135 odd_coprime := coprimality_odd
136 even_not_coprime := coprimality_even_fails
137
138end IntegrationGap
139end Foundation
140end IndisputableMonolith