governance(hypatia): confirm CSA004 agda_postulate dismissal is documented (likely already closeable)

[hyperpolymath]

Hypatia code_scanning_alerts CSA004 (medium, review), surfaced on the #266 scan.

Code-scanning alert hypatia/code_safety/agda_postulate dismissed as 'false positive' at proofs/agda/EchoImageFactorizationPropPostulated.agda — ensure dismissal is documented and justified.

Assessment (verified): appears ALREADY satisfied. The dismissal is documented in three places:

• commit ae7f8fb self-documents the CSA004 agda_postulate dismissal inline in the module;
• docs/proof-debt.md §(c) justifies the four propositional-truncation postulates as the --safe --without-K-profile shadow of the --cubical-constructed ∥_∥ in EchoImageFactorizationPropCubical.agda (which realises them with zero postulates);
• the module carries an inline hypatia: allow pragma and is allow-listed in tools/check-guardrails.sh. It is outside the wired All.agda/Smoke.agda cone, so the --safe kernel depends on it not at all.

Disposition: confirmation only — verify the above satisfies the "documented + justified" bar, then close. Likely immediately closeable.

Source: Hypatia neurosymbolic scan on #266.