gap45
plain-language theorem explainer
gap45 supplies the natural number 45 as one generator in the RS cardinality spectrum. Cross-domain work cites it when decomposing listed values such as 70 and 125 from the primitives 2, 3, 5 and this constant. The module uses it to witness that the spectrum arises by systematic combination rather than arbitrary selection. The definition is a direct literal assignment.
Claim. Let $g_{45} := 45$ denote the fixed natural number that serves as a generator for the RS cardinality spectrum.
background
The module assembles witnesses for the spectrum {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}. Each member factors via multiplication, addition or powering from the cube generators {2, 3}, the configuration dimension 5, and the constant gap45. The local claim is that RS produces a structured numerical spectrum whose members admit explicit decompositions into these primitives.
proof idea
The definition is a direct one-line assignment of the literal value 45 to the identifier gap45 in the natural numbers.
why it matters
gap45 completes one base element of the spectrum listed in the module documentation. It participates in the demonstration that every listed cardinality decomposes into RS primitives. No downstream theorems are recorded in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.