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

ledgerPeriod

show as:
view Lean formalization →

Ledger period is defined as two raised to the spatial dimension. A researcher tracing the Recognition Science forcing chain at T7 would cite this when fixing the fundamental periodicity for three spatial dimensions. The definition directly substitutes the constant three to obtain the value eight.

claimDefine the ledger period by the equation $L = 2^{D}$ where $D=3$ denotes the spatial dimension.

background

The module formalises step T7 of the forcing chain: once the spatial dimension is fixed at three the ledger period becomes eight, called the eight-tick fundamental periodicity. Spatial dimension is introduced as the constant three. The ledger period is then obtained by exponentiation with base two. This step also prepares the link to the Fibonacci sequence via the relation that the sixth Fibonacci number equals eight and the fourth equals three.

proof idea

The declaration is a direct definition that applies the spatial-dimension constant to the exponentiation operation.

why it matters in Recognition Science

The definition supplies the period value required by the EightTickCert structure and the both_fibonacci_at_D3 theorem. It realises the T7 claim that the ledger period equals eight at D equals three, thereby closing the eight-tick octave. The construction also feeds the relation that the period times the five-rung depth yields a quantity near phi to the eighth power.

scope and limits

formal statement (Lean)

  25def ledgerPeriod : ℕ := 2 ^ spatialDim

proof body

Definition body.

  26

used by (5)

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

depends on (1)

Lean names referenced from this declaration's body.