Skip to content

docs: ephapax bridge package (#125 + #127) + EchoTypes.jl v0.2.0 surfacing (#132)#161

Merged
hyperpolymath merged 1 commit into
mainfrom
session/echotypes-jl-+-ephapax
May 30, 2026
Merged

docs: ephapax bridge package (#125 + #127) + EchoTypes.jl v0.2.0 surfacing (#132)#161
hyperpolymath merged 1 commit into
mainfrom
session/echotypes-jl-+-ephapax

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Resolves three tightly-coupled documentation issues with shared inputs from a coordinated background-agent research dump (`/tmp/ephapax-bridge-proposal.md`):

The Agda companion stub (#126) lands in a separate PR.

Key honest-scope discipline preserved throughout

  • R-2026-05-18 narrowings: no "graded comonad" / "model-independence" / "categorical universal property" / "conservativity metatheorem" language re-introduced. Scanned the diff to confirm.
  • EchoTypes.jl scope: retracted surface NOT mirrored; F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) NOT mirrored — Julia has no funext, the claims would be vacuous.
  • ephapax L3 paper-paragraph scope: cites L3 ONLY, not implying anything about ephapax's overall posture (L1 has 5 Axiom + 11 Admitted, L2 has 1 Admitted, L4 is skeleton; only L3 is Qed-closed).
  • Anti-pattern note: empirical downstream test, NOT a proof of the upstream theorem.

Seam-analyst observations consumed in-PR (not scope-creep)

The background agent caught three drift points while assembling the proposal:

  1. `composition.md` is Markdown, not AsciiDoc — issue composition.md: empirical evidence for decoration-violating closure being unsound (ephapax L1→L2 case) #125 asked for AsciiDoc; draft rendered as Markdown to match file (the `.md` / `.adoc` split in `docs/echo-types/` is pre-existing and the policy direction isn't documented; flagging only).
  2. Pillar E / examples.md: ephapax L3 region-exit as canonical example (draft entry + paper paragraph) #127's cited line range `EchoResidue.agda:33-73` covers the residue block; the tight theorem range is 52-65. Tight range used in both examples.md and paper.adoc.
  3. The MEMORY `feedback_ephapax_affine_proofs_not_done.md` entry was respected — paper paragraph scoped to L3 only, not broadened to "ephapax is fully mechanised".

File-by-file

File What changed
`README.md` One-line "Executable companion" callout below synopsis
`CLAUDE.md` New ecosystem-context bullet for EchoTypes.jl
`docs/bridges/cross-repo-bridge-status.md` New "EchoTypes.jl executable mirror" row in Tracks table
`docs/echo-types/MAP.adoc` §Tooling New §"EchoTypes.jl — Executable Julia companion `[REAL]`"
`docs/echo-types/composition.md` New "Anti-pattern — closing a degrade-map obligation within an endpoint" subsection
`docs/echo-types/examples.md` New entry 11 "Region exit in a linear type system (ephapax L3)"
`docs/echo-types/paper.adoc` New paragraph in §"Sample-size on consumer evidence"

Test plan

  • All edits are docs — Agda suite unaffected.
  • Citation line ranges verified at agent's named theorems.
  • No R-2026-05-18 retraction-watch violations introduced.

Closes

🤖 Generated with Claude Code

…acing (#132)

Resolves three tightly-coupled open documentation issues with shared
inputs from a coordinated proposal at /tmp/ephapax-bridge-proposal.md
(a background-agent research dump consumed verbatim where citation-
quality matched, lightly edited for context).

=============================================

* README.md — one-line "Executable companion" callout below the
  synopsis, pointing at hyperpolymath/EchoTypes.jl with explicit
  R-2026-05-18 honest-scope clause (retracted surface NOT mirrored;
  F5 funext-qualified clauses NOT mirrored — Julia has no funext).
* CLAUDE.md ecosystem-context block — new bullet matching the
  existing one-line style of Ephapax / VeriSim entries; same scope
  caveats.
* docs/bridges/cross-repo-bridge-status.md — new row in the Tracks
  table for the executable-mirror correspondence. Row uses the
  existing 5-column shape; "Current status" cell carries the
  scope-inheritance discipline so the row stays falsifiable by an
  outside reviewer.
* docs/echo-types/MAP.adoc §Tooling — new §"EchoTypes.jl — Executable
  Julia companion `[REAL]`" subsection adjacent to the ArghDA
  subsection. Records repo URL + registry + v0.2.0 module list +
  honest-scope clause + bridge-status pointer.

The companion makes no proof claims and the Agda here remains the
sole source of truth; these edits exist so contributors and reviewers
can discover the companion without already knowing it's there.

==========================================

Adds a new "Anti-pattern — closing a degrade-map obligation within an
endpoint" subsection at the end of docs/echo-types/composition.md.
Captures the lesson surfaced by the 2026-05-27 ephapax four-layer
redesign work: when a decoration `D₁ ≤ D₂` connects two indexed
instances of a fiber, an obligation that mentions BOTH endpoints
does not close inside either endpoint alone — the load-bearing
content lives on the degrade arrow.

The note pairs the upstream Agda theorem (`EchoLinear.degradeMode-comp`
at `proofs/agda/EchoLinear.agda:93-101`, three `refl` clauses) with
an empirical downstream test from ephapax (PR #170 strengthened the
L1 variable rule with a region-well-formedness premise; the resulting
axiom remained false on a concrete typing-level counterexample; the
honest closure path identified in PRESERVATION-DESIGN.md §4.8.1 is
cross-layer at the L1→L2 boundary).

The downstream test is empirical evidence that the discipline
detects ill-shaped attempts at the point the abstraction predicts —
NOT a proof of the upstream theorem. Composition.md is Markdown, so
the note is rendered as Markdown rather than the AsciiDoc requested
in the issue body (composition.md / examples.md / overview.md /
taxonomy.md / tropical-correspondence.md / types-list-note.md are
all .md while the other dozen docs are .adoc; the split is
pre-existing and the policy direction isn't documented — flagging
as a seam observation only, not migrating the file extension here).

==========================================

Two edits:

* docs/echo-types/examples.md — new entry 11 "Region exit in a
  linear type system (ephapax L3)" inserted after entry 10
  (Abstract interpretation widening) and before §"Cross-cutting
  observations". Matches the existing 6-bullet template (Source
  map / What is lost / What remains / Echo / Extensional-
  intensional / Reference). The Reference bullet cites both
  echo-types-side `tutorial/region_exit_audit/RegionExitAudit.agda`
  (the type-level audit walkthrough) AND ephapax-side `formal/Echo.v`
  with tight line ranges (291-301 for affine_canonical /
  affine_all_equal; 502-517 for no_section_collapse_to_residue).
* docs/echo-types/paper.adoc §"Threats to validity" §"Sample-size
  on consumer evidence" — new paragraph after the existing two
  (absolute-zero and Buchholz), before §"Conservativity is
  evidence, not a theorem". Adds the ephapax L3 layer as the
  third partial external-corroboration stream, tone matched to
  the existing "validates one technical bridge, not the modality
  thesis" framing. R-2026-05-18 narrowings preserved (no
  graded-comonad / two-models / UP / model-independence language).
  Honestly scoped to L3 ONLY — not implying anything about
  ephapax's overall proof posture (L1 has 5 Axiom + 11 Admitted,
  L2 has 1 Admitted, L4 is skeleton; only L3 is Qed-closed and
  safe to cite).

