pith. machine review for the scientific record. sign in
structure definition def or abbrev high

EightTickCert

show as:
view Lean formalization →

The EightTickCert structure bundles the ledger period equaling 8 at spatial dimension 3 with the identifications of that period as the sixth Fibonacci number and the dimension as the fourth, plus the standard recurrence between consecutive Fibonacci numbers. Researchers deriving constants or mass ladders from the Recognition Science forcing chain cite it when invoking the T7 eight-tick periodicity. The declaration is a direct structure definition that packages three facts already fixed by sibling definitions and the period_8 constant.

claimA structure certifying that the ledger period equals 8, that the fourth Fibonacci number equals the spatial dimension while the sixth equals the ledger period, and that the sixth Fibonacci number satisfies the recurrence $F_6 = F_5 + F_4$.

background

In this module the spatial dimension is defined as the constant 3 and the ledger period as $2$ raised to that dimension. The Fibonacci numbers are introduced locally as $F_4 := 3$, $F_5 := 5$, $F_6 := 8$ so that the dimension and period coincide with these values. The module documentation states that from the RS forcing chain T7 the ledger period is $2^D = 8$ at $D=3$, called the 8-tick fundamental periodicity, and that $D=3$ and the period are both Fibonacci numbers connected by the recurrence. Upstream, period_8 is defined as the constant 8 in ConstantDerivations.

proof idea

This is a structure definition whose three fields are simply the equalities ledgerPeriod = 8, the conjunction $F_4 =$ spatialDim and $F_6 =$ ledgerPeriod, and the recurrence $F_6 = F_5 + F_4$. No tactics or lemmas are invoked inside the structure; the fields directly reference the sibling definitions F4, F5, F6 and the upstream period_8 constant.

why it matters in Recognition Science

The structure supplies the certificate type instantiated by the downstream definition eightTickCert. It formalizes the T7 step of the forcing chain, where the eight-tick octave (period $2^3$) is forced together with the Fibonacci relations at D=3. The construction closes the link between spatial dimension, ledger period, and the phi-ladder via the recurrence, enabling later derivations of constants such as alpha inside the interval (137.030, 137.039).

scope and limits

formal statement (Lean)

  50structure EightTickCert where
  51  period_8 : ledgerPeriod = 8
  52  fibonacci_D : F4 = spatialDim ∧ F6 = ledgerPeriod
  53  fibonacci_rec : F6 = F5 + F4
  54

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.