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

integrationGapCert

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)

 129theorem integrationGapCert : IntegrationGapCert where
 130  config_dim := configDim_at_D3

proof body

Term-mode proof.

 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

depends on (8)

Lean names referenced from this declaration's body.