{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_e40ffed0d9b124ab73e73fa2eed2b11dd6e6464a7449be041c7e721d69f51758","checked_at":"2026-10-08T07:45:21.502Z","target":{"kind":"submission","id":20,"problem_id":35,"statement_hash":"b29dcff892c50051bab9a5502dfe9aeaeca7aeac7b066ab0c3838699afd6f17d","module_hash":null},"challenge":{"statement":"∀ (A : Type) (n deleted : Nat) (inserted chunks : List (List A)), n ≤ (Hunch.ChunkedSequence.contents A chunks).length → deleted ≤ (Hunch.ChunkedSequence.contents A chunks).length - n → (Hunch.ChunkedSequence.splice A n deleted inserted chunks).length = (Hunch.ChunkedSequence.contents A chunks).length - deleted + (Hunch.ChunkedSequence.contents A inserted).length","profile":"std","module_pins":[{"id":2,"hash":"9537027be7db9dcc4d4eb2eee415ed4e015adcdae5125a7926ef5b3361dda1fc"}]},"source":{"sha256":"d8d6cb5d0e97e833ea673c7a142c596ad9a56d4ae033d05402beb5076224f0ba","bundle_url":"https://hunchroom.com/api/v1/problems/35/bundle?submission=20","url":"https://hunchroom.com/api/v1/submissions/20/source"},"policy":"oa-lean-v1","runtime":null,"dependencies":[],"axioms":["propext","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":"a9b714bed35518cf8488e60239965365441013ddc1437d18171dfd3c7e6e476d89b59cc64670c64460ce83f9ca6eae1580222d49e1770064c694f7b72db12c05"}