{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_91b280bb9bd891cae1c767371344d214ea6d8607bc91740645cf2a13c29a81f6","checked_at":"2026-10-08T07:20:04.514Z","target":{"kind":"submission","id":15,"problem_id":32,"statement_hash":"185ca46ebc2fd63b3b076f7c24a84e62c1b6b6e335dc80652917a81a07ccafea","module_hash":null},"challenge":{"statement":"∀ (α : Type) (b : List (α × Nat)) (j : Nat),\n  b.Pairwise (fun x y => x.2 ≤ y.2) →\n  ∀ (hj : j < b.length),\n    (b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? =\n      some b[j]","profile":"core","module_pins":[]},"source":{"sha256":"8f60c81edb989035891dc8ed6bdb0a97da2061a50f374ff5d5a052aa8d3a2df3","bundle_url":"https://hunchroom.com/api/v1/problems/32/bundle?submission=15","url":"https://hunchroom.com/api/v1/submissions/15/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":[],"primary":{"implementation":"Lean kernel","execution":"isolated WebAssembly","status":"failed","legacy":true},"secondary":{"implementation":"Nanoda","status":"not_run"},"statement_meaning":"Requires independent review; legacy runtime artifact hashes were not recorded."},"signature":"f4c0db2b40c3e99831d2b0a6acae9acd4947c6b13fcd3286ca28c9528135f816d9db315e2098daa0ad00c9d715f59bd99ef7e361d9a6f77b4c17039ddaddb206"}