pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Mathematics.FibonacciSequenceFromRS

show as:
view Lean formalization →

This module derives the Fibonacci sequence from Recognition Science primitives by establishing explicit equalities for the first eight terms and a recurrence certificate. Researchers modeling self-similar discrete structures or the emergence of D=3 would cite these results when linking the phi fixed point to integer sequences. The module consists of direct term computations followed by a structure that certifies the full recurrence relation.

claimThe sequence satisfies $F_3=2$, $F_4=3=D$, $F_5=5$, $F_6=8$, $F_7=13$, $F_8=21$, the relation $F_6=2D^2$, and the recurrence $F_n=F_{n-1}+F_{n-2}$ for $n>2$, certified by a structure FibonacciCert.

background

Recognition Science takes the fundamental time quantum as the tick with value 1, imported from the Constants module. The present module introduces the Fibonacci sequence as the integer sequence generated by the self-similar fixed point phi and the eight-tick octave. It defines a collection of lemmas that compute the initial terms explicitly and a certificate structure that packages the recurrence.

proof idea

The module proceeds by a sequence of direct equalities for successive terms using the standard Fibonacci recurrence, followed by a definition of the FibonacciCert structure that records the verified initial segment and the recurrence step.

why it matters in Recognition Science

The module supplies the explicit link F(4)=D that closes the forcing chain step T8 for spatial dimension. It provides the integer sequence needed for later phi-ladder constructions and mass formulas in the Recognition framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (11)