theory: Axis 8 sweep — join + composition trio (Rungs A + B; Rung C deferred)

[hyperpolymath]

Summary

Extends proofs/agda/EchoAccess.agda (the PR #68 thin slice) with the join structure and per-decoration composition trio, completing the same recipe as EchoGraded and EchoLinear at the per-decoration composition rung.

Rung A — categorical join structure. _⊔a_ (componentwise max along free ≤ decidable ≤ enum ≤ feasible ≤ infeasible) + ≤a-⊔a-left + ≤a-⊔a-right + ≤a-⊔a-univ (universal property).

Rung B — per-decoration composition trio.

• degrade-access-comp — two successive degrades along a factoring agree with one degrade along the composed proof. Closes refl on every reachable (p12, p23) constructor pair (the carriers reduce in lock-step with ≤a-trans).
• degrade-access-compose — factoring-free composition; corollary of degrade-access-comp + ≤a-prop.
• degrade-access-via-join — same law restated through the join.

Rung C — honest carriers — deferred with design note. An honest enum-grade carrier needs an enumerator Fin n → A and a decider on B. Neither can be supplied without breaking the parametricity over A that Echo f y enjoys at the free grade. The two clean resolutions are (a) parameterise the whole CEcho family on Decidable B + an enumeration witness (forces every caller to supply them, even at free where they do nothing), or (b) bury both in an existential inside the enum / feasible / infeasible cases (loses the ability to extract from outside). Both are real architectural choices — the PR brief's Stop-condition explicitly flagged this as the design-decision case and instructed landing A + B with a written deferral.

Importantly, the composition layer that lands here is grade-indexed not carrier-indexed, so it is unaffected by the eventual carrier choice. Module preamble carries the full deferral note.

All new headlines pinned in Smoke.agda. Module preamble section list refreshed; degrade-access follow-up commentary updated. No new imports beyond sym from Relation.Binary.PropositionalEquality. No postulates. --safe --without-K preserved throughout.

Build status

BUILD UNVERIFIED LOCALLY — the sandbox repeatedly blocked agda invocations on positional file arguments (the known quirk that hit PRs #71 + #72). Parent session will verify (LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda and same for Smoke.agda, both expected to exit 0) and post a confirmation comment.

The mathematical content is mechanical mirror of EchoGraded.{degrade-comp, degrade-compose, degrade-via-join, ⊔g, ≤g-⊔g-*} (with 5 grades instead of 3) and EchoLinear.{degradeMode-comp, degradeMode-compose, degradeMode-via-join, ⊔m, ≤m-⊔m-*} (with 5 grades instead of 2). Every clause closes refl modulo the ≤a-trans reduction table that already ships in PR #68.

Refs

Refs PR #68 (the thin slice), docs/echo-types/roadmap.md Axis 8 entry, /tmp/echo-types-exploration/axis8.md §5 deferred list.

Test plan

• LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda exits 0.
• LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda exits 0.
• No postulates / no escape pragmas / --safe --without-K preserved.
• All seven new headline names resolve in Smoke.agda.

Generated with Claude Code

[hyperpolymath]

Fix pushed: commit a8ac211 corrects 10 wrong-RHS clauses in ≤a-⊔a-univ, all in the rows where the join reduces to the second summand (c1 < c2 on the chain free < decidable < enum < feasible < infeasible). When c1 ⊔a c2 = c2, the required witness has type c2 ≤a c — but the buggy clauses returned the c1 ≤a c constructor instead.

Audit by (c1, c2) pair with c1 < c2:

• decidable < {enum, feasible, infeasible} — 3 pairs × variable c = 6 buggy clauses
• enum < {feasible, infeasible} — 2 pairs × variable c = 3 buggy clauses
• feasible < {infeasible} — 1 pair × variable c = 1 buggy clause

Total 10, exactly the diff. _⊔a_ itself was reducing correctly; the bug was only on the RHS of the universal-property clauses.

≤a-⊔a-{left, right} and degrade-access-{comp, compose, via-join} re-audited under the same lens — no further bugs found.

Sandbox still blocks agda invocations on positional file arguments — request re-verification.

[hyperpolymath]

Fix verified green from parent session:

$ cd /tmp/echo-types-worktrees/axis8-deferred
$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda; echo "exit: $?"
... (full module check, including Checking EchoAccess and Checking Smoke)
exit: 0

$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda; echo "exit: $?"
exit: 0

The 10-clause RHS fix in ≤a-⊔a-univ (commit a8ac211) closes the strict-inequality witness mismatch. --safe --without-K invariants intact.

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

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 quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence