Skip to content

docs: enumerate exploratory truncation postulates in docs/proof-debt.md#172

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/proof-debt
May 30, 2026
Merged

docs: enumerate exploratory truncation postulates in docs/proof-debt.md#172
hyperpolymath merged 1 commit into
mainfrom
docs/proof-debt

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Summary

  • Adds docs/proof-debt.md enumerating the repo's sole soundness-relevant escape hatch under Disposition (c) NECESSARY AXIOM
  • Closes the recurring governance / Trusted-base reduction policy red check estate-wide (consistently failing on echo-types main + every PR since policy adoption)
  • No code changes, no new postulates, no .trusted-base-ignore additions

Background

Standards #211 estate-wide gate (governance / Trusted-base reduction policy) requires every soundness-relevant escape hatch in a proof-bearing repo to be either:

  • (a) discharged (proof landed → entry removed),
  • (b) budgeted (TRUSTED: inline + entry in docs/proof-debt.md §(b)),
  • (c) necessary axiom (AXIOM: inline + entry in §(c)),
  • (d) debt (deadline + owner in §(d)).

echo-types has exactly one such hatch: the four propositional-truncation postulates in EchoImageFactorizationPropPostulated.agda. They are already:

  • explicitly scoped exploratory by the file preamble,
  • allowed by hypatia: allow code_safety/agda_postulate,
  • exempted in tools/check-guardrails.sh,
  • classified Tier-2 in docs/echo-types/echo-kernel-note.adoc.

This PR just adds the canonical enumeration so the gate goes green for all future PRs.

Verification

$ bash /tmp/check-trusted-base.sh .
[INFO] Found 1 soundness-relevant escape hatch(es).
[OK] proof-debt document(s) found: docs/proof-debt.md
[OK] All 1 escape hatch(es) are documented.

Test plan

  • bash check-trusted-base.sh passes locally
  • governance / Trusted-base reduction policy green on this PR
  • Auto-merge SQUASH armed

🤖 Generated with Claude Code

…ulates

Closes the recurring `governance / Trusted-base reduction policy`
red check (consistently failing on echo-types since the policy was
adopted estate-wide) without any code change. The repo's sole
soundness-relevant escape hatch is the top-level `postulate` block
in `proofs/agda/EchoImageFactorizationPropPostulated.agda` (four
propositional-truncation primitives), already explicitly scoped as
exploratory by:

- the file's own preamble + `hypatia: allow code_safety/agda_postulate`,
- `tools/check-guardrails.sh` allow-list (line ~exempt),
- `docs/echo-types/echo-kernel-note.adoc` Tier-2 classification.

This commit just satisfies the Trusted-Base Reduction Policy's
documentation requirement by enumerating that single escape hatch
under Disposition (c) NECESSARY AXIOM with the standard
justification + citations. No new postulates, no code changes,
no `.trusted-base-ignore` additions.

Verified locally via `bash check-trusted-base.sh .`:
    [OK] All 1 escape hatch(es) are documented.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath enabled auto-merge (squash) May 30, 2026 15:21
@hyperpolymath hyperpolymath merged commit 360ca7c into main May 30, 2026
5 of 12 checks passed
@hyperpolymath hyperpolymath deleted the docs/proof-debt branch May 30, 2026 15:29
@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 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>
hyperpolymath pushed a commit that referenced this pull request Jun 12, 2026
…2026-06-12

Faithful translation of STATE/META/ECOSYSTEM/AGENTIC/NEUROSYM/PLAYBOOK
from the Guile S-expression bodies to the estate TOML-A2ML convention
(provenance headers retained; EI-2 record, ADRs, certificates, gate
rules and procedures preserved in full; tomllib-verified).

STATE refreshed from git log since 2026-04-29 + CHANGELOG: adds
[recent-work] (PRs #160-#172, #177-#180, #185 estate adoption),
[blockers] (ordinal Gate 1 CHECKED-REFUTED routes, unreleased v0.1.1,
Pillar E author-gated, #185 LICENSE review), honest status/phase.
Stale .scm-era path citations updated to .machine_readable/6a2/*.a2ml;
contradicted ECOSYSTEM entries (root Justfile exists, MPL-2.0/CC-BY-4.0
split, k9 set now present) corrected.
hyperpolymath pushed a commit that referenced this pull request Jun 12, 2026
…, bot_directives trio, self-validating k9 set

Inventory of PR #185's estate supply found three gaps; this fills them:

- contractiles/Dustfile.a2ml: TOML-A2ML, ports the full content of the
  pre-estate root contractiles/Dustfile.a2ml (deleted by #185) into the
  flat layout; cleanup/hygiene/reversibility sections populated from
  repo reality (not-applicable keys carry explicit reasons).
- contractiles/Bustfile.a2ml: no bust reference exists anywhere in the
  estate; written fully from repo-true gates (All/Smoke suite,
  kernel-guard, guardrails, append-only history, proof-debt exceptions).
- bot_directives/{README.adoc,hypatia.a2ml,gitbot-fleet.a2ml,
  git-private-farm.a2ml}: net-new trio per the estate standard;
  accepted-findings mirror .hypatia-ignore rationales + PR #156/#172
  adjudications; propagation disabled (no instant-sync.yml).
- self-validating/: shared k9 template set copied from the
  nextgen-typing reference (maa-framework precedent), adapted only in
  repo-identity fields; examples point at the real build commands.

All new .a2ml files tomllib-verified. nickel binary unavailable;
k9 .ncl files syntax-checked by eye against the reference set.
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