gatesRendered
plain-language theorem explainer
Static catalogue of symbolic verification gates for the rendered summary layer. Currently holds one entry: the K-gate, with its input symbols and the pass criterion Z ≤ 1. Anyone wiring a dimensionless claim display or audit UI cites this list. The body is a one-element list literal of GateSpec records; no proof work.
Claim. The constant list of rendered gate specifications equals a singleton whose sole element is the K-gate: inputs $u(\ell_0)$, $u(\lambda_{\mathrm{rec}})$, $k$, optional $\rho$, and $K_B$; symbolic output $Z = |K_A - K_B| / (k \cdot \sqrt{u_{\ell_0}^2 + u_{\lambda_{\mathrm{rec}}}^2})$ with pass condition $Z \le 1$.
background
Module Verification.Rendered packages human-readable summaries of dimensionless claims. A gate specification is a triple of strings: an identifier, a list of input symbols, and a symbolic output formula. That structure is purely presentational; it does not encode a Lean proposition.
The single gate recorded here is the K-gate. Its $Z$ is a normalized absolute discrepancy between two K-values, scaled by a product of a dimensionless factor $k$ and a quadrature of two uncertainty terms $u(\ell_0)$ and $u(\lambda_{\mathrm{rec}})$. Passing means that normalized discrepancy is at most one.
Upstream name collisions on Z (path-sum measure, mass-anchor integer map, certified species map) are unrelated identifiers; this gate's $Z$ is only the symbolic string in the output field.
proof idea
Definition by list literal. One GateSpec record is constructed with fixed string fields for id, inputs, and output; the definition is the singleton list of that record. The @[simp] attribute exposes the list under simplification. No lemmas are applied.
why it matters
Gives the verification layer a stable, inspectable catalogue of which gates appear in rendered claim summaries. Downstream consumers (none registered yet in the graph) can iterate the list to display or audit gate metadata without hard-coding strings. It sits beside sibling exports such as the zero-knobs theorem list and the dimensionless-claims render list, completing the presentational side of the verification bundle. It does not itself discharge any forcing-chain step (T0–T8) or prove a numerical bound; it only names the K-gate pass criterion in symbolic form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.