pith. machine review for the scientific record. sign in
structure definition def or abbrev

CardinalitySpectrumCert

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)

 119structure CardinalitySpectrumCert where
 120  Dspatial_is_3 : Dspatial = 3
 121  Dconfig_is_5 : Dconfig = 5
 122  gap_as_D : gap45 = Dspatial^2 * Dconfig
 123  eightTick_as_D : eightTick = 2 ^ Dspatial
 124  cubeFaces_as_D : cubeFaces = twoFace * Dspatial
 125  full_turn : (360 : ℕ) = eightTick * gap45
 126  choose_central : (70 : ℕ) = Nat.choose 8 4
 127  D_cubed : (125 : ℕ) = Dconfig^3
 128  D_fifth : (3125 : ℕ) = Dconfig^5
 129  spectrum_length : rsSpectrum.length = 20
 130  spectrum_pairwise : rsSpectrum.Pairwise (· < ·)
 131  spectrum_bounded : ∀ n ∈ rsSpectrum, n ≤ 3125
 132

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.