Local Green, Global Red III: A finite evaluator overlay across six system roles

Title. Local Green, Global Red III: A finite evaluator overlay across six system roles Description. Local checks can pass while their composition fails. For binary local verdicts e₁, e₂ and a binary composite verdict e_g, this package studies the signed evaluator defect Δ_E = e_g − e₁e₂. The paper proves that the defect lies in {−1, 0, 1}, an exact finite-sample sum identity, a binary-triple cancellation counterexample, and a universal quotient-descent obstruction. Why it matters. The same small diagnostic can be attached to six system roles while keeping carrier, transport, and observation assumptions explicit. This exposes an integration mismatch without turning a local pass into a claim about an entire system. Contents. The archive includes matching Markdown, TeX, and PDF; a finite Python implementation; twelve paired break-detect-recover mutation tests; seven teaching and verification notebooks with generated plots and optional widgets; two publication figures; a Lean 4 library with a current theorem-level axiom report; typed claim maps; metadata; and deterministic checksum and archive scripts. Reproduction. Install the locked development environment, run `python verify_deposit.py --lean`, and build the dated archive with `python scripts/build_deposit_zip.py`. Scope. The checked results are finite identities and finite-data guards. A zero observed defect is not a general reliability guarantee, and the real exponential-kernel theorem remains conditional and is not fully mechanized in Lean