canonical2025Q4_path
plain-language theorem explainer
The canonical Q4-2025 RG-transport policy record stores its certificate path as the fixed relative path to the JSON artifact under data/certificates/rg_transport. Auditors and downstream certificate binders cite this equality to pin the on-disk location without reopening the structure definition. The proof is pure reflexivity against the structure field.
Claim. The certificate-path field of the canonical Q4-2025 RG-transport policy identity equals the string $\texttt{data/certificates/rg\_transport/canonical\_2025\_q4.json}$.
background
The module binds an external RG-transport certificate policy to immutable Lean metadata: policy name, artifact path, generation timestamp, generator script, and SHA-256 hash. It does not run RG numerics in Lean; it only anchors downstream certificates to one exact policy artifact.
The upstream definition canonical2025Q4 is that identity record. Its doc-comment states it mirrors data/certificates/rg_transport/canonical_2025_q4.json and that the hash is the SHA-256 of that JSON. The path field is therefore part of the declared binding, not a computed transport result.
proof idea
One-line reflexivity: unfold the structure value of the canonical Q4-2025 policy identity and match the certificatePath field against the quoted path string. No lemmas or tactics beyond rfl.
why it matters
Gives a named, machine-checkable equality for the on-disk certificate path so verification code can quote the path without hard-coding a free string. Downstream certificates that reference the canonical Q4-2025 policy can rely on this field equality as the Lean-side path anchor. No used-by edges are recorded yet; the sibling match and summary lemmas in the same module are the natural consumers. This is verification scaffolding around RG transport, not a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.