gap_45_factorization
plain-language theorem explainer
The gap-45 factorization states that the integration gap parameter equals nine times five. Researchers tracing the eight-tick synchronization argument for spatial dimension three cite this step to isolate the factors three squared and five that enter the least common multiple with the eight-tick cycle. The proof is a direct reflexivity reduction on the constant definition of the gap parameter.
Claim. The integration gap parameter evaluated at spatial dimension three satisfies $45 = 9 × 5$.
background
The DimensionForcing module proves that spatial dimension D equals three by four independent arguments, one of which is the synchronization between the eight-tick cycle (equal to two to the power D) and the forty-five-tick cumulative phase. Gap-45 is defined as the integration gap parameter D squared times (D plus two) at D equals three, which evaluates to forty-five; this number is the ninth triangular number and represents cumulative phase accumulation over a closed cycle. The upstream declaration gap_45 simply sets this constant to forty-five.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of gap_45.
why it matters
This equality supplies the prime factorization required by the Gap-45 / 8-Tick Synchronization argument in the module. The resulting least common multiple of eight and forty-five equals three hundred sixty, which factors as two cubed times three squared times five and thereby isolates D equals three via the eight-tick octave. The module documentation notes that this replaces an unmotivated numerical coincidence with a physically motivated phase accumulation over the closed cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.