zeroKnobsExports
plain-language theorem explainer
A fixed registry of nine string names for dimensionless, parameter-free theorems in the zero-knobs verification bundle. Auditors and export tooling cite it to enumerate which core results are treated as knob-free. The body is a literal list definition, marked simp for easy rewriting.
Claim. The zero-knobs export registry is the fixed list of names $K\_\mathrm{gate}$, cone bound, eight-tick minimum, period exactly $8$, dec $dd=0$, dec Bianchi, display speed identity, gap $\delta$-time identity, and recognition lower-bound saturation.
background
The module collects rendered summaries of dimensionless claims: statements whose content does not depend on free calibration parameters ("knobs"). In Recognition Science verification, a zero-knobs bundle is the set of such theorems that can be checked or exported without tuning constants.
Upstream entries named in the list include the light-cone step bound (radial advance controlled by $c$ times time advance under 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 gap clock-lag identity $\delta_{\mathrm{time}} = 3/64$ obtained from $45/960$. A parallel knobs-module list carries the same discoverable export role.
The list is therefore a catalog, not a proof of the named results; those live in Foundation, LightCone, Patterns, and Verification.Exports.
proof idea
Definitional: the value is the concrete nine-element List String written in the body. The @[simp] attribute makes the list unfold under simplification. No tactics or lemmas are applied.
why it matters
Gives a single discoverable handle for the zero-knobs dimensionless core used by verification and knobs export. Downstream, the knobs-module twin list mirrors this registry so tooling can treat the bundle as data. The named items touch framework landmarks: eight-tick / period-$8$ structure (T7 octave), cone bounds on causal reach, and the dimensionless 45-gap time fraction. It does not close open physics claims; it only indexes which proved dimensionless statements are advertised as knob-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.