module module

`IndisputableMonolith.Verification.RGTransportPolicyIdentity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (6)

structure RGTransportPolicyIdentity L18
def canonical2025Q4 L31
def policyIdMatches L43
theorem canonical2025Q4_matches L46
theorem canonical2025Q4_path L52
theorem canonical2025Q4_summary_nonempty L56