echo(image-factorization-prop): postulated-truncation consumer + Exploratory classification

[hyperpolymath]

Summary

Demonstrates the parametric TruncInterface slot in EchoImageFactorizationProp is plug-in-usable by exhibiting a concrete instance built from four postulates matching the interface fields.

New module EchoImageFactorizationPropPostulated:

• Flag profile --without-K only (no --safe) — postulate is forbidden under --safe, so this module lives outside the kernel cone.
• Four postulates realising the standard (-1)-truncation laws (cited; not mechanised).
• trunc : TruncInterface ℓ repackaged + module ImagePropPostulated f consumer wrapper.
• prop-factor-right-injective-demo (mono) + prop-factor-left-mere-surjective-demo (epi) — confirm parametric content type-checks at the concrete instance.

Classification: Exploratory in docs/echo-types/echo-kernel-note.adoc (alongside EchoDecorationBridge). Deliberately NOT wired into proofs/agda/All.agda.

Honest scope

POSTULATED-INTERFACE demonstration, NOT a HIT construction. The base EchoImageFactorizationProp remains kernel-cone compatible (--safe --without-K, zero postulates) and is the load-bearing artefact. The HIT instantiation under --cubical is the next earn-back step.

Test plan

• agda --library-file=... proofs/agda/EchoImageFactorizationPropPostulated.agda EXIT 0
• scripts/kernel-guard.sh PASS (classification-drift lint sees the new module via Exploratory section)
• Base EchoImageFactorizationProp unchanged; kernel cone unchanged
• Not wired into All.agda (per Exploratory precedent)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 75 issues detected

Severity	Count
🔴 Critical	18
🟠 High	36
🟡 Medium	21

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_workflow",
    "file": "codeql.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in agda.yml",
    "type": "unknown",
    "file": "agda.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard.yml",
    "type": "unknown",
    "file": "scorecard.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
    "type": "agda_postulate",
    "file": "/home/runner/work/echo-types/echo-types/tutorial/epistemic_erasure/EpistemicErasure.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[hyperpolymath]

Closing: tools/check-guardrails.sh enforces no-postulates + mandatory --safe repo-wide across proofs/agda/**, with no classification-based exemption. The "Exploratory" classification (used for EchoDecorationBridge) only excuses All.agda membership, not the guardrail itself.

The postulated consumer demo for the (epi, mono) image factorisation can't land here as currently architected. Three follow-on paths if revisited:

1. Relocate to a non-guarded subtree (e.g. tutorial/explorations/postulated-trunc/) — needs the tutorial aggregator's policy clarified first.
2. Implement TruncInterface with a concrete axiom-free model (e.g. Σ A (∀ x y → x ≡ y)-based propositional truncation under decidable equality) — would defeat the purpose (the demo's value is showing what a postulated consumer looks like).
3. Widen the guardrail with an explicit per-file allowlist + rationale tag — overreach for a single demo.

The keystone module EchoImageFactorizationProp (which IS axiom-free and module-parameterised in a TruncInterface) already lands and is wired; nothing on the trusted base changes.