Provenance restructure: archive v1.x, close the universal claim (PROMPT 1)#73
Merged
Conversation
Add `hub_ceiling`, the corollary of `pathCost_mono` that was never stated during v1.x development: any adapter path routing through an edge of grade g has pathCost >= g, so a single hub caps the fidelity of every format that must pass through it. Universal-and-high-fidelity is therefore self- contradictory the moment any format embeds into the hub at grade > 0; universal-and-low-fidelity is what JSON already is. This closes the universal-interoperability claim using the project's own bottleneck (max) algebra. The theorem is machine-checked with Lean 4.13.0 against its dependencies (`grade`, `pathCost`, `pathCost_mono`); it depends only on `propext` and contains no `sorry`. Existing theorems are unchanged. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Relocate the complete protocol-squisher v1.x working tree into provenance/, preserving relative structure, as a frozen evidence archive. Retained at the repository root: .git, .github, LICENSE, LICENSES, NOTICE. All moved paths are pure renames; no file content changed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add the provenance record for the v1.x archive: what the directory is; the state of the field at the start (harvested from INTENT.md and corrected to include the bottleneck-semiring lineage it omits); the need, theory, and practical challenges; an authorship/AI ledger built from the Co-Authored-By trailers; a cited methodology case study of what went wrong; the keepers; the hub-ceiling no-go as the closing result; and where the live threads went. Leaves a marked block for the author's first-person paragraph and two [ATTRIBUTION: JJ to confirm] markers where the human/AI split is not determinable from the repository. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Replace the v1.x README (now archived in provenance/) with a short honest root README: restart status pointing at provenance/PROVENANCE.adoc; the three-thread framing (field / theory / practical); a statement that the universal-interop claim is closed, with the hub_ceiling theorem linked; and a placeholder for the successor scope. Licence badge only; no roadmap; no claims. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Retire the nine workflows that exercised the archived v1.x code or proofs by moving them, unchanged, to provenance/.github-retired/ with a one-line note each (provenance/.github-retired/README.adoc). Add a single doc-lint workflow (.github/workflows/docs.yml) that renders the root AsciiDoc and the provenance record and does not touch archived code. Estate/credentialed workflows (governance, mirror, secret-scanner, scorecard, hypatia-scan, seambot, instant- sync, boj-build) are left untouched. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The v1.x .machine_readable set is archived (frozen) under provenance/. Create a
minimal root .machine_readable/6a2/ with STATE and META describing the new
situation: status "restarted", phase "successor-undecided", completion 0. META
records ADR-0001 — the provenance restructure, the pre-provenance-2026-06-11
tag, and the hub_ceiling closure of the universal-interoperability claim.
Modelled on the archived 6a2 templates (the repo's current TOML-like .a2ml
format), not the s-expression ABNF under standards/{state,meta}-a2ml, which
describe the older .scm dialect; see the final report.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Twelve open questions whose answers would fix the scope of any successor: universality after the hub-ceiling result; grammar-faithful parsers; whether the durable artefact is the grade vocabulary rather than a tool; a standalone schema-bloat linter; the smallest corpus-free claim; who would run the harness; where the tropical and linearity threads belong; the value of automated synthesis; the concrete user and measurement; and whether closing the repository is acceptable. Questions only. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Both still built or tested the archived code (cargo test; mix deps.get) and would fail or run pointlessly on the frozen tree, so the repo was not fully green. Move them, unchanged, to provenance/.github-retired/ with notes, leaving the root workflows as estate infrastructure (governance, mirror, secret-scanner, scorecard, scorecard-enforcer, instant-sync, boj-build) plus the doc lint. This also stops Hypatia security scanning for the archived repo, which is acceptable for an archive. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Use asciidoctor --failure-level=ERROR for the archive doc-lint. WARN level is strict enough to false-red on benign AsciiDoc warnings, which is the wrong threshold for a keep-green check over a frozen archive; cross-references and structure were verified by hand. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Integrate origin/main (PR #72, fcc6997 — a2ml-validate-action SHA bump). PR #72 modified .github/workflows/dogfood-gate.yml, which this branch retired to provenance/.github-retired/dogfood-gate.yml; git followed the rename and applied the one-line bump to the retired copy, so no content is lost and the archived workflow reflects its final state. Forward merge only — no history rewrite, no force-push. Co-Authored-By: Claude Opus 4.8 (1M context) <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
2 participants
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.
PROMPT 1 — protocol-squisher provenance restructure
Restructures the completed-but-superseded v1.x project into a frozen evidence
archive plus a clean root, in seven steps (one commit each):
feat(proofs)— addhub_ceiling, the corollary ofpathCost_monothatcloses the universal-interoperability claim (transport-class composition is
max, so any path through a shared hub is capped by the hub's worstembedding). Machine-checked under Lean 4.13.0; depends only on
propext;no
sorry. No existing theorem altered.refactor— move the entire v1.x tree, unchanged, intoprovenance/(523 pure renames). Kept at root:
.git,.github,LICENSE,LICENSES,NOTICE.docs(provenance)—provenance/PROVENANCE.adoc: what the archive is, thestate of the field, the authorship/AI ledger, a cited methodology case
study of what went wrong, the keepers, and the closing no-go result.
docs— short, honest rootREADME.adoc.chore(ci)— retire the workflows that exercised archived code/proofs toprovenance/.github-retired/; add a doc-lint; keep estate-infra workflows.docs(state)— fresh rootSTATE/META(.a2ml) for the restarted repo,with an ADR recording the restructure, the tag, and the hub-ceiling closure.
docs—SEED-QUESTIONS.adoc: open questions that would fix successor scope.The annotated, signed tag
pre-provenance-2026-06-11marks the pre-restructurestate.
Reviewer notes
hub_ceilingand its dependencypathCost_monocompileclean, but the rest of
TropicalAdapterPath.leandoes not under core Lean4.13.0 (pre-existing: Mathlib-only
push_neg, anAdapterPath/++typeerror). These were left untouched (the archive is frozen); the condition is
documented in
PROVENANCE.adoc.[JJ:]first-person paragraphin
PROVENANCE.adoc, a[JJ:]"what this becomes" line inREADME.adoc, andtwo
[ATTRIBUTION: JJ to confirm]markers.already ahead of
origin/mainbefore the restructure.one-commit-per-step history.
🤖 Generated with Claude Code