ratio_only
plain-language theorem explainer
A zero-parameter ledger forces all level ratios to be powers of the single adjacent ratio. Researchers closing the locality gap in the Recognition Science forcing chain cite this result. The proof relies on induction over the natural-number indices combined with the constant-ratio axiom and linear-arithmetic closure.
Claim. For a zero-parameter ledger $L$ whose level values are strictly positive and whose adjacent ratios are constant, the ratio of levels at indices $m$ and $n$ equals the base adjacent ratio raised to the power $m-n$.
background
The ZeroParameterLedger structure encodes a ledger with no external scales: its level sequence satisfies a constant adjacent ratio independent of any positive multiplier. This property is the key hypothesis for deriving dimensionless composition rules. The surrounding module uses this to bridge from ledger axioms to the local binary recurrence required by the T5 to T6 step in the unified forcing chain.
proof idea
Proof by induction on the first index m. When m is zero a nested induction on n applies the no-external-scale property to equate ratios, rewrites via division equivalence, and invokes nlinarith on the positivity facts. The successor case for m similarly invokes the scale-invariance axiom once and closes the equality with nlinarith using all positivity assumptions.
why it matters
This result is the initial lemma in the derivation that zero parameters imply ratio-only composition, which then supports the binary-is-minimal theorem and ultimately the locality-from-ledger statement. It directly addresses the gap-1b question in the module by showing that composition rules must be expressible through adjacent-level ratios alone. Within the broader framework it contributes to the T5-J-uniqueness to T6-phi-fixed-point transition by enforcing locality without additional parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.