LocalComposition
plain-language theorem explainer
LocalComposition equips a ZeroParameterLedger with a composition map that equals the adjacent level ratio at every step. Researchers deriving LocalBinaryRecurrence from scale-free ledgers cite this structure when closing the T5 to T6 step. The definition is a direct three-field structure that encodes the ratio form and positivity with no further lemmas.
Claim. Let $L$ be a ledger whose levels satisfy $0 < L(n)$ for all $n$ and $L(n)/L(n+1) = L(0)/L(1)$ for every $n$. A LocalComposition on $L$ is a map $c : ℕ → ℝ$ such that $c(k) = L(k)/L(k+1)$ and $c(k) > 0$ for all $k$.
background
ZeroParameterLedger consists of a positive real sequence whose adjacent ratios are constant, so the ledger admits no external scale. LocalComposition requires that any composition rule on these levels must be exactly the adjacent ratio and must remain positive. The module uses this structure to derive that level-(k+2) composites depend only on levels k+1 and k, closing Gap 1b in the T5→T6 bridge.
proof idea
This is a structure definition. The three fields directly state the compose function, its equality to the adjacent ratio, and positivity; no lemmas or tactics are invoked.
why it matters
binary_is_minimal applies this structure to conclude that the composition is uniform across levels. The definition supplies the ratio-only rule needed for the module's three-step argument that zero parameters force binary recurrence, thereby supporting LocalBinaryRecurrence in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.