gap_45
plain-language theorem explainer
Gap_45 supplies the integer constant 45 as the integration gap D²(D+2) evaluated at D=3. Researchers deriving spatial dimension from the Recognition Science forcing chain cite it when synchronizing the eight-tick cycle with cumulative phase T(9). The declaration is a direct constant assignment with no reduction steps or lemmas.
Claim. The integration gap parameter is the natural number $45$, equal to $D^2(D+2)$ when the spatial dimension $D=3$.
background
The Dimension Forcing module proves D=3 is forced by topological linking (non-trivial knots only in three dimensions) and by synchronization between the 8-tick cycle (2^D) and the cumulative phase sum T(9)=45. Gap-45 is introduced precisely as this 45-tick gap arising from the closed 8-tick ledger cycle. The upstream period definition from pulsar regimes supplies the phi-ladder context in which such constants appear.
proof idea
The declaration is a direct definition that assigns the integer 45. No lemmas or tactics are invoked; it functions as a named constant for subsequent lcm computations and factorizations.
why it matters
This constant enters sync_period := lcm(eight_tick, gap_45) = 360, which selects D=3 via the eight-tick octave (T7) and forces D=3 (T8). It is used by gap_correction to produce the approximate fine-structure constant and by the factorization theorems gap_45_factorization and gap_45_has_factor_9. The definition closes the gap-45/8-tick synchronization step in the dimension-forcing argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.