Skip to content

docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162)#163

Merged
hyperpolymath merged 1 commit into
mainfrom
session/ephapax-adjacency-cleanup
May 30, 2026
Merged

docs: ephapax bridge adjacency cleanup (3-file follow-up to #161 + #162)#163
hyperpolymath merged 1 commit into
mainfrom
session/ephapax-adjacency-cleanup

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Seam-analyst follow-up to the ephapax bridge package (#161 + #162). Three doc surfaces enumerate the bridges and were missing Ephapax-L3:

File Change
docs/bridges/EchoBridges.md New §5 "EchoEphapaxBridge `[NARROW]`" — purpose, components, 5-row cross-repo theorem correspondence table, scope discipline (L3 ONLY), main entry. Overview line now includes "Ephapax-L3".
docs/bridges/cross-repo-bridge-status.md New 6th Tracks row "Ephapax L3 bridge (Agda↔Coq)" after the EchoTypes.jl row landed in #161. References the two `refl`-renames, the upstream Coq headlines, the L3-only honest scope, and the per-bridge-doc follow-up.
roadmap.adoc §Lane 4 module-list appended with `EchoEphapaxBridge.agda`; added a sentence noting it's NARROW (no Lane 4 CI dependency).

Why

Per the seam-analyst sweep (background agent verdict captured in the umbrella #128 closure comment): the bridge package shipped the core Ephapax surfacing (#161 Agda stub + #162 doc paragraphs) but didn't update three documents that enumerate bridges across the repo. A reader navigating via `EchoBridges.md` overview, the bridges-status Tracks table, or the roadmap Lane 4 module list would not have found Ephapax-L3 catalogued.

Honest-scope discipline (preserved across all three surfaces)

The corroboration claim is scoped to L3 only:

  • Ephapax-affine has Rust checkers only — NOT mirrored as proof-bearing.
  • L1 has 5 `Axiom` + 11 `Admitted` in `Semantics_L1.v`.
  • L2 has 1 `Admitted` in `TypingL2.v` (post-hybrid `weaken_modality` is `Qed`).
  • L4 has no mechanised theorems yet (5 `Qed`-style obligations only).
  • L3 (`formal/Echo.v`, 584 lines, 24 `Qed`, zero `Admitted` / zero `Axiom`) is the single layer where the upstream-Agda correspondence is both literal and fully discharged.

Cf. MEMORY hooks `feedback_ephapax_affine_proofs_not_done.md` + `feedback_ephapax_no_patching_legacy_preservation.md`.

Pre-existing tech-debt NOT touched

`EchoBridges.md` §1 (EchoJanusBridge) still describes the OLD 4-variant `JanusOp` enum (Create/Delete/Modify/Move); the canonical surface in `EchoJanusBridge.agda` is now 8-variant `OpKind` (Copy/Move/Delete/Modify/Obliterate/KeyGen/KeyRotate/KeyRevoke). This drift is already tracked in `cross-repo-bridge-status.md` §JanusKey row + §"Immediate next actions" — out of scope here.

Follow-up filed

Per-bridge documentation `docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` (analogous to the existing 461-line `ECHO-CNO-BRIDGE.adoc`) is filed as a separate issue, not blocking this PR.

Test plan

  • No code changes — docs-only diff.
  • No `Echo*.agda` modules added — kernel-guard not affected.
  • Foundation guardrail not affected.
  • CI: governance + Agda lanes pass on this branch.
  • Auto-merge on green.

🤖 Generated with Claude Code

Seam-analyst sweep after the ephapax bridge package landed (#161
+ #162). Three doc surfaces enumerate the bridges and need to
include Ephapax-L3:

* `docs/bridges/EchoBridges.md` — adds §5 EchoEphapaxBridge to the
  per-bridge enumeration with the `[NARROW]` tag, cross-repo theorem
  correspondence table (5 rows: mode order / weaken-collapses /
  affine-canonical / degrade-mode-comp / no-section-collapse), honest
  scope (L3 ONLY), and the main entry. Overview line updated to
  include "Ephapax-L3".
* `docs/bridges/cross-repo-bridge-status.md` Tracks table — adds a
  6th row "Ephapax L3 bridge (Agda↔Coq)" after the EchoTypes.jl row
  landed in #161. References Coq side (`ephapax/formal/Echo.v`, 584
  lines, 24 Qed, zero Admitted), the two `refl`-renames, the
  upstream Coq headlines, and the per-bridge-doc follow-up.
* `roadmap.adoc` §Lane 4 — appends `EchoEphapaxBridge.agda` to the
  in-tree bridges list and adds a sentence noting it's NARROW
  (no Lane 4 CI dependency).

Honest-scope discipline preserved across all three: ephapax-affine /
L1 / L2 / L4 NOT mechanised to the same standard as L3; cf. MEMORY
hooks `feedback_ephapax_affine_proofs_not_done.md`,
`feedback_ephapax_no_patching_legacy_preservation.md`.

Filed concurrently as follow-up issue: author
`docs/bridges/ECHO-EPHAPAX-BRIDGE.adoc` per-bridge doc (analogous
to the existing 461-line `ECHO-CNO-BRIDGE.adoc`).

Pre-existing tech-debt unrelated to this PR (NOT touched):
* EchoBridges.md §1 EchoJanusBridge still lists the OLD 4-variant
  `JanusOp` enum; canonical surface in `EchoJanusBridge.agda` is now
  8-variant `OpKind`. Drift documented in bridges-status §JanusKey
  row; doc refresh is the same "JanusKey" entry in §"Immediate next
  actions".

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 58 issues detected

Severity Count
🔴 Critical 17
🟠 High 22
🟡 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 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": "Action rpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "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 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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

@hyperpolymath hyperpolymath merged commit 1605fb2 into main May 30, 2026
12 of 13 checks passed
@hyperpolymath hyperpolymath deleted the session/ephapax-adjacency-cleanup branch May 30, 2026 13:34
hyperpolymath added a commit that referenced this pull request May 30, 2026
…oof-debt (#173)

## Summary

- Adds `### Added (2026-05-30)` + `### Fixed (2026-05-30)` sections to
`CHANGELOG.md` under `[Unreleased]`
- Documents three cohorts that landed today: the Slice 3+4 Route A 6-PR
arc + #171 doc sweep + #172 proof-debt; the cross-repo ephapax L3 bridge
package (#161, #162, #163); the meta cohort (#156, #157, #158, #160)
- Format matches 2026-05-28's depth

## Why

The `CHANGELOG.md` hadn't been updated since 2026-05-28 — today's 15+
merged PRs were undocumented. Drift-correction.

## Test plan

- [x] No code changes; only `CHANGELOG.md` edited
- [x] Format follows the existing Keep-a-Changelog convention
- [x] GPG-signed

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

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant