docs(architecture): Aeneas translations as a default ECHIDNA learning corpus by hyperpolymath · Pull Request #29 · hyperpolymath/mathesis

hyperpolymath · 2026-11-09T13:55:54Z

Summary

This records the owner's direction of 2026-11-09 in docs/proposals/estate-mathematical-architecture.adoc. It uses the same kind of ruling box as the PWG ruling above it, and leaves the preserved brief unedited.

Default. First-party Rust verified with Creusot/Pearlite and Verus is also translated with Aeneas into a Lean or Rocq model. The security cores come first, and a repo can opt out in its proof-status file.
Purpose. The translations form a corpus for ECHIDNA. Each entry pairs the Rust, its contracts, the Aeneas model and, where one exists, the Agda theorem with its recheck. From these pairs ECHIDNA learns how statements correspond across systems, which builds toward mathematical-object arbitration.
No proof status rises. The correspondence between the model and the Rust stays ASSUMED (PROOF-POLICY §4.1). Aeneas's Rocq backend has a False-deriving axiom, and its Lean backend uses Mathlib, so its output never counts toward a PWG. Evidence stays in the home repos.
Policy gap. PROOF-POLICY §4.1 currently allows Aeneas only where Rust implements an Agda theorem. The box says an amendment is needed in metadatastician/standards, filed together with the ATS2 amendment.
Related direction, design still open. Mathesis becomes the shared, canonical record. Each repo keeps a local copy guarded by its deed, k9 contracts and coordination runners, and any drift or tampering raises an alert.

Testing

asciidoctor --failure-level=WARN renders the file cleanly.

Generated by Claude Code

… corpus Records the owner direction of 2026-11-09 in the same form as the PWG ruling box: first-party Rust verified with Creusot/Pearlite and Verus is also translated with Aeneas by default, as a correspondence corpus for ECHIDNA's mathematical-object arbitration. No proof status rises (the model/Rust correspondence stays ASSUMED, PROOF-POLICY §4.1); backend axioms and Mathlib keep the output out of any PWG count; evidence stays in home repos. Names the PROOF-POLICY §4.1 amendment this needs (to be filed in standards with the ATS2 amendment) and the open design for a shared canonical mathesis record mirrored locally under deed/k9 guard. Verified: asciidoctor --failure-level=WARN renders clean. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk

coderabbitai · 2026-11-09T13:56:03Z

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 25 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

Source mode: Auto
Repository: hyperpolymath/mathesis
Branch: claude/aeneas-echidna-corpus
File: .coderabbit.yaml
Commit: 8d280cb
Layers: Repository YAML
Review profile: CHILL
Plan: Advanced
Run ID: 572b953f-0b5a-4ca6-8fc6-96cb2a7654f8

Commits

Reviewing files that changed from the base of the PR and between a3dbe73 and 8d280cb.

Files selected for processing: 3

docs/architecture/REPOSITORY-MAP.adoc
docs/proposals/estate-mathematical-architecture.adoc
mathesis_chora.deed

Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

Canon lockstep is red on main and on every PR: the deed pins canon 2.1.3 while standards canon.lock is 2.1.5 (2.1.4 was an editorial patch; 2.1.5 records gate table 0.3.1 from standards #1419, which only widens accepted layouts). Same change as hyperpolymath/rsr-template-repo#296: version 2.1.5, gates-sha256 5c510bba…, criteria-sha256 unchanged. The (provenance) clause keeps its mint-time 2.1.2 record. Verified: deed-field.sh reads 2.1.5 and 5c510bba…; the gates file on standards main hashes to 5c510bba…; validate-deed.sh with deed_lint.js reports 0 failing. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk

hyperpolymath · 2026-11-09T14:22:22Z

Canon lockstep failed, and the cause is on main, not in this PR. The deed pins canon 2.1.3, but canon.lock in standards is now at 2.1.5, so main and every PR fail this check.

I've ported the fix here as f22faaf. It is the same change as hyperpolymath/rsr-template-repo#296:

:version is now 2.1.5;
:gates-sha256 is now 5c510bba…, the gate-table 0.3.1 hash;
:criteria-sha256 is unchanged.

deed_lint.js (run through validate-deed.sh) reports 0 failing.

Generated by Claude Code

estate-rules' repo_map_determinism_test fails on main: applied-systems/ (owner-requested 2026-11-07) landed without regenerating the map. This is the output of `just repo-map`, unedited. Verified: tests/shape/repo_map_determinism_test.sh passes; scripts/check-root-shape.sh passes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KtYYb2239tLbYa19bmeJAk

hyperpolymath · 2026-11-09T14:23:16Z

estate-rules failed, and the cause is on main. tests/shape/repo_map_determinism_test.sh reports REPOSITORY-MAP.adoc as stale on main as well: applied-systems/ was added without regenerating the map.

I've ported the fix as the next commit on this branch. It is the output of just repo-map, unedited. The determinism test and check-root-shape.sh both pass locally.

Generated by Claude Code

sonarqubecloud · 2026-11-09T14:23:54Z

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

Canon lockstep fails on main (a3dbe73) and on this PR: the deed pins canon 2.1.3, while metadatastician/standards main canon.lock is 2.1.5 (gate table 0.3.1). This ports f22faaf from #29 unchanged: :version "2.1.5" and :gates-sha256 5c510bba…; criteria-sha256 is unchanged. The resulting blob equals #29's (ddb2e29), so this is a no-op once #29 lands. Verified against the live canon.lock: [canon] version 2.1.5, gates sha256 5c510bba…, criteria 6a5aa885…; the gates file on standards main hashes to 5c510bba…. The lockstep job's own compare step, run locally, passes on all three pins. validate-deed.sh with deed_lint.js at the pinned standards 8e48b1c reports 2 files, 0 failing; deed_clause_test, root shape, template conformance and governance tests pass. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY

chatgpt-codex-connector · 2026-11-09T15:46:15Z

Codex Review Summary: ❌ Failed

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	❌ Failed 2026-11-09T15:46:09.911843Z We couldn’t complete this review. Comment `@codex review` to try again.	`8d280cb`	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

Open a pull request for review
Mark a draft as ready
Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.

chatgpt-codex-connector · 2026-11-09T15:46:17Z

You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard.

hyperpolymath mentioned this pull request Nov 9, 2026

fix(census): comment-aware proof-holes.sh, Idris2 undefined-declaration axioms; refresh 13 rows #27

Open

9 of 10 tasks

hyperpolymath marked this pull request as ready for review November 9, 2026 15:46

hyperpolymath assigned Copilot Nov 9, 2026

hyperpolymath merged commit 946cc14 into main Nov 9, 2026
44 checks passed

Navigation Menu

Repository navigation

docs(architecture): Aeneas translations as a default ECHIDNA learning corpus - #29

docs(architecture): Aeneas translations as a default ECHIDNA learning corpus#29
hyperpolymath merged 3 commits into
mainfrom
claude/aeneas-echidna-corpus

hyperpolymath commented Nov 9, 2026

Uh oh!

coderabbitai Bot commented Nov 9, 2026 •

edited

Loading

Review limit reached

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

sonarqubecloud Bot commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

hyperpolymath commented Nov 9, 2026

Summary

Testing

Uh oh!

coderabbitai Bot commented Nov 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

hyperpolymath commented Nov 9, 2026

Uh oh!

sonarqubecloud Bot commented Nov 9, 2026

Quality Gate passed

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

chatgpt-codex-connector Bot commented Nov 9, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

coderabbitai Bot commented Nov 9, 2026 •

edited

Loading