Verification Necessity Fib Subst

Fibonacci substitution

A substitution system is a rule that replaces each symbol in a word with a fixed block of symbols. The Fibonacci substitution replaces the letter false with the pair false true, and true with the single letter false. Starting from the one-letter word false, repeated application grows the word: false, false true, false true false, false true false false true, and so on. The rule is named for what it does to the counts of the two letters: after n steps, the word contains exactly F(n+1) copies of false and F(n) copies of true, where F(0)=0, F(1)=1, and each later term is the sum of the two before it. That is the Fibonacci sequence itself, appearing not as a ratio but as literal letter counts.

The classical facts about this system are standard. The substitution was studied in combinatorics on words as a simple example of a morphic sequence, and its infinite limit word is the Fibonacci word, famous for being self-similar and for having a critical exponent below 2. The substitution rule is also a cousin of the golden ratio: the growth rate of the word length is the golden ratio φ = (1 + √5)/2, since the length after n steps is F(n+2), and the ratio of consecutive Fibonacci numbers tends to φ. The system is one of the cleanest places where an infinite object with nontrivial structure arises from a two-line rewriting rule.

In Recognition Science, the module named verification necessity fib subst, part of the framework's machine-checked library of formal theorems, takes this classical system and proves its counting behavior in full formal detail. The library defines words as lists of booleans, defines the substitution as a function on single symbols and then on whole words by concatenation, and defines the two count functions. It then proves, by induction, that the counts of false and true in the n-th iterated word are exactly the Fibonacci numbers. The central result is the lemma counts_iter_fib: for every natural number n, the pair (count of false, count of true) in the n-th iterated word equals (fib (n+1), fib n). The proof uses the recurrence that the substitution induces on counts: in one step, the number of false letters becomes the old false count plus the old true count, and the number of true letters becomes the old false count. That recurrence is precisely the Fibonacci recurrence, and the library verifies it with no gaps.

What this establishes in plain language is that the Fibonacci numbers are not just a numerical sequence; they are forced by a local rewriting rule. The module shows, with machine-checked certainty, that a two-letter substitution system carries the Fibonacci recurrence inside its letter counts. This matters because it gives a concrete combinatorial realization of the Fibonacci sequence as a counting phenomenon, not an abstract definition. The framework uses such verified combinatorial facts as building blocks for larger claims about recognition and structure; here the point is that the Fibonacci recurrence is not assumed but derived from a simple, checkable rule.

The consequence for a reader is that the Fibonacci word is now a proved object, not a pattern noticed by inspection. The library's proof guarantees that the counts are correct for every finite iteration, which is stronger than checking the first few words by hand. This is the kind of small, exact result that a larger formal architecture can rely on without rechecking.

/-- Fibonacci recursion on counts: starting from `[false]` we have
    counts (false) = (1,0) and recurrence
    F_{n+1} = F_n + T_n;  T_{n+1} = F_n. -/
lemma counts_iter_fib (n : Nat) :
  (countFalse (iter n), countTrue (iter n)) = (fib (n+1), fib n) := by
  induction n with
  | zero => simp [iter, fib]
  | succ n ih =>
      rcases counts_iter_succ n with ⟨hF, hT⟩
      have ihF : countFalse (iter n) = fib (n + 1) := (congrArg Prod.fst ih)
      have ihT : countTrue (iter n) = fib n := (congrArg Prod.snd ih)
      ext <;> simp [hF, hT, ihF, ihT, fib]

@[simp] lemma counts_iter_succ (n : Nat) :
  countFalse (iter (n+1)) = countFalse (iter n) + countTrue (iter n) ∧
  countTrue (iter (n+1)) = countFalse (iter n) := by
  have h_unfold : iter (n+1) = fibSubWord (iter n) := by
    simp [iter, Function.iterate_succ_apply']
  rw [h_unfold]
  exact counts_sub_word (iter n)

What this page does not claim

This module does not prove the golden ratio is forced by the substitution alone. This module does not establish any physical claim about recognition or cost. This module does not define the Fibonacci word as an infinite object; it only proves finite iterates.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Necessity/FibSubst.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: