Foundation Period Depends On Dimension

Period as a function of dimension

In the Recognition Science framework, a recognition cycle (a discrete record of events that repeats) has a period, a number of ticks before the pattern repeats. The framework's library of machine-checked theorems defines this period not as a fixed constant but as a function of the dimension D of space: PeriodFromDimension D = 2^D. In one dimension the period is 2, in two dimensions it is 4, in three dimensions it is 8, and in four dimensions it is 16. This definition is a choice, a model of what the period means.

The important theorem is that the period equals 8 if and only if the dimension equals 3. The proof is bidirectional: if the period is 8, then the dimension must be 3, and if the dimension is 3, then the period is 8. This equivalence is proved in the framework's library, with no gaps and no extra assumptions. The result answers a concern raised by Philip Beltracchi, who noted that calling the cycle an "8-tick" cycle before proving the dimension is 3 could look circular. The module shows it is not.

The key is that the dimension is forced independently of the period. A separate theorem proves D = 3 from a topological condition called Alexander duality, which concerns how a circle can be linked in space. This proof never mentions the number 8. Once the dimension is known to be 3, the period is then defined as 2^3, which equals 8. The number 8 is a consequence of the dimension, not a premise that sneaks it in. The library packages this honest order in a structure called FinalPeriod, which records that the period is 8 because D = 3.

In Recognition Science, this establishes that the eight-tick cycle is not an arbitrary feature of the framework. It is the period that any recognition cycle must have in a three-dimensional space, once the cost of recognition is forced by the framework's five plain conditions. The module does not claim to derive the dimension itself; that is done elsewhere. It only shows that once the dimension is 3, the period of 8 follows, and that this reasoning is free of circularity.

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

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

/-- For `D = 3`, the period is 8. -/
theorem period_at_D3 : PeriodFromDimension 3 = 8 := rfl

/-- For `D = 4`, the period is 16. -/
theorem period_at_D4 : PeriodFromDimension 4 = 16 := 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

/-- **DIAGNOSTIC THEOREM.** The linking argument for `D = 3` does not
    presuppose the 8-tick period.

    Statement: every `D` with non-trivial linking equals 3, and this
    is proved *without* the predicate `EightTickFromDimension D =
    eight_tick` as a hypothesis.

    Proof: `linking_requires_D3` is proved from Alexander duality in
    `Foundation/AlexanderDuality`. Its hypothesis is `SupportsNontrivialLinking`,
    which is defined as `SphereAdmitsCircleLinking`, which is defined via the
    reduced cohomology of `S¹`. None of those refer to the 8-tick.

    Hence D = 3 is pinned first; the period 8 then follows as `2^D = 2^3`. -/
theorem no_period_circularity :
    (∀ D : ℕ, SupportsNontrivialLinking D → D = 3) ∧
    (PeriodFromDimension 3 = 8) :=
  ⟨linking_requires_D3, rfl⟩

/-- At the canonical instance, the period is 8 (as a consequence of
    D = 3, not as a premise). -/
theorem final_period_canonical_eq :
    final_period_canonical.period = 8 := rfl

What this page does not claim

This module does not derive the dimension D = 3; it only shows the period is 8 given that dimension. The period being a function of dimension is a definitional choice, not a forced consequence of the framework's axioms. The theorem does not claim that Alexander duality is the only way to force the dimension.

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: