zeroKnobsExports
plain-language theorem explainer
Registers the nine named dimensionless theorems that form the zero-knobs verification bundle: no free parameters, only forced identities and bounds. Auditors and export renderers cite this list to discover which core claims are parameter-free. The body is a static string list, not a proof.
Claim. The zero-knobs export is the fixed list of nine theorem names: $K\_\mathrm{gate}$, light-cone step bound, eight-tick minimum cover, exact period $8$, discrete $d^2=0$, discrete Bianchi, display-speed identity, $45$-gap clock-lag identity $\delta_{\mathrm{time}}=3/64$, and recognition lower-bound saturation.
background
Module Verification.Knobs holds discoverable export registries for the Recognition Science verification layer. A "knob" is a free numerical parameter; zero-knobs means the claim is fully forced (dimensionless identity or bound with no tunable constants).
Upstream items named in the list include the light-cone step bound (radial advance at most $c$ times elapsed time along local reachability), the eight-tick minimum (any surjective pass over $3$-bit patterns has length at least $8$, the Nyquist-style $2^3$ obstruction), and the $45$-gap clock-lag identity $\delta_{\mathrm{time}}=3/64$ proved by rational arithmetic. Other names point at discrete exterior-calculus identities, display-speed normalization, and recognition lower-bound saturation.
The list is the machine-readable catalog of those core dimensionless results.
proof idea
No proof. The declaration is a @[simp] definition equal to a concrete List String of nine fixed theorem names. Downstream renderers and export checks read the list by name; nothing is derived here.
why it matters
This registry is the discoverable surface of the zero-knobs bundle: the claims RS treats as parameter-free. It feeds the parallel export in Verification.Rendered.zeroKnobsExports, which re-lists the same names for rendered claim pages.
Framework landmarks touched by the named entries include the eight-tick octave (T7: period $2^3$, eight_tick_min / period_exactly_8), light-cone causality (cone_bound), and the dimensionless $45$-gap time fraction. Keeping the catalog explicit lets auditors verify that the verification surface does not smuggle free constants under those names.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.