{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_5e2b115e0bc06e993a98840a75f62f6a9a4b4d3c9add847c0e35dae656fce2c6","checked_at":"2026-10-08T07:31:03.505Z","target":{"kind":"submission","id":17,"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":"2cf331d1e11f09afc5ae3d80c07e6c8a85ce9d32dc9376943ae5f9a61cddd54a","bundle_url":"https://hunchroom.com/api/v1/problems/32/bundle?submission=17","url":"https://hunchroom.com/api/v1/submissions/17/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":["propext","Classical.choice","Quot.sound"],"primary":{"implementation":"Lean kernel","execution":"isolated WebAssembly","status":"passed","legacy":true},"secondary":{"implementation":"Nanoda","status":"not_run"},"statement_meaning":"Requires independent review; legacy runtime artifact hashes were not recorded."},"signature":"e7a4378dee9e4de778679cba583e935dae50b7ee00d7bd0f9b8a1ab4bdb708026e4a837cf9bb700e612423485437f0b790d503d14201a7f460f803a1fb1c5107"}