GateSpec
plain-language theorem explainer
A small data record for a verification gate: a string identifier, a list of symbolic input names, and a symbolic output expression. Used by the rendered verification layer to export gate checks (for example the K-gate pass condition) without embedding Lean proof objects. Definition only; no proof content.
Claim. A gate specification is a triple $(\mathrm{id},\ \mathrm{inputs},\ \mathrm{output})$ where $\mathrm{id}$ is a string label, $\mathrm{inputs}$ is a finite list of symbolic input names, and $\mathrm{output}$ is a symbolic expression (or pass criterion) written as a string.
background
The module collects rendered summaries of dimensionless claims for export and audit. A rendered claim is a human-readable packaging of a theorem that has already been proved elsewhere in the monolith; this file does not re-prove physics, it only shapes the export surface.
A gate, in this verification layer, is a named check that consumes named dimensionless inputs and reports a symbolic pass criterion. The structure holds only strings: identifiers and formula text. It does not carry numeric values, units, or Lean propositions.
Upstream edges touch identity maps in cost algebra and Peano arithmetic only as ambient imports of the broader monolith; they do not constrain the fields of this record. The local meaning is fixed by the module doc: rendered summary of a dimensionless claim.
proof idea
No proof. This is a structure declaration with three fields (id, inputs, output) and a Repr instance for printing. There is no theorem body, no tactics, and no lemmas applied.
why it matters
Gives the verification export a uniform type for symbolic gates so downstream lists can be typed and pretty-printed. The sole direct consumer is gatesRendered, which builds an example list whose first entry is the K-gate: inputs such as $u(\ell_0)$, $u(\lambda_{\mathrm{rec}})$, $k$, optional density, and $K_B$, with output the standardized residual $Z = |K_A - K_B| / (k \cdot \sqrt{u_{\ell_0}^2 + u_{\lambda_{\mathrm{rec}}}^2})$ and pass condition $Z \le 1$.
In the Recognition framework this sits in the verification/export layer rather than the forcing chain (T0–T8). It does not derive $J$, $\varphi$, the eight-tick period, or $D=3$; it only packages already-proved dimensionless checks for external audit of zero-knobs claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.