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

D3_compatible

show as:
view Lean formalization →

D = 3 satisfies the three RS-compatibility conditions for a ledger dimension. Researchers deriving spatial dimension from recognition principles would cite this as the explicit witness that closes the forcing argument. The proof constructs the structure by invoking the linking theorem for the topological condition, reflexivity for the eight-tick equality, and a rewrite plus existential witness for the gap synchronization.

claimThe dimension $D=3$ satisfies the RS-compatibility conditions: it supports non-trivial linking of ledger edges, obeys $2^D=8$ for the eight-tick cycle, and divides the synchronization period of 360.

background

In the Dimension Forcing module a dimension D is RS-compatible when it meets three conditions: non-trivial linking for conservation, the eight-tick period equal to 8, and divisibility by the sync period. The linking condition is witnessed by Alexander duality showing that only D=3 permits stable knots and links in the ledger. The eight-tick and gap-45 synchronization arise from the requirement that the ledger cycle length $2^D$ aligns with the cumulative phase 45, yielding lcm(8,45)=360.

proof idea

The proof is a direct structure instantiation. It assigns the linking field to the theorem D3_has_linking, sets the eight_tick field by reflexivity since $2^3$ equals the defined eight_tick value, and discharges the gap_sync field by rewriting with sync_period_eq_360 and exhibiting 45 as the witness that 8 divides 360.

why it matters in Recognition Science

This theorem supplies the concrete instance required by the dimension_forced theorem, which proves that D=3 is the unique RS-compatible dimension. It completes the T8 step in the unified forcing chain by verifying that the topological, periodic, and synchronization conditions all hold simultaneously at D=3. The result anchors the claim that spatial dimension is not a free parameter but is forced by the Recognition Composition Law and ledger conservation requirements.

scope and limits

formal statement (Lean)

 362theorem D3_compatible : RSCompatibleDimension 3 := {

proof body

Tactic-mode proof.

 363  linking := D3_has_linking
 364  eight_tick := rfl
 365  gap_sync := by rw [sync_period_eq_360]; use 45; rfl
 366}
 367
 368/-- D = 3 is the unique RS-compatible dimension. -/

used by (2)

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

depends on (13)

Lean names referenced from this declaration's body.