LocalBinaryRecurrence
plain-language theorem explainer
LocalBinaryRecurrence packages a UniformScaleLadder with positive integer coefficients a and b that enforce the local linear relation L_2 = a L_1 + b L_0. Researchers closing the T5 to T6 gap in Recognition Science cite this packaging when tracing zero-parameter ledger composition to the Fibonacci recurrence. The declaration is a bare structure definition with no proof body or computational content.
Claim. A uniform scale ladder with positive levels $L_k$ and ratio $σ > 1$ equipped with integers $a, b ≥ 1$ satisfying the local recurrence $L_2 = a L_1 + b L_0$.
background
The module HierarchyDynamics closes the T5→T6 bridge by deriving the Fibonacci recurrence from discrete zero-parameter ledger axioms. UniformScaleLadder extracts a scale ladder from multilevel composition: a sequence of positive level sizes with a uniform scaling ratio. Its definition states: structure UniformScaleLadder where levels : ℕ → ℝ, levels_pos : ∀ k, 0 < levels k, ratio : ℝ, ratio_gt_one : 1 < ratio, uniform_scaling : ∀ k, levels (k + 1) = ratio * levels k. The local binary recurrence encodes the physical fact that composing a recognition event at level k+1 with one at level k produces an event at level k+2, with coefficients counting sub-events in the discrete ledger.
proof idea
The declaration is the structure definition itself. It directly introduces the fields ladder, coeff_a, coeff_b, the two positivity hypotheses, and the single equation local_recurrence without any tactics or lemmas.
why it matters
This structure supplies the input type for the downstream theorem hierarchy_dynamics_forces_phi, which concludes that the ladder ratio equals φ under the minimality condition IsMinimalRecurrence. It fills the structural gap between T5 (J-uniqueness) and T6 (φ forced by self-similarity) by packaging the recurrence forced by locality and discreteness in the zero-parameter ledger. The module doc states that minimality then forces coefficients (1,1), yielding σ² = σ + 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.