pith. machine review for the scientific record. sign in
def 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)

 133def cardinalitySpectrumCert : CardinalitySpectrumCert where
 134  Dspatial_is_3 := rfl

proof body

Definition body.

 135  Dconfig_is_5 := rfl
 136  gap_as_D := gap45_eq
 137  eightTick_as_D := eightTick_eq
 138  cubeFaces_as_D := cubeFaces_eq
 139  full_turn := threeSixty_is_tick_gap
 140  choose_central := seventy_is_choose_8_4
 141  D_cubed := oneTwentyFive_is_Dcubed
 142  D_fifth := threeOne25_is_D_fifth
 143  spectrum_length := rsSpectrum_length
 144  spectrum_pairwise := rsSpectrum_pairwise_lt
 145  spectrum_bounded := rsSpectrum_bounded
 146
 147end IndisputableMonolith.CrossDomain.CardinalitySpectrum

depends on (15)

Lean names referenced from this declaration's body.