Repository navigation
chore(ordinal): move the ordinal lane out of echo-types (do not merge until the new repo is published) - #349
Merged
Merged
Conversation
…ee bridge modules Removes proofs/agda/Ordinal/** except Ordinal/OmegaMarkers.agda and Ordinal/Buchholz/Syntax.agda, which EchoOrdinal (the echo-to-ordinal bridge) imports. Drops the removed modules from All.agda and their pin blocks from Smoke.agda. This carries out the disposition recorded in D-2026-06-21: the ordinal lane is extracted to its own repository, with history, and no new ordinal rung is opened here. Verified in this tree: agda -i proofs/agda proofs/agda/All.agda exit 0 (1m48s) agda -i proofs/agda proofs/agda/Smoke.agda exit 0 sh scripts/kernel-guard.sh PASS Nothing else in the Agda sources imported the removed modules; only EchoOrdinal, All and Smoke referenced them. The two postulates in Ordinal/Buchholz/Fidelity.agda leave with it, so this repo's quarantined postulates go from three to one. Docs are not swept here: the moved documents stay in place until the new repository's URL exists. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
Contributor
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info
📜 Recent review details
📝 Summary
Merge Risk: ⚪ Minimal · up to
|
| Check name | Status | Explanation |
|---|---|---|
| Title check |  |
The title clearly summarises the main change: moving the ordinal lane out of echo-types. It also states the merge condition. |
| Description check | |
The description directly explains the ordinal lane removal, retained modules, verification results, trust boundary changes, and merge dependency. |
| Docstring Coverage | |
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0… |
| Linked Issues check | |
Check skipped because no linked issues were found for this pull request. |
| Out of Scope Changes check | |
Check skipped because no linked issues were found for this pull request. |
Full details: Docstring Coverage
-
Explanation
No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0 files.
✨ Finishing Touches
-
📝 Generate docstrings
-
- Commit to this branch
- Create a new PR
-
- 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.
Comment @coderabbitai help to get the list of available commands.
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
hyperpolymath
marked this pull request as ready for review
October 20, 2026 14:07
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: 0dd4dd460a
ℹ️ 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".
| @@ -1,237 +0,0 @@ | |||
| {-# OPTIONS --without-K #-} | |||
|
|
|||
| -- hypatia: allow code_safety/agda_postulate -- order-type fidelity for the Buchholz notation (D-2026-06-14) is external mathematics; the TWO named postulates below (denotation, ordinal-upper-bound) are the explicit, documented trust boundary. The former third postulate (the whole BH structure) is now CONSTRUCTED for real in the --safe module Ordinal.Buchholz.BHTarget; only the candidate BH height remains, as an explicit module parameter (AtHeight). This module is OUTSIDE the --safe kernel cone by design, is NOT imported by All.agda/Smoke.agda, and asserts NOTHING that the --safe core depends on. See Fidelity-OPEN-postulates.md. | |||
There was a problem hiding this comment.
Once this commit deletes the only Fidelity.agda, the basename-only "Fidelity" exemption remains in tools/check-guardrails.sh:42-46 and is applied unconditionally by is_exploratory_exempt at lines 75-92. Consequently, a future proofs/agda/**/Fidelity.agda—even an unrelated, unwired module—can omit --safe/--without-K and contain postulates or forbidden pragmas while the CI guardrail passes, undermining the stated reduction of the trust boundary; remove this exemption along with the module.
Useful? React with 👍 / 👎.
🔍 Hypatia Security ScanFindings: 38 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 48,
"reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 48,
"start_line": 48
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
"type": "WH014",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/WH014",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
…ered (Codex P2) tools/check-guardrails.sh exempted any file whose basename is exactly "Fidelity" from the --safe / --without-K / no-postulate checks. The only such file was Ordinal/Buchholz/Fidelity.agda, which this PR removes, so the entry would only let a future unrelated Fidelity.agda skip the checks. EchoFidelity.agda is not matched (the comparison is on the whole basename) and was never exempt. tools/check-guardrails.sh passes before and after: all 137 modules declare --safe --without-K, no escape pragmas, no postulates. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV
🔍 Hypatia Security ScanFindings: 38 issues detected
View findings[
{
"reason": "Required file missing",
"type": "missing",
"file": "0-AI-MANIFEST.a2ml",
"level": "epi",
"action": "create",
"rule_module": "root_hygiene",
"severity": "high",
"evidence": [
{
"span": {
"file": "0-AI-MANIFEST.a2ml",
"end_line": 0,
"start_line": 0
},
"rule": "root_hygiene/missing",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "triage",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
"type": "missing_timeout_minutes",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium",
"recipe_id": "recipe-add-workflow-timeout-minutes",
"job": "sync",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_audit/missing_timeout_minutes",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 39,
"reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 39,
"start_line": 39
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 53,
"reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 53,
"start_line": 53
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 87,
"reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 87,
"start_line": 87
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 46,
"reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
"type": "RE001",
"file": ".github/workflows/push-email-notify.yml",
"level": "epi",
"action": "report",
"rule_module": "research_extensions",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/push-email-notify.yml",
"end_line": 46,
"start_line": 46
},
"rule": "research_extensions/RE001",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 34,
"reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/labels.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/labels.yml",
"end_line": 34,
"start_line": 34
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": 48,
"reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
"type": "WH006",
"file": ".github/workflows/label-triage.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "medium",
"evidence": [
{
"span": {
"file": ".github/workflows/label-triage.yml",
"end_line": 48,
"start_line": 48
},
"rule": "workflow_hardening/WH006",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
},
{
"line": null,
"reason": "workflow .github/workflows/hypatia-scan.yml uploads SARIF to code scanning but masks the scanner's failure (`|| true` / `|| echo 0`) and never asserts the findings artefact is a non-empty array. When the scanner fails, this uploads a SARIF with zero results, and GitHub AUTO-CLOSES every previously-open alert for that category — silently, with the job green.",
"type": "WH014",
"file": ".github/workflows/hypatia-scan.yml",
"level": "epi",
"action": "report",
"rule_module": "workflow_hardening",
"severity": "high",
"evidence": [
{
"span": {
"file": ".github/workflows/hypatia-scan.yml",
"end_line": 0,
"start_line": 0
},
"rule": "workflow_hardening/WH014",
"observations": 1,
"rule_version": "0.1.0"
}
],
"support": {
"kind": "pattern"
}
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
Oct 26, 2026
## Summary #349 removed the ordinal lane from the tree, but the docs still describe it as present. This PR brings them in line with the tree and points readers at https://github.com/hyperpolymath/ordinal-notation. Its import PR is hyperpolymath/ordinal-notation#1, still a draft. ## Changes - **Living status documents** now say the lane moved and that only `EchoOrdinal`, `Ordinal.OmegaMarkers` and `Ordinal.Buchholz.Syntax` stay. Files: `CLAUDE.md` (with a new session arc at the top), `EXPLAINME.adoc`, `PROOF-STATUS.adoc`, `TOPOLOGY.adoc`, `roadmap.adoc` Lane 3, `docs/echo-types/MAP.adoc`, `docs/bridge-status.adoc`, `docs/proof-obligations.adoc`, `docs/echo-types/echo-kernel-note.adoc`, `docs/echo-types/what-echo-is.adoc`, and the three wiki pages. - **`docs/proof-debt.adoc`**: (d) is now empty here. The two `Fidelity.agda` postulates left with the lane, so echo-types has one quarantined postulate block, under (c). - **Corrections to existing claims:** - `EXPLAINME.adoc` said no `Echo*.agda` imports from `Ordinal/`; in fact `EchoOrdinal` imports the two leaves that stayed. - `PROOF-STATUS.adoc` called the Fidelity postulates "the ONLY postulates", ignoring `EchoImageFactorizationPropPostulated`. - **Moved documents.** The seven design and decision documents that moved with the lane get a "moved" banner and stay here as frozen copies: `docs/bridges/buchholz-*.adoc`, `docs/echo-types/buchholz-rank-obstruction.adoc`, the two ordinal decision records, and `Fidelity-OPEN-postulates.adoc`. - **Not edited:** - `AFFIRMATION.adoc` is a signed, dated snapshot. - Proof logs and dated status files. - `CLAIMS_AUDIT.adoc` rows; a note at the top says some rows describe the tree as it was when audited. - `docs/echos/` is about `EchoFidelity`, which is unrelated. - `CHANGELOG.adoc` has entries for the removal and this sweep. ## Testing This PR changes docs only. ``` sh scripts/kernel-guard.sh PASS bash tools/check-guardrails.sh OK (137 modules) git diff --check clean ``` ## Left for the owner - The GitHub repository description for echo-types still says "Mechanized Bachmann-Howard ordinals, Buchholz/Veblen hierarchies" (`CLAIMS_AUDIT` S-002). It needs changing in the repo settings. - #263, the extraction tracking issue, can be closed once ordinal-notation#1 merges. - Whether to delete the seven frozen copies later. They are kept for now, so existing links do not break. --- _Generated by [Claude Code](https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Do not merge yet
This removes the only copy of the ordinal lane from
main. Merge it after the extracted repository exists on GitHub and has been pushed. History is preserved either way, but the lane should have its new home first.Summary
Carries out the disposition recorded in
D-2026-06-21: the ordinal lane is extracted to its own repository and echo-types stops carrying it. No new ordinal work is opened here.proofs/agda/Ordinal/**(74 files, about 12,600 lines) exceptOrdinal/OmegaMarkers.agdaandOrdinal/Buchholz/Syntax.agda, which stay becauseEchoOrdinal(the echo-to-ordinal bridge) imports them.All.agda(73 lines) and their pin blocks fromSmoke.agda(28 blocks).EchoOrdinal,Ordinal.OmegaMarkersandOrdinal.Buchholz.Syntaxstay pinned.docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc(§Disposition). I re-checked it against the sources: onlyEchoOrdinal,AllandSmokeimport the removed modules, and the removed tree imports nothing from the rest of echo-types (stdlib only).Trust boundary
The two postulates in
Ordinal/Buchholz/Fidelity.agda(denotation,ordinal-upper-bound) leave with it. echo-types' quarantined postulates go from three to one (the cubical-island shadow inEchoImageFactorizationPropPostulated).Verified
The extracted tree was built separately:
agda proofs/agda/All.agdaexits 0 in 28 s (75--safemodules), and the quarantinedFidelity.agdaloads on its own.Not done here (follow-up once the new repo's URL exists)
Fidelity-OPEN-postulates.adoc,docs/bridges/buchholz-*.adoc,docs/echo-types/buchholz-rank-obstruction.adoc, the twoordinal-*decision records) are still in this repo; the decision record needs a pointer to the new repo, andCLAUDE.md,roadmap.adoc,MAP.adoc,proof-debt.mdand the wiki still describe the lane as living here.CLAUDE.md's build loop still globsproofs/agda/Ordinal/*.agda; harmless, but stale.OmegaMarkersandBuchholz.Syntaxnow exist in both repos and can drift.Generated by Claude Code