Background-agent seam observations folded in
=============================================

Three observations the agent caught while assembling the proposal
were applied in-PR (none scope-creep):

1. composition.md is Markdown not AsciiDoc — draft rendered as
   Markdown to match file. Noted in commit body.
2. #127's cited line range 33-73 covers the block; the tight
   theorem range is 52-65. Tight range used in both examples.md
   and paper.adoc.
3. MEMORY.md entry `feedback_ephapax_affine_proofs_not_done.md`
   warns that ephapax's overall proof posture is mixed; §3.2 paper
   paragraph is scoped to L3 specifically.

Test plan
=========

* All edits are pure docs — Agda suite unaffected.
* References to other-repo line numbers verified at the agent's
  cited points before paste.
* No retraction-watch violations: scanned the diff for
  "graded comonad", "model-independence", "categorical universal
  property", "conservativity metatheorem" — none introduced.

Refs
====

* Closes #125
* Closes #127
* Closes #132
* Refs #128 (umbrella will close when #126 also lands)
* Refs #126 (handled in a separate Agda PR — NARROW stub per
  agent's verdict)

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 3a38c6c into main May 30, 2026
12 of 13 checks passed
@hyperpolymath hyperpolymath deleted the session/echotypes-jl-+-ephapax branch May 30, 2026 13:16
hyperpolymath added a commit that referenced this pull request May 30, 2026
## Summary

**Closes #126** with the NARROW recommendation from the bg-agent
proposal at `/tmp/ephapax-bridge-proposal.md` §4:

