dimlessClaimsRendered
plain-language theorem explainer
Static catalog of three dimensionless verification claims for rendering: the K-gate ratio equality of recognition time to kinematic wavelength, the lower bound that any complete 3-bit pattern cover has period at least 8, and existence of a period-8 cover. Export or dashboard layers in the verification surface would cite this list. The body is a literal three-element list with proved flags set true.
Claim. A fixed list of three rendered dimensionless claims: (i) $(\tau_{\mathrm{rec}}/\tau_0)=(\lambda_{\mathrm{kin}}/\ell_0)$, marked proved; (ii) every complete cover of 3-bit patterns has period at least $8$, marked proved; (iii) there exists a cover with period exactly $8$, marked proved.
background
The module packages human-readable summaries of dimensionless RS claims. Each entry is a RenderedClaim: a string id, a statement string, and a Boolean proved flag. No proof obligations live here; the structure is display-only.
The first claim is the K-gate: recognition time $\tau_{\mathrm{rec}}=(2\pi)/(8\ln\varphi)\cdot\tau_0$ and kinematic wavelength $\lambda_{\mathrm{kin}}=(2\pi)/(8\ln\varphi)\cdot\ell_0$ share the same dimensionless ratio to their base units. The second and third claims come from the pattern layer: for 3-bit patterns any surjective pass has length at least 8 (the eight-tick minimum), and a cover of period exactly 8 exists. That bound is the discrete content behind the T7 eight-tick octave.
proof idea
Pure definition: a three-element list literal. Each record hard-codes id, statement text, and proved := true. No tactics, no lemmas applied at this site; the proved flags are annotations pointing at theorems proved elsewhere (notably the eight-tick minimum for 3-bit covers).
why it matters
Gives the Verification.Rendered surface a concrete, simp-normal sample of dimensionless claims so exporters and gate summaries have stable ids (K_gate, eight_tick_min, period_exactly_8). It sits next to sibling gate and zero-knob export lists in the same module.
Framework-wise it surfaces two landmarks: the K-gate tying $\tau_{\mathrm{rec}}$ to $\lambda_{\mathrm{kin}}$ in RS-native units, and the T7 eight-tick octave (period $2^3$) via the 3-bit covering lower bound and exact period-8 cover. Details and real proofs remain in core Verification and Patterns; this file only renders placeholders for the audit UI.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.