gap_delta_time_identity
plain-language theorem explainer
The dimensionless 45-gap clock-lag fraction equals 3/64 as an exact rational identity. Export and zero-knobs verification bundles cite it to register a parameter-free timing fact. The proof is a one-line rational normalization via norm_num.
Claim. As rationals, $45/960 = 3/64$. This is the dimensionless clock-lag fraction $\delta_{\mathrm{time}} = 3/64$ tied to the 45-gap.
background
Verification.Exports collects small, fully closed identities so downstream bundles can list them by name without free parameters. The present claim is pure arithmetic over $\mathbb{Q}$: a discrete 45-gap counted against a 960-tick normalization reduces to the fraction $3/64$, written $\delta_{\mathrm{time}}$.
There are no upstream lemmas. The module imports only Mathlib; the local convention is that such equalities are dimensionless display facts, not continuum derivations. Sibling export lists treat this name as one of the discoverable zero-knobs proofs.
proof idea
Term-style tactic proof: a single norm_num call evaluates both rational sides and closes the equality. No intermediate lemmas, rewrites, or hypotheses are used.
why it matters
Registers the 45-gap clock-lag identity inside the zero-knobs export lists in Verification.Knobs and Verification.Rendered, which document core dimensionless theorems for discoverability. Those bundles treat $\delta_{\mathrm{time}} = 3/64$ as a closed arithmetic fact rather than a fitted constant, consistent with RS emphasis on forced discrete timing structure (eight-tick octave and related period identities). It does not itself advance the T0–T8 forcing chain; it only certifies a display fraction used by the verification surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.