twelve_is_D_4
plain-language theorem explainer
The equality 12 = Dspatial times 4 holds in the Recognition Science cardinality spectrum, with Dspatial fixed at the spatial dimension count of 3. Cross-domain analyses cite this witness to decompose 12 as the product of spatial dimension and the square of 2, matching cube-edge counting. The proof is a one-line decision procedure that reduces the numerical identity directly.
Claim. $12 = D_{spatial} times 4$ where $D_{spatial} = 3$.
background
The RS cardinality spectrum collects canonical counts reachable from the generators 2, 3, configDim = 5, and gap45. Dspatial is the in-module definition that sets the spatial dimension count to 3. Upstream configDim definitions vary by module (one sets it to 5 for baryon rung scaling, another to d + 2 for ledger parities), but the present theorem isolates the pure spatial factor for the decomposition 12 = 3 times 4.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the concrete numerical equality 12 = 3 * 4.
why it matters
This supplies an explicit witness inside the RS Cardinality Spectrum module for the member 12, expressed as Dspatial times 4 and tied to cube edges. It reinforces the framework claim that spectrum values arise from the small set of RS primitives (spatial dimension 3 from T8, powers of 2 from the eight-tick octave). No downstream theorems depend on it yet, so it functions as a standalone numerical anchor rather than a lemma for further derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.