{"format":"hunch-receipt-v1","algorithm":"Ed25519","key_id":"149adbcaadcde04921fe70bc2e2dcec91c2632606d702595eea6481a11ba9880","payload":{"schema":"hunch-verification-v1","issuer":"https://hunchroom.com","job_id":"job_1bedda3c830ade06c2b1163e153b98a88a62cb83625061bc6b39b5f72e560bb8","checked_at":"2026-10-08T08:00:20.980Z","target":{"kind":"submission","id":24,"problem_id":39,"statement_hash":"71cacefe3ca4d1d0022708dec6804efdf1bd68d8398fbe0d361d8acb1386e486","module_hash":null},"challenge":{"statement":"(∀ m a x : Int, Hunch.SemidirectArithmetic.multiplyEffect m (Hunch.SemidirectArithmetic.addEffect a x) = Hunch.SemidirectArithmetic.addEffect (Hunch.SemidirectArithmetic.transformAdd m a) (Hunch.SemidirectArithmetic.multiplyEffect m x)) ∧ (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, Hunch.SemidirectArithmetic.transformHistory xs a = Hunch.SemidirectArithmetic.transformHistory ys a)","profile":"std","module_pins":[{"id":3,"hash":"150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9"}]},"source":{"sha256":"dcd0c070fef30e792c75dae63c891ddf78fc3b94ca7cd315d3fae5c718d5ce43","bundle_url":"https://hunchroom.com/api/v1/problems/39/bundle?submission=24","url":"https://hunchroom.com/api/v1/submissions/24/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":"b5d4a40f0b3646bd28320e089d5885f2e0ae4c7e33cc1b826f097b0496a880b7b95a771b85c335a4a1442aafb35362bd3872301cc32b796c9b139235ece66e0a"}