FibSubstCert
plain-language theorem explainer
Packages a unit certificate that the canonical two-letter substitution σ(0)=01, σ(1)=0, iterated from the seed [0], produces symbol counts exactly equal to consecutive Fibonacci numbers. Anyone tracing the discrete origin of φ in RS cites this. Verification is a five-conjunct Prop discharged by definitional equality on the rules plus the upstream iteration lemmas.
Claim. A Fibonacci-substitution certificate is a unit token whose verification asserts four facts: the substitution sends $0\mapsto 01$ and $1\mapsto 0$; for every $n$, the iterated word from seed $[0]$ has false/true counts $(F_{n+1}, F_n)$; the base counts are $(1,0)$; and successive false-counts obey the Fibonacci recurrence $\#0(w_{n+1})=\#0(w_n)+\#1(w_n)$.
background
The module certifies that Fibonacci recurrence is not fitted but forced by the simplest nontrivial binary substitution. Write $\sigma(0)=01$, $\sigma(1)=0$, seed $w_0=[0]$, and $w_{n+1}=\sigma(w_n)$. Counting false and true symbols in $w_n$ yields exactly $(F_{n+1}, F_n)$.
In the RS certificate chain this matters because $F_{n+1}/F_n\to\varphi$, and $\varphi$ is the self-similar fixed point forced at T6. The substitution supplies a concrete discrete dynamical generator of that sequence, rather than an analytic ansatz.
Upstream (from the imported FibSubst necessity module) one already has the structural facts: how symbol counts transform under a single substitution step, the identity that iterated counts equal Fibonacci pairs, the base case at $n=0$, and the one-step recurrence for counts. The empty structure here is only a packaging token; all content lives in the verification predicate.
proof idea
The structure itself is empty (a Repr-deriving unit). Content is the simp predicate verified, a five-way conjunction: the two substitution equations, the universal Fibonacci count identity, the base counts $(1,0)$, and the count recurrence.
verified_any discharges every conjunct for an arbitrary certificate. The two substitution rules are rfl against fibSub. The Fibonacci identity is exactly the upstream lemma counts_iter_fib. The base case is simp on iter and fib. The recurrence is the first projection of counts_iter_succ n. No new arithmetic is proved here; the certificate only bundles already-established facts.
why it matters
Recognition Science forces $\varphi$ as the unique self-similar cost fixed point (T6 in the UnifiedForcingChain). The classical analytic route is the limit of Fibonacci ratios. This certificate closes the discrete side of that story: the same sequence arises from iterating the shortest nontrivial substitution, so the link from discrete recognition dynamics to $\varphi$ is not an external fit.
The module doc states the point directly: the proof shows Fibonacci "is not imposed by fitting, but emerges from the simplest non-trivial substitution rule." Downstream consumers (none wired yet in the graph) would cite the certificate when assembling the φ-ladder, mass rungs, or any argument that needs a verified discrete generator of $F_n$ rather than an axiomatized sequence.
It does not itself prove the ratio limit or T6 uniqueness; it only locks the combinatorial engine those arguments rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.