eightTick_eq
plain-language theorem explainer
The equality states that the eight-tick cardinality equals two raised to the spatial dimension. Researchers verifying the RS cross-domain spectrum cite it to confirm the octave structure aligns with Dspatial set to three. The proof is a one-line wrapper that applies the decide tactic to evaluate both sides from their definitions.
Claim. Let $D = 3$ be the spatial dimension. Let eightTick denote the eight-tick cardinality. Then eightTick $= 2^D$.
background
The CrossDomain.CardinalitySpectrum module assembles witnesses for the RS cardinality spectrum, whose members arise from multiplications, sums, and powers of the generators {2, 3}, configDim 5, and gap45. Dspatial is the definition returning the natural number 3. eightTick is the definition returning 8, annotated as 2 to the power of Dspatial. The module setting is the claim that every listed cardinality admits a decomposition into these RS primitives, yielding a structured spectrum rather than an arbitrary collection.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic unfolds the definitions of eightTick and Dspatial, reduces both sides to the numeral 8, and confirms equality by computation.
why it matters
The result supplies the eightTick_as_D field inside cardinalitySpectrumCert, the top-level certificate for the spectrum. It directly instantiates the eight-tick octave (period 2^3) from the forcing chain with D equal to 3, closing the numerical link between the octave and spatial dimension in the RS primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.