pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Dimension

show as:
view Lean formalization →

Dimension is defined as the natural numbers in the RS foundation. Researchers deriving that spatial dimension equals 3 from topological linking and eight-tick synchronization would cite this abbreviation to type the variable D. The declaration is a direct abbreviation with no lemmas or computational steps.

claimSpatial dimension is represented by a natural number $D$ in the set of natural numbers $D : ℕ$.

background

The Dimension Forcing module proves that spatial dimension D equals 3 is forced by the RS framework. It presents a linking argument: D=1 is collinear with no linking, D=2 unlinks by the Jordan curve theorem, D=3 permits non-trivial knots and links, and D≥4 unlinks by codimension. A second argument requires synchronization of the 8-tick cycle (2^D) with the 45-tick cumulative phase, yielding lcm(8,45)=360 and forcing D=3 via 2^D=8.

proof idea

This is a direct abbreviation. No lemmas are applied and no tactics are used; the declaration simply sets the carrier type for dimension values referenced in downstream results such as spatial_dims_eq_3 and eight_tick_forces_temporal.

why it matters in Recognition Science

The abbreviation supplies the type used by spatial_dims_eq_3 (spatial_dims_forced = 3) and eight_tick_forces_temporal (2^D = 8). It occupies the T8 position in the unified forcing chain where D=3 is forced by the eight-tick octave. It also appears in curvature space derivations and pulsar period calculations that depend on the forced dimension.

scope and limits

formal statement (Lean)

 107abbrev Dimension := ℕ

proof body

Definition body.

 108
 109/-- The eight-tick period. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.