ledgerPeriod_eq_8
plain-language theorem explainer
The theorem establishes that the ledger period equals 8 when spatial dimension is fixed at 3. Researchers formalizing the Recognition Science forcing chain at T7 would cite it to anchor the fundamental 8-tick periodicity. The proof is a direct numerical reduction via the decide tactic on the definition ledgerPeriod := 2 raised to spatialDim.
Claim. Let $D$ denote the spatial dimension with $D=3$. The ledger period, defined by $2^D$, satisfies $2^D=8$.
background
The module formalizes the 8-tick periodicity arising from the Recognition Science forcing chain at T7. Spatial dimension is defined as the constant 3 and ledger period is defined as 2 raised to that dimension, yielding the period 8 at D=3. This matches the module statement that the ledger period is 2^D = 2^3 = 8 at D=3, called the 8-tick fundamental periodicity. Upstream definitions include the gap function F(Z) = log(1 + Z/phi)/log(phi) from AnchorPolicy, though the present equality relies only on the direct power computation.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality 2^3 = 8 arising from the definitions of ledgerPeriod and spatialDim.
why it matters
This supplies the period_8 field inside the eightTickCert certificate that also records the Fibonacci connection at D=3. It closes the T7 step of the forcing chain, confirming the eight-tick octave (period 2^3) required by the Recognition Science framework when D=3. The result sits between the spatialDim definition and the downstream certificate that bundles it with the Fibonacci recurrence and both_fibonacci_at_D3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.