binary_is_minimal
plain-language theorem explainer
Under a zero-parameter ledger the composition map of any local composition rule is constant and equals the base ratio at level zero. Researchers deriving the T5 to T6 locality bridge in Recognition Science cite this result to confirm that only adjacent-level ratios survive the zero-scale constraint. The proof is a direct term reduction that unfolds the definition of compose and invokes the uniform-ratio lemma.
Claim. Let $L$ be a zero-parameter ledger whose level sequence satisfies $L(n)/L(n+1)=L(0)/L(1)$ for every natural $n$. Let $C$ be a local composition for $L$, so that $C(k)=L(k)/L(k+1)$ for each $k$. Then $C(k)=C(0)$ holds for all natural numbers $k$.
background
A ZeroParameterLedger consists of a positive real sequence on the naturals together with the axiom that every positive rescaling leaves the adjacent ratios unchanged; the only free datum is therefore the single ratio $L(0)/L(1)$. A LocalComposition on such a ledger is a map $C$ whose value at each level is exactly the adjacent ratio of the ledger and is required to be positive. The module's setting is the derivation of LocalBinaryRecurrence from these ledger axioms alone, as stated in the module header: the T5 to T6 bridge assumes that level-$(k+2)$ composites depend only on levels $k+1$ and $k$. The upstream uniform_ratio theorem supplies the constant-ratio property used here.
proof idea
The term proof introduces the arbitrary level $k$, rewrites both sides of the target equality by the compose_from_levels field of LocalComposition, and finishes by exact application of the uniform_ratio theorem at that $k$.
why it matters
The result supplies the second step of the module's three-part argument: zero parameters force ratio-only composition, and the minimal such composition is binary. It therefore closes the gap that lets locality_from_ledger deliver LocalBinaryRecurrence, the missing hypothesis for the T5 to T6 forcing step. No downstream uses are recorded yet; the theorem stands as an internal lemma supporting the ledger-to-recurrence derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.