policyIdMatches
plain-language theorem explainer
A two-field match predicate: a policy-identity record agrees with a stated name and SHA-256 digest. Certificate authors cite it to pin an external RG-transport artifact by immutable Lean metadata. The body is the conjunction of those two string equalities; no numerics are involved.
Claim. Given an RG-transport policy identity record $id$ and strings $\mathrm{name}$, $\mathrm{sha}$, the match holds if and only if the record's policy name equals $\mathrm{name}$ and its certificate SHA-256 equals $\mathrm{sha}$.
background
The module binds an external RG-transport certificate policy to immutable Lean metadata (policy name, artifact path, generation time, generator script, SHA-256, and a short summary). It does not run RG transport inside Lean; it only supplies an auditable identity anchor so downstream certificates can name an exact policy artifact rather than bare transported numbers.
The identity carrier is the structure RGTransportPolicyIdentity: six string fields, with DecidableEq. The two fields that matter for matching are the human-readable policy name and the certificate SHA-256. Sibling definitions elsewhere that expose a .name field (kernel families, alignment protocols) are unrelated; only this structure is in scope here.
proof idea
Definitional, not a proof. The predicate is the conjunction of two field equalities on the identity record: policy name versus the supplied name string, and certificate SHA-256 versus the supplied digest string. Downstream theorems discharge it by simp against a concrete canonical record.
why it matters
Gives certificate theorems a single, reusable match surface instead of ad-hoc field comparisons. The immediate consumer is canonical2025Q4_matches, which asserts that the Q4-2025 canonical identity matches the fixed name RS_CANONICAL_2025_Q4 and a fixed SHA-256. That pins the external RG-transport policy artifact the verification layer is allowed to cite. Within Recognition Science this sits in the verification layer: it anchors external numerics to Lean metadata without claiming the transport calculation itself. No forcing-chain step (T0–T8) is at stake; the value is auditability of the certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.