- **Companion** to #161 (which closes #125 + #127 + #132).
- **Sets up** #128 umbrella close: once this and #161 merge, every
  child issue (#125 / #126 / #127 / #132) is discharged.

Ships a thin import-time documentation module that catalogues the
ephapax↔echo-types L3 correspondence without re-mechanising it. Two
definitional `refl`-renames pin the load-bearing Agda symbols under
`ephapax-L3-` prefixed names so `MAP.adoc`'s "Directions" navigation
has an ephapax row and a silent upstream rename trips `Smoke.agda`.

The cross-repo content correspondence is already discharged by
`coqc` on the ephapax side (`formal/Echo.v`, 584 lines, 24 `Qed`,
zero `Admitted` / zero `Axiom` — explicit Coq port of
`EchoLinear.agda` + `EchoResidue.agda` under a K-free / zero-axiom
discipline equivalent to `--safe --without-K`). **No Lane 4 CI
dependency.**

## Files

| File | Change |
|---|---|
| `proofs/agda/EchoEphapaxBridge.agda` | **NEW** ~45 lines. Module
docstring catalogues 5 Coq headlines (`mode_le_prop`,
`weaken_collapses_distinction`, `affine_canonical`, `degrade_mode_comp`,
`no_section_collapse_to_residue`); two definitional `refl`-renames
`ephapax-L3-weaken = weaken` + `ephapax-L3-no-section-collapse =
no-section-collapse-to-residue`. |
| `proofs/agda/All.agda` | One line: wires `EchoEphapaxBridge` between
`EchoJanusBridge` and `Dyadic`. |
| `proofs/agda/Smoke.agda` | Pins `ephapax-L3-weaken` +
`ephapax-L3-no-section-collapse` so silent upstream renames in
`EchoLinear` / `EchoResidue` trip CI fast. Comment block flags ephapax
cross-repo nature. |
| `docs/echo-types/MAP.adoc` | New `=== Ephapax L3 — linear/affine
modality bridge \`[REAL]\`` subsection in §Directions between JanusKey
and Tropical/Dyadic. Scope explicit: **L3 only** — ephapax-affine and
L1/L2/L4 are NOT mechanised to the same standard. |

## Why NARROW (not YES or NO)

Per the bg-agent verdict:

- **YES (full content bridge)** would require ephapax to add an Agda
  dependency it doesn't currently have (ephapax's stack is Coq +
  Idris2 + Rust). Definitional redundancy: by construction the
  bridge collapses to `Echo f y := Σ A (f x ≡ y), QED`.
- **NO (decline)** is right about content but wrong about
  navigability. `EchoCNOBridge.agda` + `EchoJanusBridge.agda` both
  exist for navigability reasons independent of content depth.
  Declining would mean `MAP.adoc` has no ephapax row, despite
  ephapax being more tightly mechanised than several already-bridged
  targets.
- **NARROW** captures the trade-off: ship a thin pointer without
  re-mechanising. Maintenance cost is near-zero (renames are `refl`;
  upstream renames break `Smoke.agda` and surface immediately). The
  stub does not foreclose a future full content bridge.

## Local verification

- `agda -i proofs/agda proofs/agda/EchoEphapaxBridge.agda` — clean.
- `agda -i proofs/agda proofs/agda/Smoke.agda` — clean, exit 0.
- `agda -i proofs/agda proofs/agda/All.agda` — clean, exit 0.
- `bash tools/check-guardrails.sh proofs/agda` — 160 modules pass
  (`--safe --without-K`, no escape pragmas, no postulates, with the
  two existing exploratory exemptions).

## Honest-scope discipline

The module docstring + MAP.adoc subsection both scope the
corroboration claim **to L3 only** per the MEMORY hook
`feedback_ephapax_affine_proofs_not_done.md` and the R-2026-05-18
retraction surface. Ephapax-affine has Rust checkers only; L1 has 5
`Axiom` + 11 `Admitted`; L4 has no mechanised theorems yet. L3 is
the single layer where the upstream-Agda correspondence is both
literal (file mirrors files) and fully discharged.

## Test plan

- [x] New file typechecks under `--safe --without-K` locally.
- [x] `Smoke.agda` typechecks with new pins, exit 0.
- [x] `All.agda` typechecks with new module wired in, exit 0.
- [x] Foundation guardrail passes (160 modules, no new exemptions).
- [ ] CI: Agda + cold-check + characteristic + examples lanes all
  green on this branch.
- [ ] Auto-merge on green.

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

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath added a commit that referenced this pull request May 30, 2026
…) (#163)

## 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

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

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

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

1 participant