Foundation Period Depends On Dimension Period At D1

The period as a function of dimension

The declaration period_at_D1 is a small but precise piece of a larger argument. It states that when the dimension D equals 1, the period, defined as 2^D, equals 2. In plainer terms: in a one-dimensional setting, the framework's recognition cycle has length 2. This is a direct consequence of the definition PeriodFromDimension D := 2^D, which makes the period a function of the dimension, not a separate assumption.

The definition itself is a modeling choice. The framework chooses to define the period as 2^D, and the theorems period_at_D1, period_at_D2, period_at_D3, and period_at_D4 simply compute the values 2, 4, 8, and 16 for D equal to 1, 2, 3, and 4. The number 8, often called the eight-tick cycle, is not a premise here. It is a consequence that appears only when D is 3.

The real content of the module is the relationship between the period and the dimension. A bidirectional theorem, period_eq_eight_iff_D_eq_three, proves that the period equals 8 if and only if the dimension D equals 3. This is an equivalence: either direction can serve as the hypothesis. The module also packages the honest order of derivation in a structure called FinalPeriod, where the dimension D is pinned to 3 by a separate topological argument, and the period is then computed as 2^3 = 8. A diagnostic theorem, no_period_circularity, states this explicitly: the dimension is determined by linking conditions without ever mentioning the number 8, and the period is then defined as 2^D.

What period_at_D1 does not claim is any physical fact about one-dimensional space. It does not say that recognition cycles in one dimension have length 2 in any empirical sense. It is a definitional computation within a formal framework. The theorem establishes a relationship between two defined quantities, nothing more. The physical claim that the period is 8 because D = 3 rests on the separate topological argument that forces D = 3, which is a different theorem entirely.

/-- For `D = 1`, the period is 2. -/
theorem period_at_D1 : PeriodFromDimension 1 = 2 := 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

/-- 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⟩

What this page does not claim

The theorem does not claim any empirical fact about one-dimensional space. The theorem does not establish that the physical period is 8; that requires the separate theorem forcing D = 3. The value 2 for the period at D = 1 is a definitional consequence, not a measured quantity.

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: