locality_from_ledger
plain-language theorem explainer
locality_from_ledger shows that any zero-parameter ledger has levels forming a geometric sequence with positive common ratio r. Researchers closing the T5 to T6 bridge in Recognition Science cite it to justify the local binary recurrence hypothesis. The proof constructs r directly as the ratio of the first two levels and invokes uniform_ratio to establish constancy for every subsequent step.
Claim. Let $L$ be a zero-parameter ledger: a function levels $: ℕ → ℝ$ such that levels$(n) > 0$ for all $n$ and all adjacent ratios equal the fixed base ratio levels$(0)$/levels$(1)$. Then there exists $r > 0$ with levels$(k+1) = r · levels$(k)$ for every natural number $k$.
background
The LocalityFromLedger module derives the local binary recurrence required for the T5→T6 transition. A ZeroParameterLedger is the structure whose levels map naturals to reals, all_positive ensures strict positivity, and no_external_scale forces every adjacent ratio to equal the base ratio levels 0 / levels 1 independently of any positive scaling parameter. The upstream uniform_ratio theorem states that ∀ n, levels n / levels (n+1) = levels 0 / levels 1, obtained directly by instantiating no_external_scale. Module documentation frames this as closing Gap 1b: zero parameters imply ratio-only composition, which in turn forces minimal order-two recurrence.
proof idea
The term proof selects r := levels 1 / levels 0. Positivity of r is immediate from all_positive at 0 and 1. For the universal quantifier, fix arbitrary k, apply uniform_ratio L k to equate the local ratio to the base ratio, rewrite both sides via div_eq_div_iff, then finish with field_simp and linarith.
why it matters
The result supplies the geometric property used by locality_cert_exists to build the full LocalityCert. It thereby discharges the LocalBinaryRecurrence assumption needed for the T5 J-uniqueness to T6 phi-fixed-point step in the forcing chain. In the Recognition Science setting it confirms that a ledger with no external scales admits only dimensionless ratios, closing the argument that composition order must be exactly two without introducing new parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.