Repository navigation
proofs: prove F-3 and H-3; remove the template Agda proof - #14
Conversation
Morphism.peak-not-strict proves the peak does not preserve the sequence product: peaks 2 and 3 with no drift sequence to peak 3, while the peaks sum to 5. Instances/HWM.HWM-not-annihilating proves HWM has no annihilating zero, refuted by a grade of peak 1. F-3 and H-3 move from TESTED to PROVEN, and C-4 in the direction HWM witnesses. The expected rejections PeakIsStrict and HWMAnnihilates stay as gate controls. verification/proofs/agda/Properties.agda was the template's example. It imported the standard library, which this repository does not use, so `just proof-check-agda` failed on main. It and its MANIFEST are removed; scripts/check-proofs.sh only reads proofs under verification/proofs, so the manifest cannot point at src/. The development stays gated by scripts/check-agda.sh in proofs.yml. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LiQzWJdcPfRU6YMDGRG8Xi
|
Caution Review failedThe pull request is closed. Finishing Touches
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. Comment |
Dogfood Gate's canon lockstep compares the deed's (canon ...) clause with canon.lock on standards main, which moved to 2.1.3 with a new gates hash. The pin moves from 2.1.2 as rsr-template-repo#255 did; the criteria hash is unchanged. The mint record keeps 2.1.2, the canon the repo was minted under. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LiQzWJdcPfRU6YMDGRG8Xi
|
|
Four workflows fail to load, and the cause is outside this PR:
No re-run would help: the error is deterministic. The other 24 workflow runs on Generated by Claude Code |
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 65f1c51e89
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| * `verification/proofs/agda/Properties.agda` and its MANIFEST are removed. | ||
| They were the template's example, imported the standard library this | ||
| repository does not use, and made `just proof-check-agda` fail on main. | ||
| The development is checked by `scripts/check-agda.sh` (CI `proofs.yml`). |
There was a problem hiding this comment.
When Agda is installed, removing both files makes just proof-check-agda report that there is nothing to check and exit successfully: build/just/proofs.just delegates exclusively to scripts/check-proofs.sh, which exits early when this manifest is absent. Consequently, just proof-check-all and the repository's just ci target no longer compile any of the proofs under src/; the separate proofs.yml workflow does not preserve those documented local/full-CI commands. The manifest format accepts an arbitrary source root, so retaining it with an entry rooted at src for ResourceAlgebra/All.agda would keep this gate meaningful without modifying the template-synced checker.
Useful? React with 👍 / 👎.
| | C-2 | The ⊕-induced relation `≼` is a partial order with `𝟘` least and `⊕` its join | PROVEN (`≼-refl`, `≼-trans`, `≼-antisym`, `𝟘-least`, `⊕-upperˡ/ʳ`) | ||
| | C-3 | Every dioid is ordered: distributivity ⇒ `⊗` monotone on both sides | PROVEN (`IsDioid.ordered`) | ||
| | C-4 | `IsAnnihilating` is independent of `IsDioid` (an instance can be one without the other) | TESTED (HWM is a dioid; `tests/reject/HWMAnnihilates.agda` refuses the zero) | ||
| | C-4 | `IsAnnihilating` is independent of `IsDioid` (an instance can be one without the other) | PROVEN in one direction: HWM is a dioid (`HWM-dioid`) and not annihilating (`HWM-not-annihilating`); control `tests/reject/HWMAnnihilates.agda`. No instance yet witnesses the converse (annihilating, not a dioid) |
There was a problem hiding this comment.
C-4 claims that IsAnnihilating and IsDioid are independent, but the new proof establishes only a dioid that is not annihilating, and this same row explicitly says that no converse witness exists. Marking the row PROVEN therefore overstates the checked result; keep the overall independence claim open/tested or split it into separate directional claims until an annihilating non-dioid instance is proved.
Useful? React with 👍 / 👎.
## Summary `hyperpolymath/standards` moved to `metadatastician/standards`. Four workflows stopped loading because of it: Governance, Rust CI, Hypatia and Secret Scanner (`workflow was not found`; see #14). - A reusable-workflow `uses:` does not follow the rename. - A hyperpolymath repository cannot call a reusable in metadatastician's repository. hyperpolymath/rsr-template-repo#253 measured it: every caller failed at startup. This PR ports rsr-template-repo's CI from `60cedf1` (the canary state) to `8034fc9`, its last green main commit. Template main has been red since a run of direct file renames on 2026-10-26, which are not ported here. ## Changes - **Method.** A three-way apply of the template's own diff over `.github`, `scripts`, `tests`, `.machine_readable`, `verification`, `build/container` and the K9 records. Then the mint's self-name pass, run exactly as `repo-init.just` defines it. Conflicts were resolved toward the template, except `estate-rules.yml`, which keeps this repository's own tests. - **Workflows.** - Governance, Secret Scanner, Rust CI, Hypatia, Scorecard and Mirror now run self-contained, checking out `metadatastician/standards@8e48b1c`. - New: `squabble.yml`, `proven-tests.yml` and `fork-governance.yml`. - Deed and K9 validation move into Dogfood Gate, so `deed-validate.yml` and `k9-validate.yml` go, as the template did in #247. - **Config.** - Container config is now KYAML. It was rendered with this repo's values and canonicalised by `kyaml-format.sh`, and its parsed data is byte-identical to before. - `deploy.k9.ncl` is re-rendered at K9 contract v1.0.0. `coordination.k9.ncl` and `session/custom-checks.k9.ncl` gain `component_type`. - The aibdp schema is JCS-canonical. - CLAUDE.md is regenerated by the arrival pack, plus the template's hand-written Proofs section. - `actions.lock` is the template's lock plus `proofs.yml`. - **This repo's tests.** - `actions_lock_sha_refs_test.sh` lost its subject: governance no longer calls a standards reusable. It now checks every SHA-keyed record in the lock against an exact table (tag, owner and repo IDs), keeps all its negative controls, and refuses any reusable call into the moved repository. Planted regressions fail it as intended. - `ffi_strings_test.sh` and `container_kyaml_test.sh` join `mint-verbatim.txt`. They are token fixtures, which the placeholder gate otherwise rejects. - **Not ported.** The template's generator tests (the use-this-template mint, the template-pin resolver and the e2e mint tests) exercise `build/just/repo-init.just`, and this port does not bring the generator. ### Known gap, by owner decision The self-contained governance runs one policy step. The reusable it replaces ran 19 jobs, among them UUID v8 conformance, licence consistency, actions-lockfile verify, the debt and exemption ratchets and the JS runtime checks. They come back when the owner makes `metadatastician/standards` callable from hyperpolymath; the template has the same gap. ### Template defects found on the way (not fixed here) - `container-init` renders the container KYAML without reformatting it. A freshly minted child therefore fails "Converted YAML stays KYAML". - `mint-verbatim.txt` omits `tests/ffi_strings_test.sh` and `tests/workflows/container_kyaml_test.sh`. A fresh child fails the placeholder gate. - Template main has been red since the 2026-10-26 renames, for example `LICENSE` to `LICENSE.adoc` and `CODEOWNERS` to `CODEOWNERS.adoc`. ## RSR Quality Checklist ### Required - [x] Tests pass (`just test` or equivalent) - [x] Code is formatted (`just fmt` or equivalent) - [x] Linter is clean (no new warnings or errors) - [x] No banned language patterns (no Python, Go, TypeScript, Deno or ReScript; JavaScript runs on Bun) - [x] No `unsafe` blocks without `// SAFETY:` comments - [x] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) - [x] SPDX license headers present on all new/modified source files - [x] No secrets, credentials, or `.env` files included ### As Applicable - [x] Documentation updated for user-facing changes - [x] `CHANGELOG` or release notes updated ## Testing Run locally, with yq 4.53.3 sha256-verified as CI installs it: - Every `tests/workflows/*.sh` and `tests/shape/*.sh` passes. - `check-lock-sync.sh` reports the lock in sync and transitively closed. - The deed and K9 hooks pass against `metadatastician/standards@8e48b1c`: 15 K9 files, 0 failing. - `kyaml-format.sh --check` passes on all three container files. - `check-ijson-jcs.sh --enforce`: 12 of 12 files canonical. - `check-required-contexts.sh`, `check-no-placeholders.sh`, `check-root-shape.sh`, the repository-map determinism test and `check-adoc-renders.sh` all pass. - `validate-template.sh`: 0 errors. `check-agda.sh`: all proofs and the 8 rejections pass. --- _Generated by [Claude Code](https://claude.ai/code/session_01LiQzWJdcPfRU6YMDGRG8Xi)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
Summary
Two ledger rows that only an expected rejection backed are now proved, and the template's example Agda proof is gone. This PR also ports the canon 2.1.3 pin that Dogfood Gate needs.
Changes
Morphism.peak-not-strictproves the peak does not preserve the sequence product. Peaks 2 and 3 with no drift sequence to peak 3, while the peaks sum to 5. This holds whatever the units do. F-3: TESTED → PROVEN.Instances/HWM.HWM-not-annihilatingproves HWM has no annihilating zero. A grade of peak 1 refutesannihilˡ. H-3: TESTED → PROVEN. C-4 moves too, but only in the direction HWM witnesses (a dioid that is not annihilating). No instance yet witnesses the converse, and the ledger says so.PeakIsStrictandHWMAnnihilatesstay as controls on the gate. No test is removed.verification/proofs/agda/Properties.agdaand itsMANIFESTare removed.just proof-check-agdafailed on main.scripts/check-proofs.shonly reads proofs underverification/proofs/, so its manifest cannot point atsrc/.scripts/check-agda.shinproofs.yml.check-proofs.shabout source roots outsideverification/proofs/would letjust proof-check-agdachecksrc/. That script is template-synced, so the change belongs in rsr-template-repo, not here.canon.lockon standards main moved to 2.1.3, with a new gates hash, after main last passed on 2026-10-19.(canon …)pin now moves from 2.1.2 to 2.1.3, as chore(canon): adopt canon 2.1.3 in the spine deed rsr-template-repo#255 did. The criteria hash is unchanged.docs/status/PROOF-STATUS.adocrows C-4, H-3 and F-3 are updated, and so isCHANGELOG.adoc.RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
CHANGELOGor release notes updatedTesting
Run locally on Agda 2.6.3. CI pins 2.6.4.3.
scripts/check-agda.sh: core proofs, unit tests and all 8 expected rejections pass.scripts/check-proofs.sh agda: "nothing to check". It failed on main.scripts/scan-dangerous.sh: no dangerous constructs.scripts/validate-template.sh: 0 errors.tests/workflows/*.shpasses.deed_lint.jsreports OK on the deed.🤖 Generated with Claude Code
https://claude.ai/code/session_01LiQzWJdcPfRU6YMDGRG8Xi