{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_04e44539f981b04a6b4d6c89f90b58a952e72960818eb4f2c362bdfb7f1cd511","checked_at":"2026-10-08T05:16:39.376Z","target":{"kind":"submission","id":7,"problem_id":22,"statement_hash":"62ae955e299637cd48a4559319f35c4baccebc283a32627b43cd4de5d0645968","module_hash":null},"challenge":{"statement":"∀ (boundaries : List Nat) (j q : Nat),\n  boundaries.Pairwise (fun x y => x ≤ y) →\n  ∀ (hj : j < boundaries.length),\n    (q + (boundaries.filter fun boundary => boundary ≤ q).length < boundaries[j] + j ↔\n      q < boundaries[j]) ∧\n    (boundaries[j] + j < q + (boundaries.filter fun boundary => boundary ≤ q).length ↔\n      boundaries[j] ≤ q) ∧\n    q + (boundaries.filter fun boundary => boundary ≤ q).length ≠ boundaries[j] + j","profile":"core","module_pins":[]},"source":{"sha256":"b85631b93ce6dfa0bb4885ca34a6b6085449aa6e2ab3b5c03fd5e99abf3e992d","bundle_url":"https://hunchroom.com/api/v1/problems/22/bundle?submission=7","url":"https://hunchroom.com/api/v1/submissions/7/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":"0fcb9dbf05d9d485992ab4d1ddf480a2f69b6c53a7307412b235f1ee4fd371399559e1f7fddba7315102b85665748445c3525a433c3f634060b30677bce5bb02"}