Verification Rgtransport Policy Identity

Policy identity anchor

In Recognition Science, recognition events, discrete records of comparisons, need a way to be reproduced and audited. The RG transport policy, the declared convention for how mass values are transported and compared against reference data, is one such record. This framework binds that external policy to an immutable identity anchor inside its machine-checked library of formal theorems.

The anchor is a structure called RGTransportPolicyIdentity. It holds six fields: the policy name, the path to its certificate file, the UTC timestamp of generation, the script that generated it, the SHA-256 hash of the certificate artifact, and a plain-language summary. The structure is a definitional choice, a way to model the policy's identity, not a proof about the policy's content.

The framework then defines a canonical instance for the Q4-2025 policy, named RS_CANONICAL_2025_Q4, with its certificate hash set to 558450033973f51d9041678998a9d9b83102559b0cf12636d4dd63da981bafd7. Three theorems are proved about this instance: it matches the expected name and hash, its certificate path is exactly the expected file path, and its summary is nonempty. These are small, mechanical facts, each checked by the kernel.

In plain language, the framework does not implement the transport numerics. It provides a fixed, machine-checked reference point. Downstream certificates can say "this policy, this exact artifact" and point to a stable identity that cannot drift. The payoff is auditability: a reader can verify that a given certificate refers to the precise policy artifact, not just to a transported number.

/-- Immutable identity metadata for an external RG transport policy artifact. -/
structure RGTransportPolicyIdentity where
  policyName : String
  certificatePath : String
  generatedAtUTC : String
  generatorScript : String
  certificateSha256 : String
  policySummary : String
  deriving Repr, DecidableEq

/-- Immutable identity metadata for an external RG transport policy artifact. -/
structure RGTransportPolicyIdentity where
  policyName : String
  certificatePath : String
  generatedAtUTC : String
  generatorScript : String
  certificateSha256 : String
  policySummary : String
  deriving Repr, DecidableEq

/-- Canonical Q4-2025 RG transport policy identity.

Mirrors `data/certificates/rg_transport/canonical_2025_q4.json`.
The hash is SHA-256 of that JSON artifact. -/
def canonical2025Q4 : RGTransportPolicyIdentity where
  policyName := "RS_CANONICAL_2025_Q4"
  certificatePath := "data/certificates/rg_transport/canonical_2025_q4.json"
  generatedAtUTC := "2026-02-16T04:39:34Z"
  generatorScript := "tools/rg_transport_certify.py"
  certificateSha256 := "558450033973f51d9041678998a9d9b83102559b0cf12636d4dd63da981bafd7"
  policySummary :=
    "Canonical SM RG transport policy for RS mass comparisons. "
    ++ "Declared convention for scheme/loops/thresholds/integrator; "
    ++ "used only for transport/PDG comparison (not model-layer fitting)."

theorem canonical2025Q4_matches :
    policyIdMatches canonical2025Q4
      "RS_CANONICAL_2025_Q4"
      "558450033973f51d9041678998a9d9b83102559b0cf12636d4dd63da981bafd7" := by
  simp [policyIdMatches, canonical2025Q4]

theorem canonical2025Q4_path :
    canonical2025Q4.certificatePath =
      "data/certificates/rg_transport/canonical_2025_q4.json" := rfl

theorem canonical2025Q4_summary_nonempty :
    canonical2025Q4.policySummary ≠ "" := by
  native_decide

What this page does not claim

This framework implements or verifies the RG transport numerics themselves. The SHA-256 hash is a claim about the certificate's content being correct, only that the artifact is identified. The policy identity is not a proof that the policy is physically accurate.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/RGTransportPolicyIdentity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: