f6_eq_ledgerPeriod
plain-language theorem explainer
The declaration equates the sixth Fibonacci number to the ledger period at spatial dimension 3. Workers on the T7 eight-tick periodicity step cite it to confirm that both quantities evaluate to 8 and satisfy the Fibonacci recurrence link. The proof proceeds by direct evaluation with the decide tactic.
Claim. $F_6 = 2^D$ with $D=3$, where $F_6$ is the sixth Fibonacci number and the right-hand side is the ledger period defined as $2$ raised to the spatial dimension.
background
The module formalizes the T7 forcing-chain step: the ledger period equals $2^D$ and therefore equals 8 when $D=3$. F6 is introduced as the explicit numeral 8. ledgerPeriod is defined directly as $2$ raised to spatialDim. Upstream results supply the alias F for the gap function and the master generating functional, but the present equality uses only the numeric definitions of F6 and ledgerPeriod.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality F6 = ledgerPeriod. Both sides reduce to the constant 8, so the tactic closes the goal without further lemmas.
why it matters
The equality completes the T7 formalization that the eight-tick period is the Fibonacci number F(6) at D=3. It sits inside the chain that also records F(4)=3 for the spatial dimension and the recurrence F(6)=F(5)+F(4). The result anchors the 40-rung product $8 times 5 = phi^8.37...$ used in later periodicity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.