uniform_ratio
plain-language theorem explainer
Any zero-parameter ledger has a constant ratio between successive level values independent of index. Researchers deriving binary recurrence and locality from ledger axioms cite this when showing composition rules depend only on adjacent levels. The proof is a one-line wrapper that instantiates the no_external_scale property at unit scale.
Claim. Let $L$ be a zero-parameter ledger with level sequence $ell : mathbb{N} to mathbb{R}$. Then $forall n in mathbb{N}, frac{ell(n)}{ell(n+1)} = frac{ell(0)}{ell(1)}$.
background
A ZeroParameterLedger consists of a sequence of positive real numbers (levels) equipped with the no_external_scale axiom: for every positive real $lambda$ and every natural number $n$, the ratio of level $n$ to level $n+1$ equals the base ratio of level 0 to level 1. This encodes the absence of any external scale parameter. The module derives locality conditions for composition rules from this zero-parameter assumption as part of bridging T5 to T6 by establishing LocalBinaryRecurrence.
proof idea
The proof is a one-line wrapper that applies the no_external_scale field of the ledger at lambda equal to 1 (using positivity of 1) to obtain the uniform ratio for every n.
why it matters
It is invoked in binary_is_minimal to show minimal composition order is 2 and in locality_from_ledger to extract the constant ratio r. This fills the gap for locality_cert_exists and supports derivation of LocalBinaryRecurrence assumed in the T5 to T6 bridge of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.