LocalComposition
plain-language theorem explainer
LocalComposition equips a zero-parameter ledger with a composition map whose value at each level equals the adjacent ratio of ledger levels and is required to be positive. Workers deriving the binary recurrence needed for the T5 to T6 step cite this structure when they reduce composition rules to dimensionless ratios. The declaration is introduced directly as a three-field structure whose fields encode the ratio identity and positivity.
Claim. Let $L$ be a zero-parameter ledger. A local composition on $L$ is a function $c : ℕ → ℝ$ such that $c(k) = L(k)/L(k+1)$ for every natural number $k$ and $c(k) > 0$ for every $k$.
background
A zero-parameter ledger consists of a sequence of positive real numbers (levels) whose adjacent ratios are all identical; the no-external-scale axiom forces every ratio $levels(n)/levels(n+1)$ to equal the base ratio $levels(0)/levels(1)$. The module LocalityFromLedger uses this property to derive the locality condition required by the T5→T6 bridge, which assumes that level-(k+2) composites depend only on levels k+1 and k. The upstream compose definition from VirtueComposition supplies an additive-multiplicative pattern on effects, while the two L ledger instances illustrate minimal debit-credit ledgers that conserve total value.
proof idea
Definition of the LocalComposition structure whose three fields directly encode the ratio identity and positivity constraint.
why it matters
The structure is the input type for binary_is_minimal, which concludes that any composition referencing levels below k-1 introduces an independent ratio forbidden by zero parameters. It therefore supplies the concrete composition rule needed to obtain LocalBinaryRecurrence and close the locality derivation in the forcing chain. The definition sits inside the argument that zero-parameter ledgers force ratio-only composition, the first of the three steps listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.