`cardinalitySpectrumCert`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.CardinalitySpectrum
domain: CrossDomain
line: 133 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.CardinalitySpectrum on GitHub at line 133.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 130  spectrum_pairwise : rsSpectrum.Pairwise (· < ·)
 131  spectrum_bounded : ∀ n ∈ rsSpectrum, n ≤ 3125
 132
 133def cardinalitySpectrumCert : CardinalitySpectrumCert where
 134  Dspatial_is_3 := rfl
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.