IndisputableMonolith.Foundation.PeriodDependsOnDimension
Defines the fundamental recognition period as the dimension-generic length 2^D, without baking in D=3. Records the specializations at D=1..4, the biconditional that period equals eight exactly when D=3, and lemmas that the period definition is not circular with dimension forcing. Cited by anyone separating T7 (eight-tick octave) from T8 (D=3) in the forcing chain. Mostly definitional equalities plus an independence statement.
claimThe fundamental period length at spatial dimension $D$ is $P(D) := 2^D$. Thus $P(1)=2$, $P(2)=4$, $P(3)=8$, $P(4)=16$, and $P(D)=8$ if and only if $D=3$. Once $D$ is fixed by independent forcing, a canonical final period is $P(D)$; the definition of $P$ does not presuppose $D=3$.
background
In Recognition Science the discrete tick structure of the ledger is an octave whose length is a power of two. The forcing chain later identifies that length with eight (T7) and spatial dimension with three (T8). Those two conclusions must not be smuggled into each other: writing the constant 8 into the period definition would make the D=3 argument circular.
This module therefore takes the period as the pure function $D \mapsto 2^D$, imported against the DimensionForcing development that forces $D=3$ by separate topological and cost arguments. The local objects are the definition PeriodFromDimension, its values at small D, the biconditional linking period eight to D=3, and a FinalPeriod package that freezes the period only after dimension is fixed.
Upstream DimensionForcing states that spatial dimension D=3 is forced by the RS framework (linking, cost, and related arguments). This module consumes that setting without re-proving it.
proof idea
Definition module with elementary arithmetic. PeriodFromDimension is introduced as 2^D. The four period_at_D* facts are direct evaluations of powers of two. period_eq_eight_iff_D_eq_three is the standard biconditional 2^D=8 \Leftrightarrow D=3 on natural numbers. FinalPeriod and final_period_canonical package the post-forcing value; final_period_canonical_eq identifies it with eight once D=3 is in hand. no_period_circularity and two_independent_forcings record that the period definition does not assume D=3 and that period forcing and dimension forcing are independent inputs to the unified chain.
why it matters in Recognition Science
Feeds IndisputableMonolith.Foundation.UnifiedForcingChain, which claims all of T0-T8 as forced inevitabilities from the cost foundation (Recognition Composition Law). The chain needs a clean T7/T8 split: T7 is the eight-tick octave (period 2^3), T8 is D=3 spatial dimensions. By defining period as 2^D rather than the constant 8, this module supplies the non-circular bridge those steps require.
Downstream UnifiedForcingChain strengthens earlier "CPM Ultimate Closure" claims by deriving the full forcing ladder from the cost foundation alone. Without PeriodDependsOnDimension, the octave length and the dimension theorem would risk sharing a hidden hypothesis. The independence lemmas (no_period_circularity, two_independent_forcings) are the audit points for that separation.
scope and limits
- Does not prove D=3; that lives in DimensionForcing and the T8 step.
- Does not derive the eight-tick octave from the Recognition Composition Law alone.
- Does not fix units, masses, or coupling constants; only the period-vs-dimension link.
- Does not claim 2^D is the unique possible period formula outside the RS ledger setup.
- Does not address temporal dimension or non-power-of-two tick structures.
used by (1)
depends on (1)
declarations in this module (16)
-
def
PeriodFromDimension -
theorem
PeriodFromDimension_def -
theorem
period_at_D1 -
theorem
period_at_D2 -
theorem
period_at_D3 -
theorem
period_at_D4 -
theorem
period_eq_eight_iff_D_eq_three -
structure
FinalPeriod -
def
final_period_canonical -
theorem
final_period_canonical_eq -
theorem
no_period_circularity -
theorem
two_independent_forcings -
theorem
T7_from_T8 -
theorem
T8_from_T7 -
structure
PeriodDimensionBidirectional -
theorem
periodDimensionBidirectional