docs(proof-debt): self-document the CSA004 postulate discharge in the flagged module

EchoImageFactorizationPropPostulated.agda is the `--without-K`-only module
carrying the four propositional-truncation postulates (the `agda_postulate`
code-scanning finding CSA004, dismissed as a false positive). Its header
justification was stale: it said the cubical/HIT realisation is "cited
rather than mechanised", but as of 2026-06-15 the repo DOES mechanise it.

This makes the dismissal self-documenting from the flagged file:

- The `hypatia: allow` pragma now records that the four postulates are
  DISCHARGED FOR REAL (zero postulates) in the CI-verified `--cubical
  --safe` lane by EchoImageFactorizationPropCubical.agda (run in
  .github/workflows/agda.yml "Typecheck cubical lane"), per
  docs/proof-debt.md §(a) — they are the `--safe --without-K` shadow of a
  now-constructed HIT, not an irreducible axiom.
- The "deliberately DOES NOT prove" bullet is corrected accordingly.

Comment-only change. Verified with the actual toolchain (Agda 2.6.3 +
stdlib v2.3 + absolute-zero):
- EchoImageFactorizationProp.agda          (--safe --without-K)  exit 0
- EchoImageFactorizationPropPostulated.agda (--without-K)         exit 0
- EchoImageFactorizationPropCubical.agda    (--cubical --safe)    exit 0
- kernel-guard.sh PASS

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku

Author: claude

proofs/agda/EchoImageFactorizationPropPostulated.agda

@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K #-}
 
--- hypatia: allow code_safety/agda_postulate -- ∥_∥ cannot be constructed in --safe --without-K without HITs / Cubical; the four postulates below are the scoped, documented TruncInterface demonstration. Exploratory per docs/echo-types/echo-kernel-note.adoc; guardrail-exempted in tools/check-guardrails.sh; base EchoImageFactorizationProp remains --safe --without-K with zero postulates.
+-- hypatia: allow code_safety/agda_postulate -- ∥_∥ cannot be constructed in --safe --without-K without HITs / Cubical; the four postulates below are the scoped, documented TruncInterface demonstration. Exploratory per docs/echo-types/echo-kernel-note.adoc; guardrail-exempted in tools/check-guardrails.sh; base EchoImageFactorizationProp remains --safe --without-K with zero postulates. DISCHARGED FOR REAL (zero postulates) in the CI-verified --cubical --safe lane by EchoImageFactorizationPropCubical.agda (run in .github/workflows/agda.yml step "Typecheck cubical lane (epi/mono truncation discharge)"); see docs/proof-debt.md §(a). These four postulates are therefore the --safe --without-K shadow of a now-CONSTRUCTED higher inductive type, not an irreducible axiom.
 
 -- Postulated-truncation consumer for `EchoImageFactorizationProp`.
 --
@@ -62,9 +62,15 @@
 --     the parametric proofs in `ImageProp` need.
 --   * Anything about the postulates' consistency.  The standard
 --     HoTT discipline says the four laws together characterise
---     `Trunc A` up to equivalence (and Cubical Agda or a hand-
---     rolled HIT realises them concretely); we cite that
---     literature rather than mechanise it.
+--     `Trunc A` up to equivalence.  As of 2026-06-15 that
+--     characterisation is no longer merely cited: it is MECHANISED
+--     in-repo by `EchoImageFactorizationPropCubical.agda`, which
+--     CONSTRUCTS `∥_∥` as a genuine higher inductive type under
+--     `--cubical --safe` and re-proves the four obligations as
+--     theorems (zero postulates, CI-verified — see
+--     docs/proof-debt.md §(a)).  The postulates here remain only
+--     because `∥_∥` cannot be built WITHIN `--safe --without-K`
+--     itself, not because the construction is unavailable.
 --
 -- The mechanical contribution: pin that the parameterised
 -- `EchoImageFactorizationProp.ImageProp` module can be CONSUMED