Skip to content

docs(readme): disclose class-J axiom + 13/13 build posture (Refs stan…#47

Merged
hyperpolymath merged 1 commit into
mainfrom
docs/proof-disclosure-readme
May 20, 2026
Merged

docs(readme): disclose class-J axiom + 13/13 build posture (Refs stan…#47
hyperpolymath merged 1 commit into
mainfrom
docs/proof-disclosure-readme

Conversation

@hyperpolymath
Copy link
Copy Markdown
Owner

…dards#131)

Adds a == Formal verification section to the README mirroring boj-server's (PR #108, 2026-05-20). Necessary update post-#41 because the README's previous claim of "machine-checked in Idris2" needed nuance now that one believe_me-bodied class-J axiom (stringNotEqCommut) exists in PanelIsolation.

The new section names:

Symmetric with boj-server's README.adoc:109-129 § Formal verification which documents that repo's 5 class-(J) axioms. Estate-wide pattern: honest disclosure at the README level, full audit in PROOF-NEEDS, machine-readable state in STATE.a2ml.

Refs hyperpolymath/standards#131
Refs hyperpolymath/standards#124

Summary

Changes

RSR Quality Checklist

Required

  • Tests pass (just test or equivalent)
  • Code is formatted (just fmt or equivalent)
  • Linter is clean (no new warnings or errors)
  • No banned language patterns (no TypeScript, no npm/bun, no Go/Python)
  • No unsafe blocks without // SAFETY: comments
  • No banned functions (believe_me, unsafeCoerce, Obj.magic, Admitted, sorry)
  • SPDX license headers present on all new/modified source files
  • No secrets, credentials, or .env files included

As Applicable

  • .machine_readable/STATE.a2ml updated (if project state changed)
  • .machine_readable/ECOSYSTEM.a2ml updated (if integrations changed)
  • .machine_readable/META.a2ml updated (if architectural decisions changed)
  • Documentation updated for user-facing changes
  • TOPOLOGY.md updated (if architecture changed)
  • CHANGELOG or release notes updated
  • New dependencies reviewed for license compatibility (PMPL-1.0-or-later / MPL-2.0)
  • ABI/FFI changes validated (src/interface/abi/ and src/interface/ffi/ consistent)

Testing

Screenshots

…dards#131)

Adds a `== Formal verification` section to the README mirroring
boj-server's (PR #108, 2026-05-20). Necessary update post-#41 because
the README's previous claim of "machine-checked in Idris2" needed
nuance now that one believe_me-bodied class-J axiom
(`stringNotEqCommut`) exists in PanelIsolation.

The new section names:
  * 13/13 ABI modules build green (was a mix of wired-and-tested vs
    wired-but-never-built before the standards#131 campaign discharged
    all four originally-deferred modules).
  * One believe_me invocation, isolated, classified, soundness-oracle
    explicit.
  * Forward link to PROOF-NEEDS.md "Class-J axioms (trusted base)"
    section (added in PR #41) for full per-site rationale.

Symmetric with boj-server's README.adoc:109-129 § Formal verification
which documents that repo's 5 class-(J) axioms. Estate-wide pattern:
honest disclosure at the README level, full audit in PROOF-NEEDS,
machine-readable state in STATE.a2ml.

Refs hyperpolymath/standards#131
Refs hyperpolymath/standards#124

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@hyperpolymath hyperpolymath merged commit 6aee10b into main May 20, 2026
30 of 47 checks passed
@hyperpolymath hyperpolymath deleted the docs/proof-disclosure-readme branch May 20, 2026 22:01
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