F6
plain-language theorem explainer
F6 assigns the constant 8 to the ledger period in natural numbers, matching the 2^D value at D=3 from the forcing chain. Topological veto arguments in fluid dynamics and black-hole entropy calculations cite this value to bound crossings and helicity. The declaration is a direct constant assignment with no computation or lemmas.
Claim. Define the ledger period by $F_6 := 8$, where this equals $2^D$ at spatial dimension $D=3$.
background
The module formalizes T7 of the forcing chain: the ledger period equals $2^D$, which evaluates to 8 when D=3. This eight-tick periodicity is identified with the sixth Fibonacci number, while D=3 itself is the fourth Fibonacci number; the two are linked by the recurrence F(6) = F(5) + F(4). The definition supplies the named constant used throughout the Recognition framework for periodicity constraints.
proof idea
The declaration is a direct definition that sets F6 to the constant 8. No lemmas or tactics are invoked; the value is assigned by equality.
why it matters
F6 supplies the numerical value required by T7 for the eight-tick octave at D=3. It is referenced by downstream results in TopologicalVeto, including finite_crossings_from_budget (finite budget implies finite crossings under positive cost per crossing) and linking_nontrivial_iff_D3 (nontrivial linking occurs only at D=3). The definition closes the T7 step and feeds the Fibonacci connection used in both_fibonacci_at_D3 and black-hole entropy derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.