module module high

`IndisputableMonolith.Foundation.DimensionForcing`

The DimensionForcing module establishes that spatial dimension equals 3 by combining J-symmetry ledger structure with the topological requirement of non-trivial circle linking. Researchers deriving constants or gauge groups from discrete foundations cite it to fix D=3 before proceeding to particle spectra or time emergence. The argument assembles imported results from Alexander duality and simplicial ledger to show that only D=3 satisfies both the eight-tick periodicity and linking axioms.

claimLet $D$ be the spatial dimension. Then $D=3$, because the $D$-sphere admits non-trivial circle linking if and only if $D=3$ and the ledger update period is $2^D$.

background

Recognition Science begins with a discrete ledger carrying J-cost, where J satisfies the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). PhiForcing shows self-similarity on this ledger forces the golden ratio φ. LedgerForcing derives double-entry bookkeeping from J-symmetry. SimplicialLedger represents the ledger as a coordinate-free simplicial 3-complex. AlexanderDuality supplies the topological fact: non-trivial circle linking in the D-sphere exists precisely when D=3, following Hatcher Algebraic Topology Theorem 3.44.

proof idea

The module is compositional. It imports the linking theorem from AlexanderDuality and the 2^D periodicity from PhiForcing and LedgerForcing. Theorems such as power_of_2_forces_D3 and eight_tick_forces_D3 apply these lemmas directly to conclude D=3. No internal tactic sequences are required beyond invocation of the imported results.

why it matters in Recognition Science

This module supplies D=3 to ConstantDerivations for deriving c, ħ, G, α; to GaugeFromCube for the automorphism group of the 3-cube yielding SU(3)×SU(2)×U(1); to ParticleGenerations for three fermion families; and to TimeEmergence for the minimal 8-tick cycle. It realizes step T8 of the unified forcing chain, closing the argument that dimension is forced rather than postulated.

scope and limits

Does not assume a background continuous manifold.
Does not derive D from measurement or experiment.
Does not address time dimension or spacetime signature.
Does not prove uniqueness of the simplicial representation.
Does not treat higher-dimensional or compactified extensions.

used by (10)

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

IndisputableMonolith.Foundation.ConstantDerivations module_import
IndisputableMonolith.Foundation.GaugeFromCube module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.QuarkColors module_import
IndisputableMonolith.Foundation.TimeEmergence module_import
IndisputableMonolith.Foundation.TopologicalConservation module_import
IndisputableMonolith.Foundation.WindingCharges module_import
IndisputableMonolith.Gravity.ZeroParameterGravity module_import
IndisputableMonolith.Unification.SpacetimeEmergence module_import
IndisputableMonolith.Unification.YangMillsMassGap module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.AlexanderDuality module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Foundation.SimplicialLedger module_import

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