BinaryRecurrence
BinaryRecurrence equips a zero-parameter ledger with a positive real ratio r such that its level sequence obeys the linear relation L(k+2) = r L(k+1) + (1-r) L(k) for every k. Researchers deriving the T5 to T6 bridge in Recognition Science cite it when converting dimensionless ledger constraints into a local composition rule. The entry is a pure structure definition that packages the ratio, its positivity, and the recurrence predicate with no further computation.
claimA binary recurrence for a zero-parameter ledger $L$ consists of a positive real $r$ such that $L(k+2) = r L(k+1) + (1-r) L(k)$ holds for all natural numbers $k$.
background
A zero-parameter ledger is a sequence of positive reals whose consecutive ratios are identical and fixed by the first two terms, enforcing the complete absence of any external scale. The module derives binary recurrence from this property together with a local composition rule that builds each level from finitely many predecessors. Upstream, the Recognition module supplies the base ledger L while Cycle3.L supplies a conserved instance used in related cycle arguments.
proof idea
The declaration is a structure definition that directly encodes the ratio field, its positivity predicate, and the two-point recurrence equality as structure fields.
why it matters in Recognition Science
This structure supplies the precise object needed to state LocalBinaryRecurrence, the missing locality condition in the T5 to T6 bridge of the unified forcing chain. It supports the step from J-uniqueness to the phi fixed point by guaranteeing that composition depends only on adjacent levels, which in turn licenses the eight-tick octave and the emergence of three spatial dimensions. The module document positions it as the key intermediate that closes Gap 1b without introducing new parameters.
scope and limits
- Does not prove existence of a ratio satisfying the recurrence for every zero-parameter ledger.
- Does not fix the numerical value of the ratio.
- Does not apply to ledgers that admit external scales.
- Does not extend to recurrences of order higher than two.
formal statement (Lean)
44structure BinaryRecurrence (L : ZeroParameterLedger) where
45 ratio : ℝ
46 ratio_pos : 0 < ratio
47 recurrence : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
48 actually_binary : ∀ k, L.levels (k + 2) = ratio * L.levels (k + 1) + (1 - ratio) * L.levels k
49
50/-! ## Key Theorems -/
51