IndisputableMonolith.Foundation.DimensionForcing

declarations in this module (43)

• abbrev Dimension L107
• def eight_tick L110
• def gap_45 L113
• def sync_period L116
• theorem sync_period_eq_360 L119
• def EightTickFromDimension L125
• theorem simplicial_loop_tick_lower_bound L128
• theorem eight_tick_is_2_cubed L136
• theorem power_of_2_forces_D3 L139
• theorem eight_tick_forces_D3 L155
• def spinorDimension L189
• theorem spinor_dim_D3 L192
• theorem spinor_dim_D1 L195
• theorem spinor_dim_D2 L198
• theorem spinor_dim_D4 L201
• structure HasRSSpinorStructure L214
• theorem D3_has_spinor_structure L223
• theorem D1_no_spinor_structure L230
• theorem D2_no_spinor_structure L235
• theorem D4_no_spinor_structure L240
• theorem spinor_eight_tick_forces_D3 L253
• def SupportsNontrivialLinking L282
• theorem D3_has_linking L287
• theorem linking_requires_D3 L292
• theorem D1_no_linking L297
• theorem D2_no_linking L302
• theorem D4_no_linking L307
• theorem high_D_no_linking L312
• theorem gap_45_factorization L326
• theorem gap_45_has_factor_9 L329
• theorem sync_factorization L332
• theorem sync_prime_factorization L339
• theorem rotation_period L343
• theorem sync_implies_D3 L346
• structure RSCompatibleDimension L356
• theorem D3_compatible L362
• theorem dimension_unique L369
• theorem dimension_forced L383
• def D_physical L393
• theorem D_physical_compatible L396
• theorem physical_eight_tick L399
• theorem why_D_equals_3 L425
• def dimension_forcing_summary L459