triage(backlog): notification-backlog report, parent-#7 split kit, db67 archive - #76
Merged
Merged
Conversation
- Closed #73 (338 files, conflicting): wrong-base duplicate of JoshuaJewell#7, where the same branch is clean/mergeable. Comment: PR #73 comment 5845153601. - docs/triage/2026-09-26-notification-backlog.md: full backlog report — every open PR/issue on fork + parent triaged, CI outage diagnosed (file-based workflows startup_failure repo-wide since 2026-09-25 22:19 UTC; settings/platform-side, owner action), rogue DOI-deleting branch arena/01a0db67 flagged. - docs/triage/pr7-split/: parent #7's 319-file change as 14 disjoint stacks (stacks/*.paths + make-stacks.sh + STACKS.md + RUNBOOK.md). Verified: disjoint, cover all 319 files, sequential apply reproduces the branch tree exactly. Stacks carry suggested titles for Option B (stacked PRs); Option A (merge #7 whole, review by stack) recommended. - Parent #8/#10/#11: verified dead (branches deleted, deltas already on fork main: 6c29b53, c0be951, 0ef5eee) — close commands in RUNBOOK appendix 1; bot has no parent write access. - .gitignore: track docs/triage/ (maintained triage state), ignore the derived 4.5 MB patches/ (regenerate via make-stacks.sh).
Resolves the .gitignore clash by keeping both additions: upstream's docs/formal/ negations plus this branch's docs/triage/ negations and the derived-patches ignore.
Owner asked to close the branch (selector correction). Archive its true delta (e33e10f..d94ecd4, 41 files) as a verified byte-exact patch plus restore instructions, and correct the report: the branch was stale docs (predates the DOI/ILR merges), not DOI-deleting — a merge would not have reverted PR #74/#75. The README.md deletion and missing SPDX headers were the real reasons to close it.
arena-ai-coding-agent
Bot
requested a review
from hyperpolymath
as a code owner
September 26, 2026 09:58
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
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 |
hyperpolymath
approved these changes
Sep 26, 2026
hyperpolymath
added a commit
that referenced
this pull request
Sep 26, 2026
…rs (#7) (#78) ## Summary First slice of #7 (Full Evidence Mode): the **formal foundations**. What a residual, an evidence-refined candidate set, a warrant token and a presence verdict *are* — proved, executable inside Agda, and pinned across implementations. The reference explorer's own footer admits its signed JavaScript model has **no proved extraction correspondence** with any proof. This PR closes exactly that gap: - **L0 — abstract semantics** (`Evidence.Residual`, `Echo`, `Warrant`): `Candidate observe r E = Σ W ((observe w ≡ r) × E w)`; `Holds` quantifies over *all* candidates, not the case's chosen witness; `actual-world-sound` is the honesty boundary (a warranted claim about candidates says nothing about reality until the actual world is shown admissible); `Echo`/`AvecFibre` fibre semantics with the total-space factorisation (the licence for storing rows as `(observed, witnesses)` pairs); `Warrant`/`Epi`/`SoundWarrant` with `epi-does-not-give` — a warrant token is not truth, proved by countermodel. - **L1 — signed finite model** (`Evidence.Signed`): `signed-integer-v1` as ℕ offsets, so every predicate is decidable and the model runs *inside Agda*; enumeration proved sound (`listed ⇒ satisfies`) and complete (`satisfies ∧ b ≤ 6 ⇒ listed`). - **L2 — decision procedures** (`Evidence.Decision`): the exact computation the server routes and the residual explorer run, proved to decide the candidate semantics: `entailed` ⇒ Present holds; `refuted` ⇒ Absent holds; `unresolved` ⇒ neither (explicit witnesses both ways); `inconsistent` ⇒ **no inhabited case** — an empty candidate set does *not* make claims vacuously true. The five reference presets land as computed, proved terms (e.g. `present-without-identification`: presence without a value). - **L3 — the pin**: 546 golden vectors (`proofs/vectors/evidence_vectors.json`, regenerate with `scripts/gen_evidence_vectors.py`) covering all four verdicts and both identification outcomes, for Julia and bun test stacks to consume so Agda/Julia/TS are bound to one truth. Negative control: `reject/IdentificationWithoutUniqueness.agda` — reporting an identified value from a mere presence verdict (the UI bug Evidence Mode exists to prevent) must fail to type-check, and does. ## Changes - `proofs/agda/MetaManifold/Evidence/` — six new stdlib-free modules (only `Agda.Builtin.*`, so they check under any Agda ≥ 2.6.4.3) - `proofs/agda/MetaManifold/All.agda`, `proofs/agda/README.md` — suite integration - `proofs/agda/reject/IdentificationWithoutUniqueness.agda` — new negative control - `scripts/gen_evidence_vectors.py` + `proofs/vectors/evidence_vectors.json` — the golden-vector pin - `docs/formal/evidence-verification.md` — layering, verdict theorems, theorem-to-test map, and what is deliberately *not* proved ## Verification - All six modules type-check clean (exit 0, no errors) under Agda 2.7.0.1, `--safe --without-K`. - `check-proofs.sh` guard logic replicated locally on all 17 modules: no postulates/holes/escape flags; pragma present. - Reject control fails with the error its `-- EXPECT:` line states. - `scripts/check-spdx.sh`: OK (327 files). - Vectors regenerate byte-identically (546 cases). - The full `All.agda` suite check runs in CI under the estate pin (Agda 2.6.4.3 + stdlib 2.1); the Evidence half is stdlib-free by construction, so toolchain drift cannot affect it. ## Scope note The UI layer of #7 (avec_fibre editor, fibre visualizer, residual explorer, warrant editor, provenance logging, DANGER banner) follows in later stacks on top of these foundations. Refs #7. ## Note on CI File-based workflows have been failing repo-wide with `startup_failure` since 2026-09-25 (diagnosed in #76 as settings/platform-side). If checks show that, it is unrelated to this change. --------- Co-authored-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.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
1 participant
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.
Summary
Triages the notification backlog (see
docs/triage/2026-09-26-notification-backlog.md). Docs + tooling only; no application-logic changes.Already done alongside (not in this diff):
arena/01a0db67at owner's request after archiving it here.Changes
docs/triage/2026-09-26-notification-backlog.md— every open PR/issue on fork + parent triaged; CI outage diagnosed (file-based workflowsstartup_failurerepo-wide since 2026-09-25 22:19 UTC; settings/platform-side, owner steps in runbook).docs/triage/pr7-split/— parent feat(ui): Full Evidence Mode — epistemic editor, fiber visualizer #7's 319-file change as 14 disjoint stacks (STACKS.mdreview guide,RUNBOOK.mdwith merge-as-is vs stacked-PRs options,make-stacks.shregenerates + verifies: disjoint, full coverage, sequential apply reproduces the branch tree exactly).docs/triage/db67-rescue/— archived deleted branch as a verified byte-exact patch + restore instructions..gitignore— trackdocs/triage/, ignore derived 4.5 MB stack patches.Verification
scripts/check-spdx.sh: OK (new .md/.sh carry fork-series headers).make-stacks.sh: 14 stacks, disjoint, cover all 319 files, reproduce branch tree exactly.db67-rescue/deleted-branch.patch: recreates the deleted branch tree exactly.Note on CI
File-based workflows cannot start repo-wide right now (the outage diagnosed in the report), so expect
startup_failure— unrelated to this docs-only change. Re-run once the owner fixes Actions.