{"name":"syz-lean-skeleton","lang":"bash","entry":"check_lean.sh","script":"bash check_lean.sh --repo repo --slot-map slotmap.json --out verdict.json","input":{"type":"object","required":["build_exit_code","sorry_count","slot_map","negative_control"],"properties":{"build_exit_code":{"type":"integer"},"sorry_count":{"type":"integer","minimum":0},"slot_map":{"type":"object","required":["degeneration","dimension","epsilon","fiber_smoothness","phase"]},"negative_control":{"type":"object","required":["mutated_slot","build_failed"]}}},"output":{"type":"object","required":["verdict","checks"],"properties":{"verdict":{"enum":["pass","fail","invalid"]},"checks":{"type":"array"}}},"validation":{"null_tolerance":true,"enumeration_closure":{"closure":"Five quantifier slots must map one-to-one to Lean declarations; sorry_count is computed by the script rather than self-reported; the negative control must show a mutated slot producing a failed build. The script enumerates the five slot keys and self-checks the slot count against the spec's five.","slot_key_count":5},"proposition_fidelity":{"artifact":"pin://f98855bc0903e5a4cabb499c5000aa2b9c5a5a4a86fd2b6e5fbb826a1a9a66e8i0","description":"Independent verifier-contract document published before the task, describing for each node what its verifier checks, what the machine can decide, and what is left to human review. Node-specific section: see the matching node heading in the artifact."}}}