Pith. sign in
module module high

IndisputableMonolith.Verification.Necessity.FibSubst

show as:
view Lean formalization →

Defines the Fibonacci sequence and a two-letter substitution system whose iterates realize Fibonacci growth. Supplies word types, the substitution map, and true/false symbol counters with elementary recurrence lemmas. Cited by the Fibonacci substitution certificate that packages the necessity argument linking substitution dynamics to the Fibonacci recurrence.

claimThe module introduces the Fibonacci numbers $F(0)=0$, $F(1)=1$, $F(n+2)=F(n+1)+F(n)$, finite words over a two-letter alphabet, the substitution $\sigma(0)=01$, $\sigma(1)=0$, its iterates on the seed word $[0]$, and counting functions for the two symbols on those words.

background

Recognition Science verification work often needs a discrete combinatorial model whose growth is forced to be Fibonacci. This module sits in the Necessity layer and supplies that model in Lean: a pure definition of $F_n$ together with a canonical length-2 substitution on ${0,1}$.

The substitution is $\sigma(0)=01$ and $\sigma(1)=0$. Starting from the seed word $[0]$, successive images $\sigma^n([0])$ are finite words whose symbol counts obey the Fibonacci recurrence. Companion definitions count occurrences of each letter (false/true, or $0$/$1$) and record the nil and cons cases needed for inductive arguments.

The module imports only Mathlib; it does not yet state the certificate theorem. That packaging lives one layer up in the FibSubstCert module, which consumes these definitions.

proof idea

This is primarily a definition and elementary-lemma module, not a deep proof development. It fixes fib by the standard recurrence, defines words and the substitution fibSub / fibSubWord, and proves the obvious counting identities on the empty word and on cons of false or true. Those lemmas are the inductive fuel for the certificate that later shows symbol counts equal Fibonacci numbers.

why it matters in Recognition Science

The module is the definitional substrate for IndisputableMonolith.Verification.FibSubstCert. That certificate packages the claim that the Fibonacci recurrence arises from the canonical two-letter substitution $\sigma(0)=01$, $\sigma(1)=0$, with iterates from seed $[0]$ yielding words whose symbol counts match $F_n$.

In the broader Recognition framework, Fibonacci structure appears wherever self-similar fixed-point scaling (the $\varphi$-ladder forced at T6) meets discrete tick or rung counting. A verified substitution model gives a combinatorial necessity route to that growth law, independent of analytic closed forms. Downstream certificate work can therefore treat Fibonacci counts as forced by the substitution rather than postulated.

scope and limits

used by (1)

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

declarations in this module (20)