math-tools: validate-propositions R1 should recognize the schema-1.4 `retired` field (expected-absent props)

[kiki830621]

Problem

validate-propositions.py's R1 (prop-subset / bijection check) predates the ledger schema 1.4 retired field and reports deliberately-disabled props as failures.

Schema 1.4+ (introduced 2026-07-30 in a downstream manuscript repo) marks props whose source passage was intentionally disabled:

"retired": {"since": "YYYY-MM-DD", "mechanism": "comment_env|line_comment|removed", "match": "exact|by_reading", "reason": "...", "ref": "..."}

R1 visibility is mechanism-dependent by design:

mechanism	source text state	R1 today
comment_env	still verbatim inside \begin{comment}	passes
line_comment	%-disabled (normalizer strips)	fails
removed	deleted outright	fails

Expected

R1 recognizes retired: props with mechanism line_comment/removed are expected-absent — report them in a separate "retired (expected)" bucket, exit non-blocking; a comment_env prop whose text is missing should still fail (its contract is expected-present). Optionally warn when a non-retired failure count is masked.

Actual

Every consumer must carry a hand-maintained "documented budget" (currently 14 in the downstream repo) and mentally subtract it from R1 output on every run; CI gates need workaround arithmetic (see the sibling issue on the audit-chain side).

Impact

R1's red/green signal is meaningless on any repo using retirement; new genuine drift can hide inside the expected count.