IsMinimalRecurrence
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any recurrence meeting the predicate.
- Does not derive the numerical value of the ratio from the definition alone.
- Does not extend to non-local or higher-order recurrences.
- Does not treat continuous or real-valued coefficients.
formal statement (Lean)
174def IsMinimalRecurrence (R : LocalBinaryRecurrence) : Prop :=
proof body
Definition body.
175 max R.coeff_a R.coeff_b = 1
176
177/-- Structure version of the bridge theorem. -/