three_is_Dspatial
The equality 3 = D_spatial holds by definition in the Recognition Science cardinality spectrum. Cross-domain analyses cite this witness to fix the spatial dimension count at the T8 step of the forcing chain. The proof is a direct reflexivity reduction on the constant definition of Dspatial.
claim$3 = D_{spatial}$
background
The module C21 collects witnesses that RS cardinalities decompose into primitives from the cube generators {2,3}, configDim 5, and gap45, producing the structured spectrum {2,3,4,5,6,7,8,10,12,15,16,45,70,125,216,256,3125,...}. Dspatial is the in-module definition that sets the spatial dimension cardinality to 3. This sits inside the broader Recognition Science derivation where T8 forces exactly three spatial dimensions from the eight-tick octave and J-uniqueness.
proof idea
One-line term proof that applies reflexivity directly to the definition Dspatial := 3.
why it matters in Recognition Science
Fixes the spatial dimension at T8 in the unified forcing chain and supplies the explicit 3 in the C21 cardinality spectrum. It supports the claim that every spectrum member admits a decomposition into RS primitives. No downstream theorems yet reference it, leaving open whether further spectrum members will invoke this equality explicitly.
scope and limits
- Does not derive the value 3 from the J-cost or RCL axioms.
- Does not address non-spatial cardinalities such as Dconfig or gap45.
- Does not prove that 3 is the only possible spatial dimension under alternative forcings.
formal statement (Lean)
40theorem three_is_Dspatial : (3 : ℕ) = Dspatial := rfl
proof body
Term-mode proof.
41
42/-- 4 = 2². -/