period_8
plain-language theorem explainer
period_8 defines the natural number 8 as the fundamental eight-tick period in RS-native units. Researchers deriving spacetime structure from the J-cost function and phi fixed point cite it when establishing the octave that forces D=3. The definition is a direct constant assignment with no computation or lemmas.
Claim. The eight-tick period is the natural number $8$.
background
The Constant Derivations module derives physical constants from the RS foundation via the Composition Law and J-uniqueness, reaching phi as self-similar fixed point then D=3 via eight-tick structure. Upstream results include PhiForcingDerived.of (structure of J-cost) and SpectralEmergence.of (structure forcing SU(3) x SU(2) x U(1) and 24 chiral fermions from D x 2^D). The module doc states tau_0 = 8 ticks as fundamental time in the chain from Level 2 (phi and D=3) to Level 3 (tau_0 = 8 ticks).
proof idea
Direct definition that assigns the literal value 8. No lemmas or tactics are applied; it functions as a named constant for downstream periodicity certificates.
why it matters
Supplies the period_8 field in the EightTickCert structure (EightTickPeriodicityFromD), which certifies ledgerPeriod = 8 together with F4 = spatialDim and F6 = F5 + F4. It fills the T7 eight-tick octave step (period 2^3) in the forcing chain that links phi to D=3. It touches the mapping from discrete ticks to continuous spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.