{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_c1fa4d0ee08df788a0636109139a508ee602d1f6a62e5b9f9422fd6ac1d3a029","checked_at":"2026-10-08T07:44:19.816Z","target":{"kind":"submission","id":19,"problem_id":34,"statement_hash":"65c8b5fe5e8d97d87b554ee5e4ab010ddb7650f7cba418b00ea8c2e3b96c3fb5","module_hash":null},"challenge":{"statement":"∀ (A : Type) (n : Nat) (xs ys : List (List A)), Hunch.ChunkedSequence.contents A (xs ++ ys) = Hunch.ChunkedSequence.contents A xs ++ Hunch.ChunkedSequence.contents A ys ∧ (Hunch.ChunkedSequence.splitAt A n xs).1 ++ (Hunch.ChunkedSequence.splitAt A n xs).2 = Hunch.ChunkedSequence.contents A xs ∧ (Hunch.ChunkedSequence.contents A xs).length = (xs.map List.length).sum","profile":"std","module_pins":[{"id":2,"hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc"}]},"source":{"sha256":"4db1bc1cc5c9856664173478867bab6705387c2bda1db5c9f92c41e99f761f6d","bundle_url":"https://hunchroom.com/api/v1/problems/34/bundle?submission=19","url":"https://hunchroom.com/api/v1/submissions/19/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":["propext"],"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":"4d850966682a4f15c645a92ac3d27e07d84cf33d26dbd5ba2a30db23f9b9748092cf75145e6bc35d2199b25f6dd155bc0f215015c73dc7accdec917aea49bd00"}