Skip to content

docs: ResidueForm count 6→8 + Slice 3 closure (#142 + #143)#145

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/residue-instance-count-correction
May 28, 2026
Merged

docs: ResidueForm count 6→8 + Slice 3 closure (#142 + #143)#145
hyperpolymath merged 1 commit into
mainfrom
docs/residue-instance-count-correction

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

Summary

Two corrections to PR #144's narrative refresh.

ResidueForm instance count: 6 → 8

PR #144 stated the post-#139 ResidueForm count as six. The actual count is eight. The pre-#139 baseline was already six (not four): the 2026-05-27 audit-follow-on landed `indexed-residue` + `cost-residue` (lines 181–234 of EchoResidueTaxonomy.agda). PR #139 then added `search-residue` + `epistemic-residue`, for a total of 8.

Slice 3 closure: PRs #142 + #143

PR #144 framed the Slice 3 umbrella case-split as remaining work and the `bpsi=bpsi at equal markers` sub-case as still needing α's rank via rank-adm / rank-lex. Both landed in PRs #142 + #143:

CHANGELOG + EXPLAINME updated to acknowledge both.

Files

Verification

`scripts/kernel-guard.sh` PASS. No Agda code changed.

Test plan

  • kernel-guard.sh PASS
  • Admin-merge if budget permits

Refs: echo-types#142, echo-types#143, echo-types#144.

🤖 Generated with Claude Code

… update

Two corrections to PR #144's narrative refresh.

## ResidueForm instance count: 6 → 8

PR #144 stated the post-#139 ResidueForm count as six. The actual
count is eight. The pre-#139 baseline was already six, not four:
the 2026-05-27 audit-follow-on added `indexed-residue` +
`cost-residue` (lines 181-234 of EchoResidueTaxonomy.agda) on top
of the original endpoint pair + generic Σ-cert + linear-affine.
PR #139 then added `search-residue` + `epistemic-residue`, taking
the total to eight.

Files updated:
- CHANGELOG.md — PR #139 entry rephrased: six → eight, with the
  pre-#139 six explicitly attributed to the 2026-05-27 audit
  follow-on.
- docs/echo-types/MAP.adoc — eight instances enumerated, grouped
  by landing date.
- README.md — Tier 2 mermaid label updated to "8 instances incl.
  Indexed, Cost, Search, Epistemic".
- readme.adoc — Tier 2 list line updated to 8 with the same
  enumeration.

## Slice 3 closure: PRs #142 + #143

PR #144 said the Slice 3 umbrella case-split was the remaining
wiring and the `bpsi=bpsi at equal markers` sub-case still needed
`α`'s rank via rank-adm / rank-lex. Both have now landed:

- PR #142 — Slice 3 umbrella extension: `_<ᵇ¹_` extension with
  joint-bplus constructor + strict-head dispatch wires the Slice
  3 headline (from #141) into the umbrella.
- PR #143 — Slice 3 lex-rank companion: the `bpsi-source-at-
  equality` ψ-rank discharge closes the last remaining sub-case
  via rank-lex (exactly the path #144 named as remaining work).

Files updated:
- CHANGELOG.md — new Slice 3 follow-on bullet covering #142 +
  #143; framed as "substantively complete via head-Ω + lex-rank
  composition" rather than hard-claiming full closure (the wider
  paper-critical-path claims live in `roadmap.adoc` not the
  CHANGELOG).
- EXPLAINME.adoc — Slice 3 line revised to acknowledge umbrella +
  lex-rank closures.

## Verification

scripts/kernel-guard.sh PASS — both checks green. No Agda code
changed.

Refs: echo-types#142 (umbrella), echo-types#143 (lex-rank
companion), echo-types#144 (the now-corrected narrative refresh).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 1cc2ebc into main May 28, 2026
3 of 12 checks passed
@hyperpolymath hyperpolymath deleted the docs/residue-instance-count-correction branch May 28, 2026 09:22
@github-actions
Copy link
Copy Markdown

🔍 Hypatia Security Scan

Findings: 74 issues detected

Severity Count
🔴 Critical 17
🟠 High 36
🟡 Medium 21

⚠️ 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": "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/epistemic_erasure/EpistemicErasure.agda",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

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