theory: Axis 8 graded access modality — thin slice (Access, ≤a, ≤a-trans, ≤a-prop)

[hyperpolymath]

Summary

Lands the thin-slice obligations 1–6 of the Axis 8 graded access modality (decision: refinement 2 of taxonomy.md §8 / the Axis 8 design study). Mirrors EchoGraded / EchoLinear's order-layer recipe verbatim.

New module proofs/agda/EchoAccess.agda ships:

1. Access — 5-grade enum (free / decidable / enum / feasible / infeasible).
2. _≤a_ — Hasse-enumerated access order (15 constructors, one per reachable pair along the chain).
3. ≤a-trans — transitivity by case-split.
4. ≤a-prop — propositionality by case-split + refl. The load-bearing lemma per the design's §6 falsifier — DID close on refl for all 15 cases. The recipe lives.
5. CEcho + EchoAccess — per-grade carrier (free → Echo, decidable → EchoDec, enum / feasible / infeasible → minimal Lift ⊤ placeholders) and the Σ-shape package.
6. access-of, degrade-access — projection + _≤a_-indexed degrade primitive.

Wired into All.agda; headlines pinned in Smoke.agda. No postulates, no escape pragmas, --safe --without-K throughout.

Refs docs/echo-types/roadmap.md Axis 8 entries (line 31 "Theory work" and line 239 roadmap item 6). Does NOT close anything — the follow-up PR below is needed before the lane can be marked landed.

Deferred to follow-up PR

Per the body of EchoAccess.agda and Axis 8 design doc §5 items 5–8:

• degrade-access-comp / -compose / -via-join — per-decoration composition; the factoring-free closer chain of composition.md §6.
• _⊔a_ join + ≤a-⊔a-{left,right,univ} — categorical join.
• Honest carrier for enum / feasible / infeasible (bridge to EchoFiberCount.FiberSize-fin) — the falsifier mode B of the design's §6. The current Lift ⊤ carriers are deliberately minimal so the order layer ships green; promoting them is the design's deferred mitigation.

Agda build

$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda
Checking All (.../proofs/agda/All.agda).
 Checking EchoAccess (.../proofs/agda/EchoAccess.agda).
 Checking Smoke (.../proofs/agda/Smoke.agda).
EXIT=0

$ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda
EXIT=0

Agda 2.8.0, stdlib v2.3.

Test plan

• agda proofs/agda/All.agda exits 0 under --safe --without-K.
• agda proofs/agda/Smoke.agda exits 0 (verifies pinned headlines resolve).
• No postulates introduced (greppable in EchoAccess.agda).
• No escape pragmas (NO_TERMINATION_CHECK, etc.) introduced.
• ≤a-prop closes on case-split + refl for all 15 constructor pairs (the design's load-bearing test).
• CI green on the PR.

🤖 Generated with Claude Code

[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