locality_cert_exists
plain-language theorem explainer
Existence of a LocalityCert is established for any zero-parameter ledger, bundling uniform level ratios and geometric progression of levels. Researchers deriving local binary recurrence from ledger constraints in the Recognition Science T5-T6 bridge would cite this result. The proof is a direct term construction that populates the certificate fields using the uniform_ratio and locality_from_ledger theorems.
Claim. There exists a structure $C$ such that for every zero-parameter ledger $L$, the ratio $L_n / L_{n+1} = L_0 / L_1$ holds for all $n$, and there exists $r > 0$ with $L_{k+1} = r L_k$ for all $k$.
background
A ZeroParameterLedger admits only dimensionless ratios with no external scales. The LocalityCert structure packages two properties: uniform ratios (constant across all level steps) and geometric progression (levels form a geometric sequence with positive common ratio). The module derives locality from ledger by showing zero parameters force ratio-only composition and minimal binary order. Upstream, uniform_ratio applies the no_external_scale axiom to fix the ratio at the base level, while locality_from_ledger extracts the positive ratio $r = L_1 / L_0$ and verifies the recurrence.
proof idea
The proof is a term-mode construction that directly builds the LocalityCert instance. It maps the uniform field to the function applying uniform_ratio to any ledger and the geometric field to the function applying locality_from_ledger to any ledger.
why it matters
This theorem supplies the existence witness for LocalityCert, which completes the derivation of LocalBinaryRecurrence from the zero-parameter ledger assumption and feeds the T5 to T6 bridge in the forcing chain. It confirms geometric self-similarity with positive ratio, consistent with the phi-ladder fixed point. The result carries no open scaffolding as the module reports zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.