docs: state the idea — domain transition, silent failure, and the 007 dual - #53
Merged
Conversation
… dual
The clearest articulation of what this repo is for existed in exactly one
place: a dated entry in DESIGN.md from 2026-06-18. The README said
'semantic overlay for tracing how claims move from source to target',
which is true but too abstract to build from, and ARCHITECTURE.md is
template boilerplate ('Separation of Concerns', 'Each module has a single
responsibility') that says nothing about this repo.
State it properly: a claim can hold on BOTH sides of a domain transition
and still not MEAN the same thing on both sides. The invariant is not
'true here and true there' but 'the same claim here and there'. The
failure is silent by construction — cross-domain equality is not
expressible from inside either domain, so every per-domain test can pass
forever while the load-bearing claim is already broken.
Also names the dual explicitly: 007's hermeneutic semantics is the mirror
case (same syntax, different readings) where this is many syntaxes, one
meaning. Anyone working on one should read the other.
And states the profile rule that was only implicit: a profile is a lens
onto a corpus that lives elsewhere and does NOT vendor it (see pmpl).
examples/same-cube violates this today; flagged inline.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedDocumentation update clarifying the core concepts of domain transition, silent cross-domain failures, and the 007 dual across the README and architectural guides. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 5 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
…not-paraphrase The manifest is the universal AI entry point, and its purpose field said 'monorepo for heuristic extraction and classification, provides a shared CLI'. That describes the plumbing. An agent reading it learns nothing about domain transitions or claim identity, so it reads the code and invents its own account — which is how this idea has been re-derived and distorted repeatedly, each restatement plausible and each drifting further. Add a core-idea block carrying the canonical statement, why the failure is silent by construction, the faces/cube worked example, the explicit dual with 007, the profile vendor-nothing rule, and the known deviation (issue #54). Marked DO NOT PARAPHRASE: quote or link, and if you think it is wrong, argue the point rather than silently improving the wording. The purpose field now says outright that reading only it is how the idea gets lost. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This was referenced Aug 5, 2026
hyperpolymath
added a commit
that referenced
this pull request
Aug 5, 2026
…ure (#56) **This repo has had no working CI.** All 16 workflows return `startup_failure` in 0s; the last 30 runs are `startup_failure` without a single exception. That has a consequence worth stating before anything else: **the two open PRs here (#53, #55) have never been verified by anything.** Their green-looking absence of failures is an absence of checks. ## Cause Workflow-lockfile enforcement is active on this account, and this repo had no `.github/workflows/actions.lock`. ## The cure, in four steps Proven on haec#50 and trope-particularity-workbench#45. It takes four steps because **each one's failure is invisible until the previous is fixed** — they surface strictly one at a time: 1. **`gh actions-lock`** — generates the lockfile, normalises pins to readable tags. 2. **Hoist SPDX back to line 1.** `actions-lock` inserts its own banner as line 1, and the workflow linter requires the SPDX header there — so the tool that cures the startup failures reddens every workflow file unless this is undone in the same commit. 3. **Hand-author an empty `[]` lockfile entry per reusable caller** (6 here). `gh actions-lock` **skips reusable-workflow callers**, so without this they remain `startup_failure` while everything else goes green — which reads as a partial fix rather than a missing step. 4. **Re-pin those callers** to standards `bd0df9ead7fa`, the commit that made the governance check lockfile-aware. Verified present via the commits API rather than copied. ## Expect failures Nothing here has been checked in a long time. The first green run is a **starting point, not a result** — some of what surfaces will be real and long-standing. If two callers come back `startup_failure` after this, the cause is permission escalation (a reusable requesting more than its caller grants is rejected before any job starts, producing no log); that was the last residual on tpw#45. Found during the 2026-08-05 estate CI/CD census, which measured 8 repos mostly dead and 47 partly dead out of 421. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
…ayer broke (#55) Stacked on #53 (it quotes the `(core-idea (statement …))` block that #53 introduces). Base retargets to `main` automatically when #53 merges. ## What this is The three-layer claim-checking architecture (type / trope / knot) invited an obvious attack: if Layer 1's diode makes every admissible strand monotone in time, the configurations are braids rather than knots, and Layer 3 looks like an optimizer rather than a layer. I built the sharpest five-count case against Layer 3 I could, then had it attacked adversarially, with a separate fact-check of the theorems it relied on. **Three of the five counts broke** — two of them on checkable errors in my own argument. This ADR records the surviving position. ## Why an ADR and not a `DESIGN.md` entry Deliberate. The core idea of this repository was written down correctly, and only, in a dated `DESIGN.md` entry (2026-06-18). It was accurate and invisible: readers took the plumbing description from the manifest, went to the code, and reconstructed the idea their own way. This record has the same failure profile — a load-bearing conclusion that reverses a plausible position — so it goes where it can be found. This adds `docs/decisions/` (the estate norm, present in trope-checker, typell, boj-server). The repo had no ADR infrastructure. ## The three counts that broke **Count 1 — "topology cannot form" — wrong.** The diode constrains *edges*, but it cannot constrain the Morse structure at *vertices*, and Layer 2 mandates them. A merge is a local maximum of time along any cycle through it; a split is a local minimum. So a confluence diamond is a closed curve with one min and one max — the profile of a round circle — and two of them link with **every edge strictly forward in time**. No closure, no time-reversal. The supporting lemmas all fact-checked correct; the false premise was *unpinned*: shared anchors and shared conclusions identify endpoints, and Artin combing needs a free boundary. **Count 2 — "the plane is notation" — falls to intrinsic linking.** Conway–Gordon properties are fixed by incidence alone yet quantify over all realizations. Drawing-invariant and epistemically contentful, and no Layer 1 predicate quantifies over embeddings. **Count 5 — "it is only a complexity switch" — falls to the doubling attack.** Present one derivation twice, paraphrased, under distinct labels. Label-honest (diode silent), well-founded, exogenously attested, each copy individually warranted. It has an **identical pass/fail profile to genuine two-witness corroboration on every subdiagram** — so the exponential sweep cannot distinguish them even in principle — yet corroboration weight is 2 vs 1. Worse, the sweep answers *its own* robustness question wrongly without the identity quotient supplied as input. ## The decision Layer 3 is retained, with a restated charter: it adjudicates **identity of an argument across presentations**, issuing equivalence certificates (a move sequence whose every intermediate stays green) or obstruction certificates. Reduction to an equivalence proof is not a demotion — detection and equivalence-certification are dual. And the dependency arrow was missing one direction. The design ran L1 → L3 (temporality gives clean orientations). The missing arrow is **L3 → L2**: overlapping presentations must be recognised as the same argument *before* resource accounting, or L2 double-counts. ## ⚠ Two things recorded as open, not resolved **The Layer 2 vocabulary does not match committed code.** Of the six terms in play (strength, consistency, coherence, resemblance-warrant-on-merge, p-residue, p-sufficiency), only **p-sufficiency** is real — `floor(U) ⊑ acc(v)`. **`p-residue` does not exist anywhere in the estate.** What is built in `trope-checker@69221ad` is a six-coordinate `Grade`, nine `p-*` effects, a `Floor`, and a witness-carrying `Verdict`. This matters because Count 3 read p-residue as affine resource accounting — a term I could not ground — so the reachability result should be re-derived against the actual grade algebra. Also, `check-vocabulary.sh` hard-fails on entries outside the nine. **"Knot" is already taken — by a repo doing this exact job.** quandledb hosts KRL (Knot Resolution Language) and 007 proves a knot composition monoid with a real `unknot`. More interesting than a clash: QuandleDB describes itself as *"the invariant/equivalence + semantic-identity face"* — the charter this ADR assigns to Layer 3. ## Verification - **Quote check**: the canonical `(statement …)` is reproduced verbatim — diffed character-by-character against `0-AI-MANIFEST.a2ml`, identical. - `asciidoctor -o /dev/null docs/decisions/*.adoc` — parses clean, no warnings. - `reuse lint` — none of the new files flagged; missing-info count unchanged from baseline (1, pre-existing). - Every cross-repo `file:line` citation re-resolved against a recorded SHA. - No code touched. Note: `trope-checker` has two working copies at different commits (`hyper-repos` @ `69221ad`, `_TROPES _SET` @ `680fc20`). Citations use the former and record the SHA. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,704 @@ | |||
| // SPDX-License-Identifier: CC-BY-SA-4.0 | |||
…#60) Stacked on #53. Retargets to `main` automatically when that merges. ## The correction that drove this The **three-layer claim checker** is this repository's principal subject — and it was barely documented, while the AffineScript same-cube example was over-represented relative to it. `faces` is one profile of six, a lens onto a corpus that lives elsewhere: a good demonstration of the idea in miniature, not the subject. This PR fixes that proportion. ## Human **`ARCHITECTURE.md` was template boilerplate** describing `src/`, `tests/`, `config/` and `README.adoc` — none of which match this repo — duplicating the real `docs/ARCHITECTURE.md`, and saying *nothing whatever* about the three layers. (Closed PR #58 independently spotted this as "drop false ARCHITECTURE"; it did not land, so the problem persisted.) Rewritten in two parts: **Part I** the layer architecture — Layer 1 (`type`) and what the diode actually buys, with its three open problems (epistemic vs ontic clock, partial-order time, composition-forgery as holonomy); Layer 2 (`trope`) as actually built in `trope-checker`/`hermeneia`, affine with a guarded contraction rule; Layer 3 (`sortal`), the doubling attack, and the `L3 -> L2` dependency arrow. **Part II** the shipping extractor/classifier. **`README.md` had drifted from the tool.** It said every face's lowering "must normalise to the same canonical text"; the verifier now compiles each face to typed-wasm and compares `sha256`, keeping text diffs as a diagnostic only. The README asserted something that held on both sides of a transition while no longer meaning the same thing — **this repository's own failure mode, turned inward.** ## Machine `0-AI-MANIFEST.a2ml`: real structure (it omitted `docs/decisions/`, `proofs/`, `examples/`, `src/ui/`); new `(architecture …)` block with the three layers, dependency order, doubling attack, decided-not-built status and the `L1`/`L2`/`L3` numbering hazard; new `(debt …)` block; ADR-0001 in milestones. **The do-not-paraphrase `(core-idea)` block is untouched.** **Wiki** was a one-line stub → `Home` + `Three-Layers` (pushed separately — wikis are their own git repo). ## Debt — new `docs/DEBT.md` | | Dimension | Open | Worst | |---|---|---|---| | A | Architecture | 3 | **HIGH** | | C | CI/CD | 3 | MEDIUM | | L | Licence | 3 | MEDIUM | | D | Docs | 3 | MEDIUM | | P | Proof | 2 | MEDIUM | | K | Code | 1 | LOW | **The headline finding went stale mid-audit, and that is recorded rather than hidden.** C1 was filed CRITICAL — no lockfile, every workflow `startup_failure` on every branch, `main` never green. **PR #56 fixed it while this was being written.** Re-measured: 10 workflows green on `main` including Rust CI, CodeQL and Secret Scanner. C1 is now RESOLVED with the history kept, and the residue split into C2 (Scorecard still `startup_failure`), C3 (two workflows failing on *content*, untriaged — invisible until the lockfile landed), C4 (no proof gate). Other findings: - **L1** — GitHub reported **no licence**. Cause found: `LICENSE` deviated from canonical MPL-2.0 by a **trailing space** (line 38) and `http` vs `https` (line 360). Replaced with the canonical text. - **A1–A3** — Layer 1 has no substrate anywhere; Layer 3's equivalence side does not exist; Layer 2's vocabulary does not match its implementation (**`p-residue` exists in no repository**). - **P1** — `SameCube.agda` is genuinely good (`--safe`, zero postulates, zero holes) but **ungated**. `docs/tech-debt-2026-05-26.md`'s "RESOLVED" banner was **partly wrong** and is corrected in place: licence was not actually detected, and proof debt was half closed. ## Repo metadata (applied via API, not in this diff) - **Description** was `Dual-use claim-grounder (Phase A in progress)` — vague and stale. Now states what the tool does and its governance role. - **Topics** were `development, hyperpolymath, open-source, rust, software, tooling` — owner name, generic words, and a language GitHub detects itself. Replaced with eight concept-level ones: `claim-checking`, `argumentation`, `semantic-drift`, `provenance`, `cross-domain-equivalence`, `architecture-decision-records`, `formal-methods`, `static-analysis`. ## Verification - `0-AI-MANIFEST.a2ml` parens and quotes balance - `reuse lint` missing-info count **unchanged** from baseline (1, pre-existing) — verified by stashing and re-running - every path cited in `ARCHITECTURE.md` exists on disk - CI state re-measured per workflow before publishing the claim - no code touched 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5 <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.
The clearest statement of what this repo is for existed in exactly one place: a dated entry in
DESIGN.mdfrom 2026-06-18, filed as an implementation decision. The README said "a repo-native semantic overlay MVP for tracing how claims move from source evidence/specification to target conclusions" — true, but too abstract to build from.ARCHITECTURE.mdis template boilerplate ("Separation of Concerns", "Each module has a single responsibility") that describes no repo in particular, with an empty## Directory Structureheading.That gap has costs. Someone with only the README to go on cannot tell what a profile is supposed to do — which is very likely why
examples/same-cube/ended up vendored inside this repo and the profile named after a claim rather than its target corpus.What this states, that was previously only implicit
The idea. A claim can hold on both sides of a domain transition and still not mean the same thing on both sides. The invariant is not "true here and true there" — it is "the same claim here and there". That path is the thing that must be invariant.
Why it needs tooling at all. The failure is silent by construction: cross-domain equality is not expressible from inside either domain. A test in domain A checks A against itself; a test in B checks B against itself. Every per-domain test can pass forever while the load-bearing claim is already broken — and everything looks green, because each side really is internally consistent.
The worked example, promoted out of the decision log: AffineScript's faces all lower to one canonical form; per-face snapshot tests catch drift within a face and can never compare face A's cube against face B's. The cross-face equality is the load-bearing claim, and no per-face test can even express it.
The dual with
007. Named explicitly, because the two repos are halves of one concern and currently read as unrelated:Many forms, one meaning against one form, many meanings.
The profile rule. A profile is a lens onto a corpus that lives elsewhere; it names a target by path and does not vendor it — see
profiles/pmpl.md, which points at the palimpsest-license tree and copies nothing. A profile that carries a copy of its target drifts from the real thing and starts grounding a claim about a stale fixture, which is this tool's own failure mode turned inward.Known deviation, flagged inline rather than silently fixed
examples/same-cube/vendors an AffineScript corpus, and the profile is calledfaceswhere the other five are named for their target repo (echidna,panll,hypatia,pmpl,standards-docs). Both are noted in the layout section pointing at the follow-up issue — a docs PR should not quietly change behaviour.🤖 Generated with Claude Code