unit_coefficients_give_fibonacci
plain-language theorem explainer
Integer recurrence with unit coefficients on a uniform scale ladder reduces to the Fibonacci relation between consecutive levels. Researchers deriving the T5 to T6 bridge in Recognition Science cite this when tracing minimal ledger composition to the golden ratio. The proof is a short algebraic reduction that casts coefficients to reals, applies the one-multiplication lemma, and finishes with linear arithmetic.
Claim. Let $L$ be a uniform scale ladder. If the level sizes satisfy $L_2 = a L_1 + b L_0$ where the positive integers $a$ and $b$ both equal 1, then $L_2 = L_1 + L_0$.
background
A uniform scale ladder is a sequence of positive real level sizes with uniform scaling ratio greater than one, extracted from multilevel ledger composition under the Recognition framework. The Hierarchy Dynamics module derives the Fibonacci recurrence from zero-parameter axioms to bridge T5 (J-uniqueness via the cost functional) and T6 (self-similar fixed point). Upstream results include the UniformScaleLadder structure, which encodes the uniform_scaling property that each level equals the ratio times the prior level, and the one_mul theorem establishing that multiplication by one leaves a value unchanged.
proof idea
The proof casts the natural-number coefficients to reals via exact_mod_cast, rewrites the scaled terms using the one_mul lemma from ArithmeticFromLogic to recover the unscaled levels, and concludes directly with linarith.
why it matters
This supplies the Fibonacci step that feeds the parent bridge_T5_T6 theorem, which shows minimal local binary recurrence forces the ratio to equal phi. It closes the gap between J-uniqueness (T5) and the self-similar fixed point (T6) in the forcing chain. The module documentation states that this traces derivation through multilevel composition, zero parameters, locality, discreteness, and minimality to obtain the recurrence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.