fix(hypatia): scope-narrow agda_postulate alert on Exploratory module via inline allow (#156)

## Summary

Remedies the lingering GitHub Advanced Security alert

[#101](https://github.com/hyperpolymath/echo-types/security/code-scanning/101)
("Hypatia code_safety: agda_postulate -- Agda postulate assumes without
proof") raised on
`proofs/agda/EchoImageFactorizationPropPostulated.agda` by PRs #153 /
#155.

Adds a single-line `-- hypatia: allow code_safety/agda_postulate --
<reason>`
directive in the first 20 lines of the file. The Hypatia scanner's
`scanner_suppression.ex` recognises this and stops re-raising the alert
at
file scope, with the rationale visible inline next to the postulates.

## Why this, not a fix or a `.hypatia-ignore`

Per Hypatia's own guidance (`hypatia/CLAUDE.md` §"When you need to
suppress a
real finding") the preference is **fix > inline directive >
`.hypatia-ignore`
> baseline**.

**Why not a fix.** Propositional truncation `∥_∥` cannot be CONSTRUCTED
in
`--safe --without-K` without HITs (Cubical Agda) or `--rewriting`. The
repo's
`flake.nix` pins `agda-stdlib v2.3` only — there is no cubical library
in the
toolchain. Discharging the four postulates would mean either adding
Cubical
Agda to the flake + a sibling `--cubical` module realising `Trunc` as a
HIT,
or relaxing the `--safe` profile — both substantial design decisions
explicitly flagged in `CLAUDE.md` §"Plan for the next Claude" item 3
(image-factorisation earn-back) and out of scope for alert-management.

**Why inline over `.hypatia-ignore`.** Inline lives next to the
postulates;
the rationale is self-documenting; no new repo-level allowlist file for
one
entry; scope is exactly this file via the directive matcher's
`max_header_lines = 20` default.

## What the directive justifies

The flagged postulates (`Trunc-pos`, `∣_∣-pos`, `is-prop-pos`,
`rec-pos`) are
the deliberate scoped `TruncInterface` DEMONSTRATION shipped by #153 /
#155:

- The base `EchoImageFactorizationProp` remains `--safe --without-K`
with
  zero postulates — the load-bearing artefact is unaffected.
- This consumer is module-scoped to demonstrate the parametric
  `TruncInterface` slot is plug-in usable, taking the four standard
  (-1)-truncation laws as assumptions.
- Classification: Exploratory per
`docs/echo-types/echo-kernel-note.adoc`;
  outside the kernel cone; outside `proofs/agda/All.agda`.
- Already exempt from the local `tools/check-guardrails.sh` allowlist
  (`EXPLORATORY_EXEMPT`, landed in `ea46e09` / PR #155).

This PR closes the loop with the GitHub-side Hypatia scanner, matching
the
local-side exemption that already shipped.

## Test plan

- [x] `agda -i proofs/agda
proofs/agda/EchoImageFactorizationPropPostulated.agda`
typechecks clean — the directive is an Agda line comment, no AST impact.
Upstream modules (`EchoImageFactorizationProp`, `EchoTotalCompletion`,
`EchoOrthogonalFactorizationSystem`, `EchoFiberBridge`, `Echo`) check
      through unchanged.
- [x] `proofs/agda/All.agda` and `proofs/agda/Smoke.agda` unaffected —
this
      file is already outside both per the Exploratory classification.
- [ ] Post-merge: GitHub Advanced Security alert #101 transitions out of
"open" on the next Hypatia scan against `main`. (Dismissing #101 by
      API as a follow-up step so the change is reflected immediately.)

## Honest scope

This PR does NOT discharge the postulates. The genuine "earn-back" path
(Cubical / HIT-realised `Trunc`) remains the design decision tracked in
`CLAUDE.md`'s "Plan for the next Claude" item 3.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/agda/EchoImageFactorizationPropPostulated.agda

@@ -1,5 +1,7 @@
 {-# 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.
+
 -- Postulated-truncation consumer for `EchoImageFactorizationProp`.
 --
 -- ## Purpose