IndisputableMonolith.Verification.RGTransportPolicyIdentity

   1import Mathlib
   2
   3/-!
   4# RG Transport Policy Identity (Lean-side Binding)
   5
   6This module binds a declared external RG-transport certificate policy to
   7immutable Lean metadata (policy name + artifact hash + summary).
   8
   9It does not implement RG transport numerics inside Lean. Instead, it provides an
  10auditable identity anchor so downstream certificates can reference an exact
  11policy artifact, not just transported numbers.
  12-/
  13
  14namespace IndisputableMonolith
  15namespace Verification
  16
  17/-- Immutable identity metadata for an external RG transport policy artifact. -/
  18structure RGTransportPolicyIdentity where
  19  policyName : String
  20  certificatePath : String
  21  generatedAtUTC : String
  22  generatorScript : String
  23  certificateSha256 : String
  24  policySummary : String
  25  deriving Repr, DecidableEq
  26
  27/-- Canonical Q4-2025 RG transport policy identity.
  28
  29Mirrors `data/certificates/rg_transport/canonical_2025_q4.json`.
  30The hash is SHA-256 of that JSON artifact. -/
  31def canonical2025Q4 : RGTransportPolicyIdentity where
  32  policyName := "RS_CANONICAL_2025_Q4"
  33  certificatePath := "data/certificates/rg_transport/canonical_2025_q4.json"
  34  generatedAtUTC := "2026-02-16T04:39:34Z"
  35  generatorScript := "tools/rg_transport_certify.py"
  36  certificateSha256 := "558450033973f51d9041678998a9d9b83102559b0cf12636d4dd63da981bafd7"
  37  policySummary :=
  38    "Canonical SM RG transport policy for RS mass comparisons. "
  39    ++ "Declared convention for scheme/loops/thresholds/integrator; "
  40    ++ "used only for transport/PDG comparison (not model-layer fitting)."
  41
  42/-- Lightweight matcher for policy identity checks in downstream certificates. -/
  43def policyIdMatches (id : RGTransportPolicyIdentity) (name sha : String) : Prop :=
  44  id.policyName = name ∧ id.certificateSha256 = sha
  45
  46theorem canonical2025Q4_matches :
  47    policyIdMatches canonical2025Q4
  48      "RS_CANONICAL_2025_Q4"
  49      "558450033973f51d9041678998a9d9b83102559b0cf12636d4dd63da981bafd7" := by
  50  simp [policyIdMatches, canonical2025Q4]
  51
  52theorem canonical2025Q4_path :
  53    canonical2025Q4.certificatePath =
  54      "data/certificates/rg_transport/canonical_2025_q4.json" := rfl
  55
  56theorem canonical2025Q4_summary_nonempty :
  57    canonical2025Q4.policySummary ≠ "" := by
  58  native_decide
  59
  60end Verification
  61end IndisputableMonolith
  62