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

choke_dimension

show as:
view Lean formalization →

The choke_dimension definition records the fourth choke point in Recognition Science's inevitability structure, asserting that dimension forcing from linking requirements selects D = 3 as the sole viable spatial dimension. Physicists tracing the derivation of three-dimensional space from the phi-ladder and eight-tick period would cite this when evaluating alternatives to the framework. It is implemented as a direct record definition marking the status as a scaffold pending the linking proof.

claimThe fourth choke point is the record with name ``Dimension Forcing'', status ``scaffold'', and consequence that $D = 3$ is the only viable spatial dimension.

background

A ChokePoint is a structure with fields name (String), status (String, one of closed'', scaffold'', or ``open''), and consequence (String), serving as a place where alternatives can hide unless proven closed. The module sets the local theoretical setting as the inevitability structure under CPM/cost foundation, where alternatives fall into three buckets and must violate one of six necessities to survive; the dimension necessity is the sixth: linking requirements force D = 3. Upstream, DimensionForcing.Dimension is the abbreviation Dimension := ℕ, RSNativeUnits.status records the phi-ladder phiRung n = φⁿ together with the eight-tick period, and Constants.Dimensions.Dimension tracks [Length, Time, Mass] exponents.

proof idea

This is a direct definition that constructs the ChokePoint record by supplying the three fields name, status, and consequence. No lemmas are applied and no tactics are used; it functions as a one-line wrapper that registers the scaffold status for the incomplete linking proof.

why it matters in Recognition Science

This declaration populates the list returned by all_choke_points, which enumerates the necessities any alternative framework must violate. It corresponds to the dimension step in the Inevitability Theorem quoted in the module documentation, linking to T7 (eight-tick octave of period 2³) and T8 (D = 3) in the forcing chain. The scaffold status flags the open question of completing the proof that linking requirements force three spatial dimensions.

formal statement (Lean)

 232def choke_dimension : ChokePoint := {

proof body

Definition body.

 233  name := "Dimension Forcing"
 234  status := "scaffold"  -- Linking proof incomplete
 235  consequence := "D = 3 is the only viable dimension"
 236}
 237
 238/-- All choke points. -/

used by (1)

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

depends on (9)

Lean names referenced from this declaration's body.