Pith. sign in
module module moderate

IndisputableMonolith.Verification.FibSubstCert

show as:
view Lean formalization →

Verification certificate module for the two-letter Fibonacci substitution system. It packages the necessity-layer substitution facts (letter counts obey the Fibonacci recurrence) into a checkable cert object used by the verification stack. Researchers tracing discrete self-similarity or phi-ladder combinatorics cite it. Structure is thin: import and re-export the necessity development as a cert.

claimA verification certificate for the two-letter substitution system whose letter-count sequences satisfy the Fibonacci recurrence $F_{n}=F_{n-1}+F_{n-2}$, linking combinatorial substitution dynamics to the golden-ratio growth rate $\varphi$.

background

Recognition Science forces $\varphi$ as the unique self-similar fixed point (forcing chain T6) and uses $\varphi$-ladder mass and timing formulae. Combinatorially, the same growth appears in the classical Fibonacci word / two-letter substitution: a morphism on an alphabet of size two whose incidence matrix has dominant eigenvalue $\varphi$, so that letter counts obey the Fibonacci recurrence.

The upstream module Necessity.FibSubst develops that substitution system and proves the count recurrences. The present module sits in the Verification domain: it does not redo the combinatorics; it wraps those facts as a certificate consumable by higher verification and audit layers.

Local setting is therefore certificate packaging rather than new dynamics: Mathlib plus the necessity FibSubst import, exposing a cert-shaped interface named FibSubstCert.

proof idea

This is a certificate/module wrapper, not a deep proof development. It imports the necessity-layer Fibonacci substitution theory and surfaces it as a verification certificate object. No independent tactic script or algebraic derivation lives here; the mathematical content is inherited from the upstream FibSubst results on two-letter substitutions and Fibonacci count recurrences.

why it matters in Recognition Science

Connects the discrete substitution model of self-similarity to the verification stack that audits Recognition claims. Fibonacci counts are the combinatorial shadow of $\varphi$-growth used in the mass ladder and eight-tick timing story; certifying them keeps the necessity layer auditable. No downstream consumers are recorded in the graph yet, so the module is presently a leaf cert in Verification, ready for audit or export rather than an intermediate lemma in a longer proof chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)