docs(explorations): scaffold the decoration bridge as R5 (exploratory)

[hyperpolymath]

Summary

Bounded exploratory scaffold for a "decoration bridge" — a place to ask
whether the one Choreo × Graded axis pair that EchoIntegration
integrates resembles the shape adjacent-domain constructions exhibit
when they compose two decorations on a shared state evolution (CRDT
merges, gossip partial views, local-first causal histories). Strictly
scoped to that one axis pair; candidate analogies carry falsifiers,
never evidence the recipe generalises. Lands as R5 under the deferred-
research track with explicit termination criteria, not as a new Lane.

What's in this PR

4 new files (the originally-scoped scaffold):

• proofs/agda/EchoDecorationBridge.agda — DecorationFit record +
  decoration-claim one-line wrapper of
  EchoIntegration.knowledge-and-controlled-degradation. Prose
  header documents the imports allowlist, the signature-change
  policy (retire, never patch), the reverse-import prohibition,
  retraction-watch, and the forbidden-rebrandings discipline. Not
  in proofs/agda/All.agda.
• docs/echo-types/explorations/decoration-bridge/README.adoc —
  status banner, scope discipline, what-this-is-NOT, Track A/B/C
  clearance argument, three candidate analogies with falsifiers,
  open questions QB-1…QB-4, item-by-item forbidden-rebrandings
  check against both registers in
  .machine_readable/6a2/STATE.a2ml, R-2026-05-18
  retraction-watch with three drift conditions, six-clause
  termination criteria including automatic closure on register
  addition and a cleanup invariant.
• docs/echo-types/explorations/decoration-bridge/01-decoration-instances.adoc
  — per-candidate pseudo-Agda sketches sharing the DecorationFit
  shape.
• docs/echo-types/explorations/decoration-bridge/02-non-commuting-residue.adoc
  — conceptual core: under --safe --without-K, the residue can only
  live in the witness x, not in y and not in the equality leg.

2 modified files (both with explicit justification):

• roadmap.adoc (+60 lines) — R5 entry with a schema-divergence
  note flagging the additional *Termination* bullet as
  intentional (R1–R4 do not carry it); one-liner Lane 4
  cross-reference for navigability. Pillar A–E entries and Lane
  1–4 status lines untouched.
• docs/echo-types/echo-kernel-note.adoc (+11 lines) —
  CI-mandatory single-row addition under a new "Exploratory
  (not in All.agda)" classification, satisfying
  scripts/kernel-guard.sh Check B's requirement that every
  proofs/agda/Echo*.agda be named in the note. Mirrors the
  existing "Sibling (not kernel-derived)" precedent for
  non-derived rows; does not reshape the taxonomy.

What's explicitly NOT in this PR

• No changes to EchoIntegration.agda, EchoChoreo.agda,
  EchoGraded.agda, EchoCNOBridge.agda, EchoJanusBridge.agda,
  DyadicEchoBridge.agda, or All.agda (verified by empty
  git diff against each).
• No new external dependencies (echo-types.agda-lib and
  flake.nix unchanged).
• No postulates / believe_me / escape pragmas in the new module
  (verified by grep returning 0).
• No edits to either bridge ledger (docs/bridges/cross-repo-bridge-status.md,
  docs/bridge-status.md) — the conceptual bridge has no
  adjacent-side column to fill; reshaping the ledgers to fit was
  rejected per the original scaffolding directive.
• No new identity claim, no Pillar move, no Gate edit, no
  reopening of EI-2 (forbidden-rebrandings preflight done in
  README §"Forbidden-rebrandings check").

Test plan

• scripts/kernel-guard.sh PASS locally — funext-free
  certificate (Check A) and classification-drift lint (Check B)
  both clean.
• git diff against EchoIntegration / EchoChoreo /
  EchoGraded / existing EchoXBridge / All.agda returns
  empty.
• No postulates introduced (verified by grep against the
  new module).
• echo-types.agda-lib and flake.nix unchanged (no new
  external deps).
• CI agda typecheck (deferred — no agda binary in the
  container that produced this PR). The bridge module's signature
  was manually verified against the read-in source signatures of
  knowledge-and-controlled-degradation, client-stability, and
  Knows. If CI reveals a unification gap, the cleanup invariant
  in the README applies — delete the four created files plus the
  two diffs and the repo returns to its pre-scaffolding state with
  zero residue.
• Reviewer sanity-check on the forbidden-rebrandings check
  table (README §"Forbidden-rebrandings check"). Closest-adjacent
  entry is "the recipe is uniformly applicable across all 2D
  axis pairs"; mitigation is scope-strictly-Choreo × Graded +
  per-candidate falsifiers + the auditable cite-by-name table.

Termination clauses (so the cleanup path is explicit)

The exploration terminates and the 6 file additions/edits revert
under any of: (i) Track A/B/C failure; (ii) all three candidates
fail their falsifiers; (iii) the residue analysis reduces to the
retracted-prose graded-comonad framing; (iv) any audit pass adds
the bridge framing to STATE.forbidden-rebrandings; (v)
retraction-watch trips on any of the three R-2026-05-18
narrowings. See roadmap.adoc §R5 and the bridge README §
"Termination criteria" for the canonical list.

https://claude.ai/code/session_013nLEeKZXpvHnrDZMgRm19S

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 56 issues detected

Severity	Count
🔴 Critical	10
🟠 High	27
🟡 Medium	19

⚠️ 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 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/provenance_debugging/ProvenanceDebugging.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "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