IsMinimalRecurrence
plain-language theorem explainer
A definition that marks a local binary recurrence minimal precisely when the larger of its two positive integer coefficients equals 1. Workers on the T5-to-T6 bridge cite it to enforce the zero-parameter condition that selects the Fibonacci recurrence among all integer pairs. The predicate is a direct one-line comparison on the coefficient pair.
Claim. A local binary recurrence with positive integer coefficients $a,b$ is minimal when $a$ and $b$ satisfy $a=1$ or $b=1$ (equivalently, their maximum is 1).
background
The Hierarchy Dynamics module closes the T5-to-T6 gap by deriving the Fibonacci recurrence from zero-parameter ledger composition. A local binary recurrence packages a uniform scale ladder with positive integer coefficients $a$ and $b$ such that the level at position $k+2$ equals $a$ times the level at $k+1$ plus $b$ times the level at $k$; the coefficients count the discrete sub-events that participate in each composition step.
proof idea
One-line definition that equates minimality to the condition that the maximum of the two coefficients equals unity.
why it matters
The predicate is invoked by the parent theorem hierarchy_dynamics_forces_phi, which concludes that the ladder ratio equals phi. It supplies the final step in the module's derivation chain: zero parameters force uniform ratio, locality forces order-2 recurrence, discreteness forces integer coefficients, and minimality selects the pair (1,1), thereby deriving sigma squared equals sigma plus 1 without assuming the golden equation as a closure axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.