module module moderate

`IndisputableMonolith.CrossDomain.CardinalitySpectrum`

The CardinalitySpectrum module establishes D_spatial equals three via cardinality relations across domains. Researchers working on the T0-T8 forcing chain cite it when closing the spatial dimension step. The module organizes a collection of definitions and equalities without internal proofs.

claim$D_ {spatial} = 3$

background

This module belongs to the CrossDomain section and imports only Mathlib. It introduces sibling objects including Dspatial, Dconfig, twoFace, gap45, eightTick, cubeFaces and their equality variants, plus three_is_Dspatial. The local theoretical setting connects cardinality spectra to dimension selection in the unified forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the T8 step that forces D equals three spatial dimensions. It supplies the cardinality-spectrum machinery used by downstream results that close the forcing chain.

scope and limits

Does not contain any theorem proofs.
Does not import Recognition Science core modules.
Does not list external dependencies beyond Mathlib.

declarations in this module (36)

def Dspatial L26
def Dconfig L27
def twoFace L28
def gap45 L29
def eightTick L30
def cubeFaces L31
theorem eightTick_eq L33
theorem gap45_eq L34
theorem cubeFaces_eq L35
theorem three_is_Dspatial L40
theorem four_is_2sq L43
theorem five_is_Dconfig L46
theorem six_is_cubeFaces L49
theorem seven_is_cube_minus_one L52
theorem eight_is_2cube L55
theorem ten_is_2_D L58
theorem twelve_is_D_4 L61
theorem fifteen_is_3_D L64
theorem sixteen_is_2_fourth L67
theorem twentyfive_is_Dsq L70
theorem fortyfive_is_gap L73
theorem sixtyfour_is_2sixth L76
theorem seventy_is_choose_8_4 L79
theorem oneTwentyFive_is_Dcubed L82
theorem twoSixteen_is_six_cubed L85
theorem twoFiftySix_is_power_of_2cube L88
theorem threeSixty_is_tick_gap L91
theorem threeOne25_is_D_fifth L94
theorem eleven_check L99
theorem thirteen_is_fib_7 L103
def rsSpectrum L107
theorem rsSpectrum_length L110
theorem rsSpectrum_pairwise_lt L113
theorem rsSpectrum_bounded L116
structure CardinalitySpectrumCert L119
def cardinalitySpectrumCert L133