RGTransportPolicyIdentity
plain-language theorem explainer
Defines an immutable Lean record that pins an external RG-transport policy artifact by name, path, generation time, script, SHA-256 hash, and summary. Verification authors cite it when binding certificates to a fixed policy rather than free-floating numbers. It is a plain structure with decidable equality; no proof content.
Claim. An RG transport policy identity is a record of six strings: policy name, certificate path, UTC generation timestamp, generator script path, SHA-256 digest of the certificate artifact, and a human-readable policy summary. Two such records are equal precisely when all six fields agree.
background
The module is a Lean-side binding layer for external renormalization-group (RG) transport certificates. It does not compute transport numerics inside Lean. It only anchors downstream certificates to an exact external policy artifact (name plus content hash), so audits can reject silent policy drift.
The structure packages the metadata that such an anchor needs: who named the policy, where the JSON lives, when and by which script it was produced, the SHA-256 of that JSON, and a short summary. Decidable equality is derived so matchers can compare identities propositionally.
Local convention: the canonical Q4-2025 instance mirrors data/certificates/rg_transport/canonical_2025_q4.json; the stored hash is the SHA-256 of that file. Upstream graph edges that mention identity events or forcing-chain dimension results are name collisions, not mathematical dependencies of this record type.
proof idea
No proof. This is a structure declaration with six String fields and automatic Repr and DecidableEq instances. Downstream values are filled by field assignment (see the canonical Q4-2025 constant); equality of identities reduces to componentwise string equality.
why it matters
In the Verification domain this type is the auditable handle for RG transport policy. Downstream, canonical2025Q4 is the frozen Q4-2025 instance (name RS_CANONICAL_2025_Q4 and a fixed SHA-256), and policyIdMatches is the lightweight predicate that checks a name/hash pair against a stored identity.
That split matters for Recognition Science certificate hygiene: transported constants and ladder quantities can change with numerics, but the policy artifact they claim to obey is pinned by hash. The module doc states the intent explicitly: downstream certificates reference an exact policy artifact, not just transported numbers. It does not itself close a T0–T8 forcing step; it is infrastructure so gravity and constant-transport certificates stay reproducible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.