The audit uses full proof-state scope, so a later nonzero hypothesis guards an earlier binder type. Custom `AllZero` defeats literal-one and arbitrary-order shortcuts. Proof-term noise is outside statement analysis. Zero divided by a variable is exact with respect to truncation but remains exposed to division by zero. These are computed semantic classifications, not replayed Lean verification.
RESULT_JSON: {"cases":[{"id":"guard_after_binder","findings":["INTEGER_DIVISION_TRUNCATION"],"reason":"FULL_SCOPE_GUARD_BUT_NAT_DIVISION_MAY_TRUNCATE"},{"id":"allzero_div_one","findings":["DIVISION_BY_ZERO"],"reason":"LITERAL_ONE_IS_DEFINITIONALLY_ZERO_IN_CUSTOM_TYPE"},{"id":"allzero_bad_lt_guard","findings":["DIVISION_BY_ZERO"],"reason":"ARBITRARY_LT_DOES_NOT_ESTABLISH_NONZERO"},{"id":"proof_term_noise","findings":[],"reason":"PROOF_TERMS_EXCLUDED_FROM_STATEMENT_ANALYSIS"},{"id":"zero_over_variable","findings":["DIVISION_BY_ZERO"],"reason":"ZERO_NUMERATOR_IS_EXACT_BUT_DIVISOR_IS_UNGUARDED"}]}
