Foundation Period Depends On Dimension Period At D2

Period as a function of dimension

The Recognition Science framework models the universe as a discrete record of events, a ledger where each entry has a recognition cost. The framework's forcing chain derives that the number of ticks in a full recognition cycle is a power of the spatial dimension, written as PeriodFromDimension(D) = 2^D. The theorem period_at_D2 is a simple instance of that definition: when the dimension D is 2, the period is 2^2 = 4. It is a direct consequence of the defining equation, not an independent discovery.

What the theorem does not claim is any physical content about two-dimensional space itself. It does not say that two-dimensional worlds exist, that recognition happens in them, or that the number 4 has any meaning beyond the definition. The declaration is a formal identity: given the definition of period as 2^D, plugging in D = 2 yields 4 by computation. The framework's interest lies elsewhere, in the case D = 3, where the period becomes 8, the famous eight-tick cycle.

The surrounding module addresses a circularity concern raised by Philip Beltracchi: the label "8-tick" seems to presuppose three dimensions. The framework's library proves that the dimension is forced to 3 by a topological linking condition, independently of the number 8, and then the period is defined as 2^D. So the honest order is dimension first, period second. period_at_D2 is a stepping stone in that definitional chain, showing the period for a lower dimension, not a claim about any physical two-dimensional universe.

/-- For `D = 2`, the period is 4. -/
theorem period_at_D2 : PeriodFromDimension 2 = 4 := rfl

/-- Period equals 8 iff `D = 3`. Proved from `power_of_2_forces_D3`.
    Neither direction is the "natural" one; they are equivalent. -/
theorem period_eq_eight_iff_D_eq_three (D : ℕ) :
    PeriodFromDimension D = 8 ↔ D = 3 := by
  constructor
  · intro h
    unfold PeriodFromDimension at h
    exact power_of_2_forces_D3 D h
  · intro h; subst h; rfl

/-- The fundamental period length from the spatial dimension: `2^D`.
    This is a **definition** that does not presuppose `D = 3`.
    Writing `8` here would be wrong in general; writing `2^D` is
    dimension-generic. -/
def PeriodFromDimension (D : ℕ) : ℕ := 2 ^ D

What this page does not claim

The theorem does not establish that two-dimensional space exists or that recognition occurs in it. The theorem does not assign any physical meaning to the number 4 beyond the formal definition of period. The theorem does not by itself prove the eight-tick cycle, which requires the dimension to be three.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PeriodDependsOnDimension.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: