pith. machine review for the scientific record. sign in
theorem proved term proof high

twelve_is_D_4

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  61theorem twelve_is_D_4 : (12 : ℕ) = Dspatial * 4 := by decide

proof body

Term-mode proof.

  62
  63/-- 15 = 3·5 = 3 nested configDim (planet strata). -/

depends on (4)

Lean names referenced from this declaration's body.