gap45_eq
plain-language theorem explainer
The equality shows that the gap cardinality equals the square of the spatial dimension times the configuration dimension. Cross-domain analysts in Recognition Science cite it to confirm that the spectrum member 45 decomposes directly from the primitives 3 and 5. The proof is a single decide tactic that evaluates the arithmetic after unfolding the constant definitions.
Claim. Let $g$ denote the gap cardinality, $D_s$ the spatial dimension, and $D_c$ the configuration dimension. Then $g = D_s^2 · D_c$.
background
The RS Cardinality Spectrum module collects witnesses that canonical cardinalities arise from multiplications, sums, and powers of the generators 2 and 3 together with the dimensions 3 and 5. Dspatial is defined as the spatial dimension fixed at 3; Dconfig is defined as the configuration dimension fixed at 5. Upstream theorems in RSCoupledAxis and DarkMatterMassFromGap45 already record that the gap cardinality equals 45 by reflexivity.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. After the constants Dspatial and Dconfig are unfolded, decide evaluates 3 squared times 5 to 45 and confirms numerical identity with the gap cardinality.
why it matters
This supplies the decomposition referenced by cardinalitySpectrumCert, which certifies the full spectrum {2, 3, 4, 5, ..., 45, ...}. It is also used in StyleSuccessionCert to bound average style gaps inside the interval [15, 90] and in darkMatterMassCert to set the mass ratio 1/gap45. Within the framework it links the eight-tick octave (T7) and spatial dimension D = 3 (T8) to the gap-45 reference point employed for mass and style predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.