eight_is_2cube
plain-language theorem explainer
Equating the natural number 8 to the eight-tick cardinality anchors the octave period as 2 cubed from three spatial dimensions. A physicist checking the structured spectrum in Recognition Science would cite this when confirming that 8 arises as 2^Dspatial rather than by fiat. The proof is a one-line reflexivity step that matches the literal 8 to the definition of the eight-tick value.
Claim. $8 = 2^{3}$ holds in the natural numbers, where the right-hand side is the eight-tick cardinality $2^{D}$ with $D = 3$ the number of spatial dimensions.
background
The CrossDomain.CardinalitySpectrum module assembles witnesses showing that RS cardinalities form a structured spectrum generated from the cube-generators 2 and 3, the configuration dimension 5, and gap45. The eight-tick cardinality is defined as the constant 8 and annotated as 2 raised to the spatial dimension count. This definition sits directly upstream of the spectrum witnesses and aligns with the forcing-chain step that fixes the eight-tick octave period at 2^3 once spatial dimensions equal 3.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity to the definition of the eight-tick cardinality.
why it matters
This declaration supplies the concrete 8 that appears in the enumerated spectrum set and thereby supports the module claim that every listed cardinality decomposes into RS primitives. It fills the T7 eight-tick octave slot in the forcing chain once T8 has set spatial dimensions to 3. No downstream uses are recorded yet, but the equality anchors the base case for later spectrum decompositions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.